OAI/Analysis/AffineBernstein/AffineStripArea.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.verticalScale line 17
2. lemma OAI.AffineBernstein.verticalScale_apply line 27
3. lemma OAI.AffineBernstein.det_verticalScale line 30
4. theorem OAI.AffineBernstein.affine_image_strip_area line 45

   Source comment

   The exact epsilon power in source (strip-area), for the actual area of an affine-image boundary patch. Only this patch, not the whole transformed cap or graph, needs to lie in the coordinate box.

   theorem affine_image_strip_area {n : ℕ} {Ω 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 × ℝ)
       (j : Fin n ⊕ Unit) {R ε : ℝ} (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)
       (hstrip : ∀ x ∈ K, |ambientCoordinates n (L (x,u x)+v) j| ≤ ε) :
       Real.rpow |L.toContinuousLinearMap.det| ((n:ℝ)/((n:ℝ)+2)) *
         (∫ x in K, affineAreaDensity u x) ≤
         (graphAreaBoxBound n (2*max R 1)).toReal * ε^((n:ℝ)/((n:ℝ)+2)) := by
   …

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