RootLogComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integral_root_log_comparison line 24

Source documentation

The actual finite-root logarithmic comparison, with an explicit uniform geometric remainder and the Q-averaged physical shape defect.

lemma integral_root_log_comparison (hm : Monotone q) (hpos : ∀ j, 0 ≤ q j)
    (hnz : ∀ j : Fin (L+1), q j.succ≠0) (hroot : q 0=0) (hend : q (Fin.last (L+1))=1)
    (hV : ∀ z i, TerminalInterior L (rootTower T Q (fun j => q j.succ) base old z)
      (fun y => rootVector (fun w j => spin (V w j)) z y i))
    (a : ℕ) (F : (Fin a → Spin) → ℝ) {C : ℝ} (hC : 0≤C) (hF : ∀ s, |F s|≤C) (K : ℕ) :
    |(∫ z, sameInsertionAverage T Q (fun j => q j.succ) base old V a F z ∂μ)-
      (∫ z, independentInsertion T Q (fun j => q j.succ) base old V a F z
        ∂Measure.pi (fun _ : Fin a => μ.prod (siteLaw N)))| ≤
      2*(∑' k : ℕ, |insertionRadius C|^(k+K+1)/(k+K+1))+
      ∑ k∈Finset.range K, |insertionRadius C|^(k+1)/(k+1)*((a:ℝ)*
        qExpect q (fun S => shapeDeviation μ (rootAlphabet (Ω := Ω) (A := A)) S
…

Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.HeterogeneousMarks.rootTower, OAI.DilutedSpinGlass.HeterogeneousMarks.rootVector, OAI.DilutedSpinGlass.spin, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.HeterogeneousMarks.sameInsertionAverage, OAI.DilutedSpinGlass.HeterogeneousMarks.independentInsertion, OAI.DilutedSpinGlass.insertionRadius, OAI.DilutedSpinGlass.HeterogeneousMarks.rootAlphabet