OAI/Probability/DilutedSpin/HeterogeneousVariance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.correctedRoot_family_variance line 16

   Source documentation

   The random-count convex correction has its own addition/deletion cost. Replacement of an existing root point is unaffected.

   theorem correctedRoot_family_variance
       (μ : Measure I) [IsProbabilityMeasure μ] (r : ℝ≥0)
       (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
       (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
       (base : FinitePath Ω L → ℝ)
       (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ) {C : ℝ} (hC : 0 ≤ C)
       (hf : ∀ i x y, |Real.log (factor i x y)| ≤ C) (c : ℝ) :
       variance (fun z : Sigma (RootPath I) =>
         root T Q m base (rootArray z.1 z.2) factor+c*z.1)
         (familyLaw (poissonMeasure r) (fun n => rootLaw n (fun _ => μ))) ≤
           (2*C^2+(C+|c|)^2)*(r : ℝ) := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.HeterogeneousMarks.root, OAI.DilutedSpinGlass.rootArray, OAI.DilutedSpinGlass.familyLaw, OAI.DilutedSpinGlass.rootLaw