OAI/Probability/DilutedSpin/ParameterConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.PhysicalRoot.spin_parameter_concentration line 17

   Source documentation

   Concentration averaged over the literal infinite dictionary parameter law. All other coordinates remain fixed during the one-coordinate estimate.

   theorem spin_parameter_concentration
       (μ : Measure X) [IsProbabilityMeasure μ] (ν : Measure I) [IsProbabilityMeasure ν]
       (ξ : Measure Y) [IsProbabilityMeasure ξ] (r s : ℝ≥0)
       (V : X → (Fin N → Spin) → ℝ) (field : Y → ℝ)
       (hVm : ∀ σ, Measurable (fun x => V x σ)) (hhm : Measurable field)
       {C H c : ℝ} (hC : 0 ≤ C) (hc : 0 < c)
       (hV : ∀ x σ, |V x σ| ≤ C) (hh : ∀ y, |field y| ≤ H)
       (Q : (i : I) → Fin (L+1) → FiniteLaw (A i)) (m : Fin (L+1) → ℝ)
       (hm : ∀ l, c ≤ m l)
       (key : I → J) (a b t : J → ℝ) (hab : ∀ j, a j < b j)
       (hI : ∀ j, Icc (a j) (b j) ⊆ Icc (-(1:ℝ)/4) (1/4)) (ht : ∀ j, |t j| ≤ 1/4)
       (D E : (i : I) → FinitePath (Fin N → Spin) (L+1) → FinitePath (A i) (L+1) → ℝ)
   …

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