L2ConvexTails.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A single deterministic sequence of finite convex tail combinations for a countable family of uniformly L²-bounded random variables. Both L² convergence and simultaneous almost-sure convergence are obtained.

lemma OAI.SLEExactGauge.ae_tendsto_Lp_of_summable_errors line 19
lemma OAI.SLEExactGauge.ae_coeFn_weighted_sum line 33
theorem OAI.SLEExactGauge.exists_L2_convex_tail_limit line 40

theorem OAI.SLEExactGauge.exists_randomVariable_convex_tail_limit line 61

Source documentation

The same extraction stated for actual random variables, rather than chosen representatives of their L² classes.

theorem exists_randomVariable_convex_tail_limit (f : ℕ → ℕ → Ω → ℝ)
    (hf : ∀ n j, MemLp (f n j) 2 P)
    (hbound : ∀ j, ∃ B : ℝ, ∀ n, ‖(hf n j).toLp (f n j)‖ ≤ B) :
    ∃ x : ℕ → Lp ℝ 2 P, ∃ s : ℕ → Finset ℕ, ∃ w : ℕ → ℕ → ℝ,
      (∀ n i, i ∈ s n → 0 ≤ w n i) ∧
      (∀ n, ∑ i ∈ s n, w n i = 1) ∧
      (∀ j, Tendsto (fun n => ∑ i ∈ s n, w n i • (hf (n+i) j).toLp (f (n+i) j))
        atTop (𝓝 (x j))) ∧
      (∀ᵐ ω ∂P, ∀ j,
        Tendsto (fun n => ∑ i ∈ s n, w n i * f (n+i) j ω) atTop (𝓝 (x j ω))) := by
…