OAI/Analysis/AffineBernstein/DualDetCompact.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.affineMaximal_dual_det_phase_bound line 19
2. lemma OAI.AffineBernstein.positionSquared_eq_norm_sq line 49
3. lemma OAI.AffineBernstein.dualHeight_zero line 52
4. lemma OAI.AffineBernstein.affineMaximal_det_inverse_upper_of_modulus line 58

   Source documentation

   Determinant lower estimate from the original PDE and the genuinely geometric, all-base section modulus. The dual section is pulled back to primal coordinates, avoiding any assumed Legendre-PDE regularity.

   lemma affineMaximal_det_inverse_upper_of_modulus {n : ℕ} {O : Set (Space n)}
       (hO : IsOpen O) (hcv : Convex ℝ O) {u : Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u O) (hp : ∀ x ∈ O, (hessian u x).PosDef)
       (hm : AffineMaximalOn O u) {r : ℝ} (hr : 0 < r)
       (hball : Metric.closedBall (0:Space n) r ⊆ O) (b : ℝ → ℝ)
       (hb : 0 < b r) (hmod : HasLowerSectionModulus O u b) :
       ((hessian u 0).det)⁻¹ ≤
         (2*(n:ℝ)*((n:ℝ)+2)*(2*(r^2+1)))^n * (b r/2)^2 *
           Real.exp (r^2/(4*(r^2+1))) / (b r/2)^(n+2) := by
   …

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