OAI/Probability/DilutedSpin/ConcreteAnalyticSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.ConcreteReservoir.actual_analytic_selection line 21

   Source documentation

   Selection and analytic extraction for the literal physical diluted model. There is one parameter vector per selected size and ONE complete old reservoir for all trees, tests, colors, and probe indices. No score or coefficient-limit assumption occurs in this statement. This is the bounded-stage producer, not the main variational formula.

   theorem actual_analytic_selection (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)
       (hw : ∀ j, 0 < ν.real {j})
       (hD : ∀ q σ y, |D q σ y| ≤ 1) (hE : ∀ q σ y, |E q σ y| ≤ 1)
       {ε : ℝ} (hε : 0 < ε) :
       ∃ (Ns : ℕ → ℕ) (us : ℕ → K×ℕ → ℝ), StrictMono Ns ∧
         (∀ n i, us n i ∈ Icc (probeLow i.2) (probeHigh i.2)) ∧
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.probeLow, OAI.DilutedSpinGlass.probeHigh