ActualProductBounds.lean`

2 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_product_minors_bound line 18

Source comment

Integrating the actual large-principal-minor bound over all unit fiber normals. This is the product-measure bound in bounds.tex (hessian-minor-bound), including base dimension zero. No polynomial determinant bound is assumed.

theorem affineEpigraph_product_minors_bound {n k m : ℕ} (hm : 1 ≤ m)
    {Ω : 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 × Space m) ≃L[ℝ] (Space n × ℝ))
    {D : Set (Space k)} (hD : IsOpen D) (hcD : Convex ℝ D)
    (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ D, (0:Space m) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    {Q : Set (Space k)} (hQ : MeasurableSet Q) (hQD : Q ⊆ D)
    {r M R : ℝ} (hr : 0 < r) (hM : 0 ≤ M)
    (hball : ∀ s ∈ Q, Metric.closedBall s r ⊆ D)
    (hbound : ∀ s ∈ D, ∀ y : Space m, (s,y) ∈ affineEpigraphPullback Ω u a L → ‖y‖ ≤ M)
    (hR : ∀ s ∈ Q, ‖s‖ ≤ R) :
…

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

theorem OAI.AffineBernstein.affineEpigraph_product_fiber_area_bound line 61

Source comment

The literal fiber cofactor density integrated over a bounded base set. The transverse dimension-one endpoint is retained.

theorem affineEpigraph_product_fiber_area_bound {n k m : ℕ} (hm : 1 ≤ m)
    {Ω : 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 × Space m) ≃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:Space m) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    {Q : Set (Space k)} (hQ : MeasurableSet Q) (hQD : Q ⊆ D) {M : ℝ}
    (hbound : ∀ s ∈ Q, ∀ y : Space m, (s,y) ∈ affineEpigraphPullback Ω u a L → ‖y‖ ≤ M) :
    let H := fun q : Space k × Space m =>
…

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