OAI/Probability/DilutedSpin/PhysicalNewSpin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.newSpin_field_marginal line 12
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.averagedEnergyRoot_newSpin line 50

   Source documentation

   Removing marks on the new site and then summing out that spin gives the actual cavity-site root, with precisely the O(s/N) projection error.

   lemma averagedEnergyRoot_newSpin
       (ξ : Measure Y) [IsProbabilityMeasure ξ] (ν : Measure I) [IsProbabilityMeasure ν] (s : ℝ≥0)
       (Q : (i : I) → Fin (L+1) → FiniteLaw (A i)) (m : Fin (L+1) → ℝ)
       (hm : ∀ d,0 < m d) (hend : m (Fin.last L)=1)
       (ψ : (i : I) → Spin → FinitePath (A i) (L+1) → ℝ)
       (field : Y → ℝ) (hhm : Measurable field) (E : (Fin N → Spin) → ℝ)
       (θ : Fin k → InteractionSample p) (j : Fin k × Fin (p-1) → Fin N)
       {H D : ℝ} (hH : 0≤H) (hh : ∀ y,|field y|≤H)
       (hf : ∀ i σ a,|Real.log (ψ i σ a)|≤D) :
       |averagedEnergyRoot ξ (ν.prod (finiteUniform (Fin (N+1)))) s
         (fun i : I×Fin (N+1) => Q i.1) m field (locatedFactor ψ)
         (fun σ : Fin (N+1) → Spin => E (fun i => σ i.succ)+
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.finiteUniform