OAI/Probability/DilutedSpin/CavitySplit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.oneNewRate line 10
2. lemma OAI.DilutedSpinGlass.cavityOldRate_card line 13
3. lemma OAI.DilutedSpinGlass.cavityOneRate_card line 23
4. lemma OAI.DilutedSpinGlass.cavity_compound_split line 39

   Source documentation

   Exact old-site / one-new-site split of the physical Poisson energy after discarding only indices meeting the new site at least twice. No symmetry of the interaction has yet been used; the distinguished coordinate is explicit.

   lemma cavity_compound_split (α : ℝ≥0) (q N : ℕ) [NeZero N]
       (V : X × (Fin (q+1) → Fin (N+1)) → E) (hV : Measurable V) :
       compoundPoisson (α*(N+1)) (Measure.map (fun z => if CavityGood z.2 then V z else 0)
         (μ.prod (finiteUniform (Fin (q+1) → Fin (N+1))))) =
         compoundPoisson (reservoirRate α q N)
           (Measure.map (fun z : X × (Fin (q+1) → Fin N) => V (z.1,fun i => (z.2 i).succ))
             (μ.prod (finiteUniform (Fin (q+1) → Fin N)))) ∗
         compoundPoisson (oneNewRate α q N)
           (Measure.map (fun z : X × (Fin (q+1) × (Fin q → Fin N)) =>
               V (z.1,z.2.1.insertNth 0 (fun i => (z.2.2 i).succ)))
             (μ.prod (finiteUniform (Fin (q+1) × (Fin q → Fin N))))) := by
   …

   Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.compoundPoisson, OAI.DilutedSpinGlass.CavityGood, OAI.DilutedSpinGlass.finiteUniform, OAI.DilutedSpinGlass.reservoirRate, OAI.DilutedSpinGlass.oneNewRate