OAI/Probability/DilutedSpin/JointGridSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.UniversalDictionary.joint_grid_selection line 14

   Source documentation

   A single grid reservoir sequence, with its regular singleton base case and EVERY actual centered multileaf history simultaneously.

   theorem joint_grid_selection (M : Model p) {C H : ℝ} (hC : 0 ≤ C) (hH : 0 ≤ H)
       (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)
       {ε : ℝ} (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 (gridExponents L) direction anchor M (Ns n) (us n) ≤
           liminf (pressure M) atTop+ε) ∧
         (∀ η : ℝ, 0 < η → ∀ t : ℝ, 0 < t → ∀ᶠ n in atTop,
           ∀ d ∈ regularSingletonDepths L η,
   …

   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.gridExponents, OAI.DilutedSpinGlass.UniversalDictionary.direction, OAI.DilutedSpinGlass.UniversalDictionary.anchor, OAI.DilutedSpinGlass.pressure, OAI.DilutedSpinGlass.UniversalDictionary.regularSingletonDepths