EntireAndDoubling.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.affineMaximal_entire_and_balance line 19
Source documentation
The global geometric part of the exact main theorem: the nonempty open convex base is all of Euclidean space, and one section-balance constant works at all centers and heights. This is not the quadratic-rigidity conclusion.
```
theorem affineMaximal_entire_and_balance {n : ℕ} (hn : 3 ≤ n) (hn9 : n ≤ 9)
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
    (hc : EuclideanGraphComplete Ω u) :
    Ω = univ ∧ ∃ ρ : ℝ, 0 < ρ ∧ ρ ≤ 1 ∧ SectionBalance univ u ρ := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.SectionBalance

theorem OAI.AffineBernstein.affineMaximal_entire_gap_doubling line 31

Source documentation

Uniform tangent-gap doubling is also produced, with the manuscript's exact constants and no global growth assumption.

theorem affineMaximal_entire_gap_doubling {n : ℕ} (hn : 3 ≤ n) (hn9 : n ≤ 9)
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
    (hc : EuclideanGraphComplete Ω u) :
    Ω = univ ∧ ∃ ρ : ℝ, 0 < ρ ∧ ρ ≤ 1 ∧ ∀ a x : Space n,
      tangentHeight u a (a+(1+ρ/2) • (x-a)) ≤
        ((2+ρ)*(1+ρ)/ρ) * tangentHeight u a x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.tangentHeight

def OAI.AffineBernstein.logHessianDet line 52
Source documentation
The logarithm is taken only on the positive Hessian determinant at points where the estimates are asserted. Outside the domain this is just a total function.
```
def logHessianDet {n : ℕ} (u : Space n → ℝ) (x : Space n) : ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.inverseHessianTrace line 57
Source documentation
The actual inverse-Hessian linearized operator, without the harmless positive determinant factor in the frozen original PDE.
```
def inverseHessianTrace {n : ℕ} (u f : Space n → ℝ) (x : Space n) : ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.inverseHessianPair line 60
lemma OAI.AffineBernstein.contDiffAt_logHessianDet line 64
lemma OAI.AffineBernstein.contDiffOn_logHessianDet line 69
lemma OAI.AffineBernstein.affineMaximal_inverseHessianTrace_zero line 75
lemma OAI.AffineBernstein.affineWeight_eq_exp_logHessianDet line 87
theorem OAI.AffineBernstein.affineMaximal_logHessianDet_equation line 95
Source documentation
The exact logarithmic form of the original affine maximal equation. It is derived from the frozen determinant exponent, not a replacement PDE.
```
theorem affineMaximal_logHessianDet_equation {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
    {x : Space n} (hx : x ∈ Ω) :
    inverseHessianTrace u (logHessianDet u) x =
      (((n : ℝ)+1)/((n : ℝ)+2)) *
        inverseHessianPair u (logHessianDet u) (logHessianDet u) x := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.inverseHessianTrace, OAI.AffineBernstein.logHessianDet, OAI.AffineBernstein.inverseHessianPair
lemma OAI.AffineBernstein.dirDeriv_logHessianDet line 132
Source documentation
The differential of the log determinant is the literal inverse-Hessian contraction of the differentiated Hessian.
```
lemma dirDeriv_logHessianDet {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : ContDiffAt ℝ ∞ u x) (hp : (hessian u x).PosDef) (v : Space n) :
    dirDeriv v (logHessianDet u) x =
      ∑ i, ∑ j, (hessian u x)⁻¹ i j * dirDeriv v (fun y => hessian u y i j) x := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.logHessianDet
lemma OAI.AffineBernstein.inverseHessianTrace_dirDeriv line 157