OAI/Analysis/AffineBernstein/GraphBallArea.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.measurableSet_inter_preimage_continuousOn line 14
2. lemma OAI.AffineBernstein.graph_area_vertical_patch_bound line 29
3. theorem OAI.AffineBernstein.graph_affine_area_in_box line 60

   Source documentation

   A dimension/radius-only bound for the literal affine area on any measurable part of a smooth strictly convex graph with |x_i|,|u| ≤ R. This proves the area-in-a-ball producer without assuming a surface-area or Gauss-map theorem: two injective coordinate projections supply its Jacobians directly.

   theorem graph_affine_area_in_box {Ω K : Set (Space n)}
       (hΩ : IsOpen Ω) (hc : Convex ℝ Ω) (hK : MeasurableSet K) (hKΩ : K ⊆ Ω)
       {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       {R : ℝ} (hR : 0 ≤ R) (hxR : ∀ x ∈ K, ∀ j, |x j| ≤ R)
       (huR : ∀ x ∈ K, |u x| ≤ R) :
       (∫⁻ x in K, ENNReal.ofReal ((hessian u x).det^(1/((n:ℝ)+2)))) ≤
         (2*n+1 : ℕ) * ((volume (Metric.closedBall (0 : Space n) n))^(1/((n:ℝ)+2)) *
         (volume (Metric.closedBall (0 : Space n) (n*R)))^(1-1/((n:ℝ)+2))) := by
   …

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

4. def OAI.AffineBernstein.graphAreaBoxBound line 158
5. lemma OAI.AffineBernstein.graphAreaBoxBound_ne_top line 162