OAI/Analysis/AffineBernstein/NormalizedLogVariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.AffineBernstein.BalancedNormalized line 19

   Source documentation

   Literal normalized solution data, produced by the actual centered section maps.

   structure BalancedNormalized {n : ℕ} (ρ R : ℝ) (v : Space n → ℝ) : Prop where
   …

   Mentions: OAI.AffineBernstein.Space

2. lemma OAI.AffineBernstein.normalized_gradient_bound line 29
3. lemma OAI.AffineBernstein.normalized_gradient_chord_bound line 63
4. theorem OAI.AffineBernstein.normalized_log_variance line 84

   Source documentation

   Uniform logarithmic variance for the actual inverse-Hessian operator. The determinant bounds and all geometric constant dependencies are outputs.

   theorem normalized_log_variance {n : ℕ} {ρ R : ℝ}
       (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hR : 1 ≤ R) :
       ∃ V : ℝ, 0 ≤ V ∧ ∀ v : Space n → ℝ, BalancedNormalized ρ R v →
         ∀ s : Space n → ℝ, ContDiff ℝ ∞ s → (∀ x, 0 < s x) →
         (∀ x, inverseHessianTrace v s x ≤ 0) →
         (∫ x in Metric.closedBall (0:Space n) (1/16:ℝ),
           ∫ y in Metric.closedBall (0:Space n) (1/16:ℝ),
             (Real.log (s y)-Real.log (s x))^2) ≤ V := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.BalancedNormalized, OAI.AffineBernstein.inverseHessianTrace