OAI/Probability/DilutedSpin/JointPhysicalSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.UniversalDictionary.joint_energy_matrix_selection line 16

   Source documentation

   ONE low-increment sequence simultaneously controls the singleton base case AND every actual multileaf centered matrix history. This avoids separately selected sequences at the base and inductive stages.

   theorem joint_energy_matrix_selection (m : Fin (L+1) → ℝ)
       (M : Model p) {C H c : ℝ} (hC : 0 ≤ C) (hH : 0 ≤ H) (hc : 0 < c)
       (hθ : ∀ᵐ z ∂M.disorder.toMeasure, ∀ σ, |z.1 σ| ≤ C)
       (hh : ∀ᵐ h ∂M.field.toMeasure, |h| ≤ H)
       (hθi : Integrable (fun z : InteractionSample p => ‖z.1‖) M.disorder.toMeasure)
       (hhi : Integrable (fun h : ℝ => |h|) M.field.toMeasure)
       (hm : ∀ l, c ≤ m l) (hmono : Monotone m) (hend : m (Fin.last L) = 1)
       {ε : ℝ} (hε : 0 < ε) :
       ∃ (Ns : ℕ → ℕ) (us : ℕ → Spec L×ℕ → ℝ), StrictMono Ns ∧
         (∀ n i, us n i ∈ Icc (probeLow i.2) (probeHigh i.2)) ∧
         (∀ n, ConcreteReservoir.increment (weights L) prior m direction anchor M (Ns n) (us n) ≤
           liminf (pressure M) atTop+ε) ∧
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.probeLow, OAI.DilutedSpinGlass.probeHigh, OAI.DilutedSpinGlass.ConcreteReservoir.increment, OAI.DilutedSpinGlass.UniversalDictionary.weights, OAI.DilutedSpinGlass.UniversalDictionary.prior, OAI.DilutedSpinGlass.UniversalDictionary.direction, OAI.DilutedSpinGlass.UniversalDictionary.anchor, OAI.DilutedSpinGlass.pressure