OAI/Analysis/AffineBernstein/LogMassWeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.tubeBasePair_coordinate_log line 18

   Source comment

   Exact coordinate formula for the true inverse-block logarithmic norm.

   lemma tubeBasePair_coordinate_log {k : ℕ} (H : Space k × E → ℝ) (q : Space k × E)
       (i : Fin k) (hq : q.1 i ≠ 0) :
       tubeBasePair H (EuclideanSpace.basisFun (Fin k) ℝ).toBasis
         (fun z => Real.log (z.1 i)) (fun z => Real.log (z.1 i)) q =
         H q*(tubeBaseMatrix H q (EuclideanSpace.basisFun (Fin k) ℝ).toBasis)⁻¹ i i/(q.1 i)^2 := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.tubeBasePair, OAI.AffineBernstein.tubeBaseMatrix

2. lemma OAI.AffineBernstein.tubeLogMassWeight_le_trace line 36

   Source comment

   On a positive base collar, the manuscript's sigma weight is bounded by one plus the actual inverse-Hessian trace, with the exact support-height factor.

   lemma tubeLogMassWeight_le_trace {k : ℕ} (H : Space k × E → ℝ) (q : Space k × E)
       {r M : ℝ} (hr : 0 < r) (hs : ∀ i, r ≤ q.1 i)
       (hh : 0 ≤ H q) (hhM : H q ≤ M)
       (hB : (tubeBaseMatrix H q (EuclideanSpace.basisFun (Fin k) ℝ).toBasis).PosDef) :
       tubeLogMassWeight H q ≤ 1 + (M/r^2)*(tubeBaseMatrix H q
         (EuclideanSpace.basisFun (Fin k) ℝ).toBasis)⁻¹.trace := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.tubeBaseMatrix, OAI.AffineBernstein.tubeLogMassWeight