OAI/Probability/DilutedSpin/CountableTagSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.countable_tag_parameter_selection line 14

   Source documentation

   Countable tags, including the manuscript's pairs (specification, probe), are selected simultaneously. The error array is not collapsed to finitely many specifications.

   theorem countable_tag_parameter_selection
       {Ω J : Type*} [MeasurableSpace Ω] [Countable J]
       (μ : Measure Ω) [IsProbabilityMeasure μ]
       (Δ : ℕ → Ω → ℝ) (e : J → ℕ → Ω → ℝ)
       (hΔ : ∀ N, Integrable (Δ N) μ) (he : ∀ j N, Integrable (e j N) μ)
       (hne : ∀ j N x, 0 ≤ e j N x)
       {C v u : ℝ} (hC : 0 ≤ C) (hvu : v < u)
       (hlower : ∀ N x, -C ≤ Δ N x)
       (hlow : ∀ n, ∃ N, n ≤ N ∧ ∫ x, Δ N x ∂μ ≤ v)
       (hlim : ∀ j, Tendsto (fun N => ∫ x, e j N x ∂μ) atTop (𝓝 0)) :
       ∃ (Ns : ℕ → ℕ) (xs : ℕ → Ω), StrictMono Ns ∧
         (∀ n, Δ (Ns n) (xs n) ≤ u) ∧
   …