OAI/Probability/DilutedSpin/MarkMeanProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.locatedTerminalRoot line 15
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.locatedTerminalRoot_bound line 24
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.locatedTerminalRoot_pullback line 38
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integral_locatedTerminalRoot line 51
5. def OAI.DilutedSpinGlass.HeterogeneousMarks.terminalMean line 82
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalMean_count_integral line 90
7. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalMean_mark_projection line 109

   Source documentation

   The original Poisson marked system may move mark sites off the added spin at cost exactly twice the mark amplitude times its expected new-site count.

   lemma terminalMean_mark_projection [NeZero N]
       (ν : Measure I) [IsProbabilityMeasure ν] (s : ℝ≥0)
       (Q : (i : I) → Fin (L+1) → FiniteLaw (A i)) (m : Fin (L+1) → ℝ) (hm : ∀ j,0 < m j)
       (ψ : (i : I) → Spin → FinitePath (A i) (L+1) → ℝ)
       (E : (Fin (N+1) → Spin) → ℝ)
       {D : ℝ} (hf : ∀ i σ a,|Real.log (ψ i σ a)|≤D) :
       |terminalMean ν s Q m ψ (id : Fin (N+1) → Fin (N+1)) E-
         terminalMean ν s Q m ψ (Fin.succ : Fin N → Fin (N+1)) E|≤2*D*s/(N+1) := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.terminalMean