OAI/Analysis/AffineBernstein/TiltedLIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.lintegral_inverse_trace_le_tilted line 20

   Source comment

   The tilted-cap trace estimate for nonnegative integrals, with no a priori integrability assumption on the trace being bounded.

   lemma lintegral_inverse_trace_le_tilted {α : Type*} [MeasurableSpace α]
       {μ : Measure α} {B : α → Matrix ι ι ℝ} {I : α → ℝ}
       (hB : ∀ᵐ x ∂μ, (B x).PosDef) (hI : 0 ≤ᵐ[μ] I)
       (hc : ∀ r, AEMeasurable (fun x => ENNReal.ofReal (I x*inverseMatrixPair (B x)
         (capTiltedCovector r) (capTiltedCovector r))) μ) :
       (∫⁻ x, ENNReal.ofReal (I x*(B x)⁻¹.trace) ∂μ) ≤
         ∑ r, ∫⁻ x, ENNReal.ofReal (I x*inverseMatrixPair (B x)
           (capTiltedCovector r) (capTiltedCovector r)) ∂μ := by
   …

   Mentions: OAI.AffineBernstein.inverseMatrixPair, OAI.AffineBernstein.capTiltedCovector

2. theorem OAI.AffineBernstein.affineEpigraph_sigma_cap_interpolation line 44

   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_cap_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