CountedSizeCoupling.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.SizeCoupling.abs_integral_sub_le_const line 15

theorem OAI.DilutedSpinGlass.SizeCoupling.fieldMean_size_coupling line 24

Source documentation

The independent additional field is integrated under its original law. The per-count cost is uniform in every auxiliary mark prior and parameter.

theorem fieldMean_size_coupling (ξ : Measure Y) [IsProbabilityMeasure ξ]
    {p r N k l : ℕ} [NeZero N] {B : Fin l → Type} [∀ i, Fintype (B i)]
    (field : Y → ℝ) (hfm : Measurable field)
    (theta : Fin k → InteractionSample p)
    (Q : (i : Fin l) → Fin (r+1) → FiniteLaw (B i)) (m : Fin (r+1) → ℝ)
    (hm : ∀ j, 0 < m j) (ψ : (i : Fin l) → Spin → FinitePath (B i) (r+1) → ℝ)
    {C H D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D)
    (hθ : ∀ j σ, |(theta j).1 σ| ≤ C) (hh : ∀ y, |field y| ≤ H)
    (hψ : ∀ i σ a, |Real.log (ψ i σ a)| ≤ D) :
    |(∫ h : RootPath Y (N+1), spinMean Q m theta (fun i => field (rootArray (N+1) h i)) ψ
        ∂rootLaw (N+1) (fun _ => ξ))-
      (∫ h : RootPath Y N, spinMean Q m theta (fun i => field (rootArray N h i)) ψ
…

Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.SizeCoupling.spinMean, OAI.DilutedSpinGlass.rootArray, OAI.DilutedSpinGlass.rootLaw

theorem OAI.DilutedSpinGlass.SizeCoupling.countedMean_size_coupling line 69

Source documentation

Uniform finite-size comparison for the same quenched countable dictionary and the same counts. All three root measures are the actual independent laws.

theorem countedMean_size_coupling (μ : Measure X) [IsProbabilityMeasure μ]
    (ξ : Measure Y) [IsProbabilityMeasure ξ] (ν : Measure I) [IsProbabilityMeasure ν]
    {p r N : ℕ} [NeZero N] (theta : X → InteractionSample p) (field : Y → ℝ)
    (hθm : ∀ σ, Measurable (fun x => (theta x).1 σ)) (hhm : Measurable field)
    (Q : (i : I) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
    (hm : ∀ j, 0 < m j) (ψ : (i : I) → Spin → FinitePath (A i) (r+1) → ℝ)
    {C H D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D)
    (hθ : ∀ x σ, |(theta x).1 σ| ≤ C) (hh : ∀ y, |field y| ≤ H)
    (hψ : ∀ i σ a, |Real.log (ψ i σ a)| ≤ D) (k l : ℕ) :
    |countedMean (N := N+1) μ ξ ν theta field Q m ψ k l-
…

Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.countedMean