OAI/Analysis/AffineBernstein/PositiveFaceMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.integral_le_good_add_cover line 21
2. theorem OAI.AffineBernstein.affine_image_good_area_lower line 40

   Source comment

   Quantitative positive area away from finitely many supporting faces.

   theorem affine_image_good_area_lower {n k : ℕ} {Ω K : Set (Space n)}
       (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) (hK : MeasurableSet K) (hKΩ : K ⊆ Ω)
       {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ)
       (s : Fin k → Fin n ⊕ Unit) {R ε c : ℝ} (hR : 0 ≤ R) (hε : 0 < ε)
       (hxR : ∀ x ∈ K, ∀ i, |(L (x,u x)+v).1 i| ≤ R)
       (htR : ∀ x ∈ K, |(L (x,u x)+v).2| ≤ R)
       (hlow : ∀ x ∈ K, ∀ i, -ε ≤ ambientCoordinates n (L (x,u x)+v) (s i))
       (harea : c ≤ Real.rpow |L.toContinuousLinearMap.det| ((n:ℝ)/((n:ℝ)+2)) *
         (∫ x in K, affineAreaDensity u x))
       (heps : (k:ℝ)*(graphAreaBoxBound n (2*max R 1)).toReal*ε^((n:ℝ)/((n:ℝ)+2)) ≤ c/2) :
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.ambientCoordinates, OAI.AffineBernstein.affineAreaDensity, OAI.AffineBernstein.graphAreaBoxBound