OAI/Probability/DilutedSpin/PerturbedEnergyMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.SizeCoupling.perturbedMean_energy_integral line 16

   Source documentation

   The literal perturbed physical mean as a compound Poisson energy integral. Counts, index repetitions, fields, and the full marked reservoir are retained.

   lemma perturbedMean_energy_integral
       (μ : Measure X) [IsProbabilityMeasure μ] (ξ : Measure Y) [IsProbabilityMeasure ξ]
       (ν : Measure I) [IsProbabilityMeasure ν] (r s : ℝ≥0)
       (theta : X → InteractionSample p) (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) μ ξ ν theta field Q m ψ r s =
   …

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

2. lemma OAI.DilutedSpinGlass.SizeCoupling.integrable_indexedPotential line 39
3. lemma OAI.DilutedSpinGlass.SizeCoupling.indexedPotential_norm_integral_bound line 48