OAI/Analysis/AffineBernstein/AffineBoxArea.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.triangular_graph_patch_area line 12
2. lemma OAI.AffineBernstein.triangularGraph_smooth_positive line 34
3. lemma OAI.AffineBernstein.integral_affineAreaDensity_le_box_measurable line 58
4. theorem OAI.AffineBernstein.affine_image_graph_area_in_box line 78

   Source documentation

   Genuine affine area of every bounded measurable patch of an arbitrary invertible affine image of the original convex graph. The constant depends only on dimension and the physical coordinate radius, not on the affine map.

   theorem affine_image_graph_area_in_box {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 × ℝ)
       {R : ℝ} (hR : 0 ≤ R)
       (hxR : ∀ x ∈ K, ∀ i, |(L (x,u x)+v).1 i| ≤ R)
       (htR : ∀ x ∈ K, |(L (x,u x)+v).2| ≤ R) :
       Real.rpow |L.toContinuousLinearMap.det| ((n:ℝ)/((n:ℝ)+2)) *
         (∫ x in K, affineAreaDensity u x) ≤ (graphAreaBoxBound n (2*R)).toReal := by
   …

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