ActualSigmaInterpolation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.affineEpigraph_sigma_interpolation line 20

Source comment

The genuine sigma density is controlled by exactly the three source geometric integrals: fiber area, large base minors, and cap inverse energy. No upper bound on sigma or on inverse energy is assumed.

theorem affineEpigraph_sigma_interpolation {n k : ℕ} (hn : 1 ≤ n) (hk : 1 ≤ k)
    {Ω : 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)
    (ν : Measure (Metric.sphere (0:E) 1)) [SFinite ν] {r ρ M : ℝ} (hr : 0 < r) (hρ : 0 < ρ)
    (hM : 0 ≤ M) (hbase : ∀ s ∈ Q, ∀ i, r ≤ s i)
    (hinner : ∀ s ∈ Q, Metric.closedBall (0:E) ρ ⊆ {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
…

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