ActualAreaMass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The first missing differential identity in sections/area.tex, Stationarity: the cofactor of an actual Hessian is divergence-free. The proof below uses multilinearity of the determinant and symmetry of second derivatives (Piola).

theorem OAI.AffineBernstein.affineEpigraph_area_le_sigma line 23

Source documentation

The literal spherical affine area is bounded in terms of the actual weighted sigma density, by Holder and the actual fiber support height.

theorem affineEpigraph_area_le_sigma {n k : ℕ} (hn : 1 ≤ n)
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (a : Space n × ℝ) (L : (Space k × E) ≃L[ℝ] (Space n × ℝ))
    {D : Set (Space k)} (hD : IsOpen D)
    (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ D, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
    {Q : Set (Space k)} (hQ : MeasurableSet Q) (hQD : Q ⊆ D) {M : ℝ} (hM : 0 ≤ M)
    (hbound : ∀ s ∈ Q, ∀ y : E, (s,y) ∈ affineEpigraphPullback Ω u a L → ‖y‖ ≤ M) :
    let H := fun q : Space k × E => homogeneousSupport {y | (q.1,y) ∈ affineEpigraphPullback Ω u a L} q.2
…

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