FaceSigmaTransport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.affineEpigraph_face_sigma_transport line 24

Source documentation

The original graph affine area over any compact-fiber rectangle is controlled by the actual weighted sigma mass. The multiplicity constant is fixed before all epigraphs and affine coordinates.

theorem affineEpigraph_face_sigma_transport {n k m d : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m)
    (e : Fin n ≃ Fin k ⊕ Fin d) (eE : Fin m ≃ Fin d ⊕ Unit)
    (f : WithLp 2 (Space d × ℝ) ≃ₗᵢ[ℝ] Space m) :
    ∃ CA > 0, ∀ {Ω : Set (Space n)}, IsOpen Ω → Convex ℝ Ω →
    ∀ {u : Space n → ℝ}, ContDiffOn ℝ ∞ u Ω → (∀ x ∈ Ω, (hessian u x).PosDef) →
    ∀ (a : Space n × ℝ) (L : (Space k × Space m) ≃L[ℝ] (Space n × ℝ))
      {D : Set (Space k)}, IsOpen D →
    (∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) →
    (∀ s ∈ D, (0:Space m) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) →
    ∀ {Q : Set (Space k)}, MeasurableSet Q → Q ⊆ D → ∀ {M : ℝ}, 0 ≤ M →
    (∀ s ∈ Q, ∀ y : Space m, (s,y) ∈ affineEpigraphPullback Ω u a L → ‖y‖ ≤ M) →
    ∀ {K : Set (Space n)}, K ⊆ Ω → (∀ x ∈ K, (L.symm ((x,u x)-a)).1 ∈ Q) →
…

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