PhysicalCavitySplit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.SizeCoupling.perturbedMean_averagedEnergyRoot line 14

lemma OAI.DilutedSpinGlass.SizeCoupling.perturbedMean_cavity_split line 40

Source documentation

The actual new system differs from its reservoir-plus-cavity energy law only by the double-new-coordinate rate. All physical field and mark averages are retained, with their original counts and sites.

lemma perturbedMean_cavity_split
    (μ : Measure X) [IsProbabilityMeasure μ] (ξ : Measure Y) [IsProbabilityMeasure ξ]
    (ν : Measure I) [IsProbabilityMeasure ν] (α s : ℝ≥0)
    (theta : X → InteractionSample (q+1)) (field : Y → ℝ)
    (hθm : ∀ σ,Measurable (fun x => (theta x).1 σ)) (hhm : Measurable field)
    (Q : (i : I) → Fin (L+1) → FiniteLaw (A i)) (m : Fin (L+1) → ℝ) (hm : ∀ i,0 < m i)
    (ψ : (i : I) → Spin → FinitePath (A i) (L+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) :
    |perturbedMean (N := N+1) μ ξ ν theta field Q m ψ (α*(N+1)) s -
…

Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.perturbedMean