OAI/Probability/DilutedSpin/PhysicalSelectedConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The concentration envelope for the actual bounded physical spin energy, with all heterogeneous dictionary marks retained.

   theorem spin_selected_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 : ∀ j, c ≤ m j)
       (sel : I → Bool)
       (fixed D E : (i : I) → FinitePath (Fin N → Spin) (L+1) → FinitePath (A i) (L+1) → ℝ)
       (hf : ∀ i x y, |Real.log (fixed i x y)| ≤ 1)
   …

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