NormalizedDetLower.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.normalized_det_lower_producer line 19

Source documentation

Genuine uniform determinant lower producer on the exact fixed ball used in rigidity. All constants precede the solution. No determinant/Hessian bound or estimate from the missing TW producer is a premise.

theorem normalized_det_lower_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 →
      HasLowerSectionModulus (Metric.ball 0 (1/4 : ℝ)) f b →
      c ≤ (hessian f 0).det := by
…

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

theorem OAI.AffineBernstein.normalized_det_two_sided_producer line 47

Source documentation

The determinant stage of the Trudinger--Wang proof, with both constants uniform and with the source PDE/modulus retained. This is not yet uniform ellipticity: determinant bounds alone do not bound individual eigenvalues.

theorem normalized_det_two_sided_producer (n : ℕ) (b : ℝ → ℝ)
    (hb : ∀ r : ℝ, 0 < r → 0 < b r) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ 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 →
      c ≤ (hessian f 0).det ∧ (hessian f 0).det ≤ C := by
…

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