Documentation

Lean 4 Proof

theorem information_shadow (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) :
    0 < curvatureK J ρ :=
  curvatureK_pos hJ hρ

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:154

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file