TiltedTrace.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.capTiltedCovector line 16
Source comment
Every coefficient of these covectors is positive, so their affine caps are uniformly bounded in the orthant model.
```
def capTiltedCovector (r : ι) (i : ι) : ℝ := 1 + (Pi.single r (1:ℝ) : ι → ℝ) i
```
lemma OAI.AffineBernstein.inverse_trace_tilted_identity line 18
lemma OAI.AffineBernstein.inverse_trace_le_tilted line 45
Source comment
The literal trace of the inverse Hessian is controlled by the finite family of tilted cap energies, with sharp coefficient one.
```
lemma inverse_trace_le_tilted {A : Matrix ι ι ℝ} (hA : A.PosDef) :
    A⁻¹.trace ≤ ∑ r, inverseMatrixPair A (capTiltedCovector r) (capTiltedCovector r) := by
…
```
Mentions: OAI.AffineBernstein.inverseMatrixPair, OAI.AffineBernstein.capTiltedCovector
lemma OAI.AffineBernstein.inverse_trace_nonneg line 51

theorem OAI.AffineBernstein.integral_inverse_trace_le_cap_sum line 56

Source comment

Integration of the preceding finite-family estimate. This closes the last purely algebraic summation step after actual cap transport.

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

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