OAI/Probability/DilutedSpin/MarkSiteCoupling.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot_mark_sites line 16

   Source documentation

   Move only perturbation sites off the added spin, leaving energy and all auxiliary mark labels and count laws unchanged.

   lemma terminalRoot_mark_sites
       (Q : (i : I) → Fin (L+1) → FiniteLaw (A i)) (m : Fin (L+1) → ℝ)
       (hm : ∀ j,0 < m j) (E : (Fin (N+1) → Spin) → ℝ) (roots : Fin k → I)
       (ψ : (i : I) → Spin → FinitePath (A i) (L+1) → ℝ)
       {D : ℝ} (hψ : ∀ i s a,|Real.log (ψ i s a)|≤D)
       (z : Fin k → Fin (N+1) × Fin N) :
       |terminalRoot (fun _ : Fin (N+1) => false) FiniteLaw.uniform
           (fun j : Fin k => Q (roots j)) m E id
           (fun j σ a => ψ (roots j) (σ (newIndex (z j))) a) -
         terminalRoot (fun _ : Fin (N+1) => false) FiniteLaw.uniform
           (fun j : Fin k => Q (roots j)) m E id
           (fun j σ a => ψ (roots j) (σ (oldIndex (z j)).succ) a)| ≤
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot, OAI.DilutedSpinGlass.FiniteLaw.uniform

2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot_mark_site_expect line 47
3. def OAI.DilutedSpinGlass.PhysicalRoot.indexedPotential line 89
4. def OAI.DilutedSpinGlass.PhysicalRoot.locatedFactor line 93
5. lemma OAI.DilutedSpinGlass.PhysicalRoot.measurable_indexedPotential line 98
6. lemma OAI.DilutedSpinGlass.PhysicalRoot.rootSample_eq_spinRoot line 109