NormalizedDet.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.HasLowerSectionModulus line 18
Source documentation
Prescribed lower modulus of tangent sections; this is the same section condition as rigidity.tex, with the frozen tangentSection definition.
```
def HasLowerSectionModulus {n : ℕ} (O : Set (Space n)) (f : Space n → ℝ)
    (b : ℝ → ℝ) : Prop :=
…
```
Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.normalized_det_upper_producer line 26

Source documentation

A genuine solution-uniform nonlinear estimate. The determinant bound is produced from the unchanged PDE, oscillation and section modulus, rather than postulated. This is an intermediate estimate, not the TW Hessian/C³ producer or the full Bernstein theorem.

theorem normalized_det_upper_producer (n : ℕ) (b : ℝ → ℝ)
    (hb : ∀ r : ℝ, 0 < r → 0 < b r) :
    ∃ C > (0:ℝ), ∀ f : Space n → ℝ,
      ContDiffOn ℝ ∞ f (Metric.ball 0 (1/4 : ℝ)) →
      (∀ x ∈ Metric.ball (0 : Space n) (1/4 : ℝ), (hessian f x).PosDef) →
      AffineMaximalOn (Metric.ball 0 (1/4 : ℝ)) f →
      (∀ x ∈ Metric.ball (0 : Space n) (1/4 : ℝ), -1 ≤ f x ∧ f x ≤ 0) →
      HasLowerSectionModulus (Metric.ball 0 (1/4 : ℝ)) f b →
      (hessian f 0).det ≤ C := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.HasLowerSectionModulus