Komlos lemma: uniform convergence and diagonal lemma

BrownianMotion/StochasticIntegral/ConvexWeights.lean

@@ -9,80 +9,39 @@ public import Mathlib.MeasureTheory.Function.LpSpace.Basic
 
 @[expose] public section
 
-variable {R : Type*} [PartialOrder R] [Semiring R] {M N P : Type*}
+variable {R : Type*} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M N P : Type*}
 
-namespace Convexity.StdSimplex
+namespace Convexity
 
-instance instFunLike : FunLike (StdSimplex R M) M R := {
-  coe s := s.weights.toFun
-  coe_injective := fun _ _ h ↦ ext (Finsupp.ext fun i ↦ congrFun h i)
-}
-
-variable [IsStrictOrderedRing R]
-
-/-- Given convex weights `a : StdSimplex R ι` and a family of convex weights
-`b : ι → StdSimplex R ι'`, `StdSimplex.bind a b` is the convex combination of the `b k`, weighted
-by `a`, defined as monadic bind. -/
-noncomputable def bind (a : StdSimplex R M) (b : M → StdSimplex R N) : StdSimplex R N :=
-  (a.map b).join
-
-variable (a : StdSimplex R M) (b : M → StdSimplex R N)
-
-@[simp]
-lemma bind_single (i : M) : bind (single i) b = b i := by simp [bind, join]
-
-@[simp]
-lemma bind_const (c : StdSimplex R N) : bind a (fun _ ↦ c) = c := by simp [bind, join]
-
-lemma weights_bind :
-    (bind a b).weights = (fun m ↦ ∑ k ∈ a.weights.support, a.weights k * (b k).weights m) := by
-  ext m
-  rw [bind, join, map]
-  simp only [Finsupp.sum_apply]
-  rw [Finsupp.sum_mapDomain_index (fun _ => by simp) (fun _ _ _ => by simp [add_mul])]
-  simp [Finsupp.sum]
-
-lemma support_subset_support_bind {a : StdSimplex R M} (b : M → StdSimplex R N)
-    {i : M} (hi : i ∈ a.weights.support) :
-    (b i).weights.support ⊆ (bind a b).weights.support := by
-  intro m hm
-  have hpos : 0 < a.weights i * (b i).weights m :=
-    mul_pos ((a.nonneg i).lt_of_ne' (by grind)) (((b i).nonneg m).lt_of_ne' (by grind))
-  have hnonneg (k : M) (hk : k ∈ a.weights.support) : 0 ≤ a.weights k * (b k).weights m := by
-    exact mul_nonneg (a.nonneg k) ((b k).nonneg m)
-  have hsum_pos : 0 < ∑ k ∈ a.weights.support, a.weights k * (b k).weights m :=
-    lt_of_lt_of_le hpos (Finset.single_le_sum hnonneg hi)
-  rw [Finsupp.mem_support_iff, weights_bind]
-  positivity
+open StdSimplex
 
 /-- Given a doubly-indexed family of convex weights `cw : ℕ → ℕ → StdSimplex R ℕ`,
-`iteratedBind cw k n` is the iterated convex multiplication obtained by combining
-the weights `cw 0 n, cw 1 n, …, cw k n` via `StdSimplex.bind`. -/
-noncomputable def iteratedBind (cw : ℕ → ℕ → StdSimplex R ℕ) : ℕ → ℕ → StdSimplex R ℕ
+`iteratedComb cw k n` is the iterated convex multiplication obtained by combining
+the weights `cw 0 n, cw 1 n, …, cw k n` via `iConvexComb`. -/
+public noncomputable def iteratedComb (cw : ℕ → ℕ → StdSimplex R ℕ) : ℕ → ℕ → StdSimplex R ℕ
   | 0 => cw 0
-  | k + 1 => fun n ↦ bind (cw (k + 1) n) (iteratedBind cw k)
+  | k + 1 => fun n ↦ iConvexComb (cw (k + 1) n) (iteratedComb cw k)
 
-lemma iteratedBind_congr {cw1 cw2 : ℕ → ℕ → StdSimplex R ℕ} {k : ℕ}
+lemma iteratedComb_congr {cw1 cw2 : ℕ → ℕ → StdSimplex R ℕ} {k : ℕ}
     (h : ∀ i ≤ k, cw1 i = cw2 i) :
-    iteratedBind cw1 k = iteratedBind cw2 k := by
+    iteratedComb cw1 k = iteratedComb cw2 k := by
   induction k with
-  | zero => simp [iteratedBind, h]
-  | succ k ih => simp [iteratedBind, h, ih (fun i hi => h i (Nat.le_succ_of_le hi))]
+  | zero => simp [iteratedComb, h]
+  | succ k ih => simp [iteratedComb, h, ih (fun i hi => h i (Nat.le_succ_of_le hi))]
 
-lemma bind_sum_smul {E : Type*} (f : N → E) [AddCommGroup E] [Module R E] [IsDomain R] :
-  (bind a b).weights.sum (fun m cwm ↦ cwm • f m) =
+lemma iConvexComb_sum_smul {E : Type*} (a : StdSimplex R M) (b : M → StdSimplex R N) (f : N → E)
+    [AddCommGroup E] [Module R E] [IsDomain R] :
+    (iConvexComb a b).weights.sum (fun m cwm ↦ cwm • f m) =
   a.weights.sum (fun i wi ↦ wi • (b i).weights.sum (fun m bm ↦ bm • f m)) := by
   classical
-  simp only [bind, StdSimplex.join, StdSimplex.map]
+  simp only [iConvexComb, weights_sConvexComb, weights_map]
   rw [Finsupp.sum_sum_index (fun _ => by simp) (fun _ _ _ => by simp [add_smul]),
       Finsupp.sum_mapDomain_index (fun _ => by simp)
       (fun d r₁ r₂ => by simp [add_smul, Finsupp.sum_add_index, add_smul])]
   simp only [Finsupp.sum]
-  refine Finset.sum_congr rfl ?_
-  intro i hi
-  have hsupp : (a.weights i • (b i).weights).support = (b i).weights.support :=
-    Finsupp.support_smul_eq (by grind)
-  simp [hsupp, Finset.smul_sum, Finsupp.smul_apply, smul_smul]
+  refine Finset.sum_congr rfl fun i hi => ?_
+  rw [Finsupp.support_smul_eq (by grind)]
+  simp [Finset.smul_sum, Finsupp.smul_apply, smul_smul]
 
 open MeasureTheory
 open scoped ENNReal NNReal
@@ -116,4 +75,4 @@ lemma coeFn_sum_smul {μ : Measure Ω} {p : ℝ≥0∞} (s : Finset ℕ) (c : 
     exact (Lp.coeFn_add _ _).trans <|
       ((Lp.coeFn_smul _ _).trans ((hmem j).coeFn_toLp.const_smul (c j))).add ih
 
-end Convexity.StdSimplex
+end Convexity

BrownianMotion/StochasticIntegral/Komlos.lean

@@ -123,7 +123,6 @@ lemma komlos_norm [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpac
   rcases CompleteSpace.complete g_cauchy with ⟨x, hx⟩
   tauto
 
-
 lemma exists_stdSimplex_of_mem_convexHull {M ι : Type*} [AddCommGroup E] [Field M] [LinearOrder M]
     [IsStrictOrderedRing M] [Module M E] {s : ι → E} {x : E}
     (hx : x ∈ convexHull M (Set.range s)) :
@@ -166,16 +165,18 @@ lemma convex_combination_bounded {x : ℕ → E}
   refine mul_le_of_le_one_left ?_ bound
   exact le_trans (norm_nonneg (x 0)) (hx 0)
 
+open Convexity
+
 /-- `komlosFormula x cw k n` is the convex combination of the stage-`k` vectors `x k m`,
 weighted by `iteratedBindSimplex cw k n`. It is the sequence whose convergence is
 established at each stage of the Komlós construction. -/
 noncomputable def komlosFormula (x : ℕ → ℕ → E) (cw : ℕ → ℕ → StdSimplex ℝ ℕ) (k i n : ℕ) : E :=
-  (StdSimplex.iteratedBind cw k n).weights.sum (fun m cwm ↦ cwm • x i m)
+  (iteratedComb cw k n).weights.sum (fun m cwm ↦ cwm • x i m)
 
 lemma komlosFormula_congr (x : ℕ → ℕ → E) {cw1 : ℕ → ℕ → StdSimplex ℝ ℕ}
   {cw2 : ℕ → ℕ → StdSimplex ℝ ℕ} {k : ℕ} (h : ∀ k' ≤ k, cw1 k' = cw2 k') :
   komlosFormula x cw1 k = komlosFormula x cw2 k := by
-  unfold komlosFormula; rw [StdSimplex.iteratedBind_congr]
+  unfold komlosFormula; rw [iteratedComb_congr]
   exact h
 
 /--
@@ -185,6 +186,13 @@ every `y n` can be written as a convex combination of elements `x k` with `k ≥
 def convexTail (x : ℕ → E) : Set (ℕ → E) :=
   { y | ∀ n, y n ∈ convexHull ℝ (Set.range (fun m ↦ x (n + m))) }
 
+lemma convexTail_self (x : ℕ → E) : x ∈ convexTail x := by
+  simp only [convexTail, Set.mem_setOf_eq]
+  intro n
+  rw [mem_convexHull_iff_exists_fintype]
+  use (Fin 1), (by infer_instance), (fun _ ↦ (1 : ℝ)), (fun _ ↦ (x n))
+  simp [Exists.intro 0]
+
 lemma exists_stdSimplex_of_mem_convexTail_reindexed {x g : ℕ → E} (hg : g ∈ convexTail x) (n : ℕ) :
   ∃ w : StdSimplex ℝ ℕ, g n = w.weights.sum (fun i wi ↦ wi • x i) ∧ ∀ m < n, w.weights m = 0 := by
   obtain ⟨w₀, hw₀⟩ := exists_stdSimplex_of_mem_convexHull (hg n)
@@ -235,7 +243,7 @@ lemma komlos_step {x : ℕ → ℕ → E} (hx : ∀ i : ℕ, ∃ M : ℝ, ∀ n,
   ∃ (cw_new : ℕ → ℕ → StdSimplex ℝ ℕ),
     (∃ glim : E, Tendsto (komlosFormula x cw_new (k+1) (k+1)) atTop (𝓝 glim))
     ∧ (∀ i ≤ k, cw_new i = cw i) ∧ (∀ n, ∀ m < n, (cw_new (k+1) n).weights m = 0) := by
-  let gtilde := fun n ↦ (iteratedBind cw k n).weights.sum (fun m cwm ↦ cwm • (x (k+1) m))
+  let gtilde := fun n ↦ (iteratedComb cw k n).weights.sum (fun m cwm ↦ cwm • (x (k+1) m))
   obtain ⟨M, hM⟩ := hx (k+1)
   have gtilde_bound : ∃ M, ∀ n, ‖gtilde n‖ ≤ M := ⟨M, convex_combination_bounded hM⟩
   obtain ⟨g_step, gstep_conv, glim, hglim⟩ := komlos_norm (gtilde_bound)
@@ -248,13 +256,13 @@ lemma komlos_step {x : ℕ → ℕ → E} (hx : ∀ i : ℕ, ∃ M : ℝ, ∀ n,
       (fun n ↦ (Classical.choose_spec (existence n)).1)⟩
   let cw_new := Function.update cw (k+1) cw_step
   have g_step_eq (n : ℕ) : g_step n =
-    (iteratedBind cw_new (k + 1) n).weights.sum (fun m cwm ↦ cwm • x (k+1) m) := by
-    have aux : (iteratedBind cw_new (k + 1) n)
-      = (bind (cw_step n) (iteratedBind cw k)) := by
+    (iteratedComb cw_new (k + 1) n).weights.sum (fun m cwm ↦ cwm • x (k+1) m) := by
+    have aux : (iteratedComb cw_new (k + 1) n)
+      = (iConvexComb (cw_step n) (iteratedComb cw k)) := by
       unfold cw_new
-      rw [iteratedBind, Function.update_self, iteratedBind_congr]
+      rw [iteratedComb, Function.update_self, iteratedComb_congr]
       grind
-    rw [g_step_eq_gtilde n, aux, ← bind_sum_smul]
+    rw [g_step_eq_gtilde n, aux, ← iConvexComb_sum_smul]
   use cw_new
   refine ⟨?_, by grind, ?_⟩
   · use glim; exact Tendsto.congr g_step_eq hglim
@@ -338,27 +346,124 @@ lemma TendstoUniformly_convexTail {x : ℕ → E} {xlim : E} (hx : Tendsto x atT
     simpa [dist_comm] using (convexHull_min htail (convex_ball xlim ε)) (y.2 n)
   simpa only [gt_iff_lt] using this
 
+lemma komlosFormula_convexTail_incr (x : ℕ → ℕ → E) (cw : ℕ → ℕ → StdSimplex ℝ ℕ) (i : ℕ) :
+    komlosFormula x cw (i + 1) i ∈ convexTail (komlosFormula x cw i i) := by
+  simp only [convexTail, Set.mem_setOf_eq, komlosFormula]
+  intro n
+  sorry
+
+lemma komlosFormula_convexTail (x : ℕ → ℕ → E) (cw : ℕ → ℕ → StdSimplex ℝ ℕ) (k i : ℕ)
+  (hk : i ≤ k) :
+  komlosFormula x cw k i ∈ convexTail (komlosFormula x cw i i) := by
+  let n := k - i
+  rw [(show k = i + n by grind)]
+  induction n with
+  | zero => simp only [add_zero]; exact convexTail_self (komlosFormula x cw i i)
+  | succ m hm => sorry
+
 omit [CompleteSpace E] in
-lemma Tendsto_convexTail {x : ℕ → E} {xlim : E} (hx : Tendsto x atTop (𝓝 xlim)) :
-    ∀ y ∈ convexTail x, Tendsto y atTop (𝓝 xlim) := by
-  intro y hy
-  exact TendstoUniformly.tendsto_at (TendstoUniformly_convexTail hx) ⟨y, hy⟩
+lemma TendstoUniformly_convexTail' {x : ℕ → E} {xlim : E} (hx : Tendsto x atTop (𝓝 xlim))
+    {y : ℕ → ℕ → E} (hy : ∀ᶠ i in atTop, (fun n ↦ y n i) ∈ convexTail x) :
+    TendstoUniformly y (fun _ ↦ xlim) atTop := by
+  intro u hu
+  rcases Metric.mem_uniformity_dist.mp hu with ⟨ε, εpos, hεu⟩
+  have hxε : ∀ᶠ n in atTop, dist (x n) xlim < ε := by
+    simpa using hx (Metric.ball_mem_nhds _ εpos)
+  rcases Filter.eventually_atTop.mp hxε with ⟨N, hN⟩
+  rcases Filter.eventually_atTop.mp hy with ⟨M, hM⟩
+  refine Filter.eventually_atTop.mpr ⟨max N M, ?_⟩
+  intro n hNM i
+  have hn : n ≥ N := by grind
+  apply hεu
+  simp only
+  clear hεu hu u
+
+  have htail : Set.range (fun m ↦ x (n + m)) ⊆ Metric.ball xlim ε := by
+    rintro _ ⟨m, rfl⟩
+    simpa using hN (n + m) (le_trans hn (Nat.le_add_right n m))
+
+  have aux : y n i ∈ Metric.ball xlim ε := by
+    sorry
+
+  simp only [gt_iff_lt]
+  exact Metric.mem_ball'.mp aux
 
 lemma komlos_uniform_convergence
     {x : ℕ → ℕ → E} (hx : ∀ i : ℕ, ∃ M : ℝ, ∀ n, ‖x i n‖ ≤ M)
     (cw : ℕ → ℕ → StdSimplex ℝ ℕ) (lim : ℕ → E)
     (hcw: ∀ k : ℕ, Tendsto (komlosFormula x cw k k) atTop (𝓝 (lim k))) :
-    ∀ i, TendstoUniformly (fun k ↦ komlosFormula x cw k i) lim atTop
-    -- maybe too strong, the blueprint statement limits to k ≥ i
+    ∀ i, TendstoUniformly (fun k ↦ komlosFormula x cw k i) (fun _ ↦ lim i) atTop
      := by
   intro i
+  apply TendstoUniformly_convexTail' (hcw i)
+  simp only [eventually_atTop]
+  use i -- check if this is right!
+  intro k hk
+  -- unfold komlosFormula
+  -- informal argument: to show convergence, it suffices to show convergence for k >= K with some
+  -- fix K. Let's consider K := i.
+  -- we want to rewrite `fun k ↦ komlosFormula x cw k i` in terms of convexTail
+  sorry
+
+lemma komlos_uniform_convergence_epsilon
+    {x : ℕ → ℕ → E} (hx : ∀ i : ℕ, ∃ M : ℝ, ∀ n, ‖x i n‖ ≤ M)
+    (cw : ℕ → ℕ → StdSimplex ℝ ℕ) (lim : ℕ → E)
+    (hcw: ∀ k : ℕ, Tendsto (komlosFormula x cw k k) atTop (𝓝 (lim k))) (i : ℕ) :
+    ∀ ε > 0, ∃ N, ∀ n ≥ N, ∀ k ≥ i, ‖komlosFormula x cw k i n - lim i‖ < ε
+     := by
+  intro ε hε
+  unfold komlosFormula
+  have (k : ℕ) (hk : i ≤ k) :
+    (komlosFormula x cw k i) ∈ convexTail (fun n ↦ komlosFormula x cw i i n)
+    := by -- WIP proof. Need the right lemmas on convexTail + komlosFormula
+    unfold komlosFormula
+    unfold convexTail
+    simp only [Set.mem_setOf_eq]
+    intro n
+    unfold convexHull
+    simp only [ClosureOperator.ofCompletePred_apply, Set.le_eq_subset, Set.iInf_eq_iInter,
+      Set.mem_iInter, Subtype.forall, and_imp]
+    intro s hsub hconv
+    sorry
   sorry
 
-lemma komlos_convex_weights_diagonal
-    {x : ℕ → ℕ → E} (hx : ∀ i : ℕ, ∃ M : ℝ, ∀ n, ‖x i n‖ ≤ M) :
+-- statement needs work!
+lemma weights_zero {cw : ℕ → ℕ → StdSimplex ℝ ℕ}
+    (h : ∀ (k n m : ℕ), m < n → (cw k n).weights m = 0) (k n m : ℕ) (hm : m < k) (hn : n ≤ k) :
+    (iteratedComb cw k n).weights m = 0 := by -- 2nd k needs generalisation
+  induction k with
+  | zero => grind
+  | succ k hk =>
+    simp [iteratedComb]
+    -- need to adjust the statement!
+    sorry
+
+lemma komlos_convex_weights_diagonal {x : ℕ → ℕ → E} (hx : ∀ i : ℕ, ∃ M : ℝ, ∀ n, ‖x i n‖ ≤ M) :
     ∃ (η : ℕ → StdSimplex ℝ ℕ), (∀ n, ∀ m < n, (η n).weights m = 0) ∧ ∀ i : ℕ,
     ∃ glim : E, Tendsto (fun n ↦ (η n).weights.sum (fun m ηm ↦ ηm • x i m)) atTop (𝓝 glim) := by
-  sorry
+  let ⟨cw, cwlim, cwnonneg⟩ := komlos_convex_weights hx
+  let g (i : ℕ) := Classical.choose (cwlim i)
+  have glim (i : ℕ) := Classical.choose_spec (cwlim i)
+  let η (n : ℕ) : StdSimplex ℝ ℕ := iteratedComb cw n n
+  have lim (i : ℕ) : Tendsto
+    (fun n ↦ (η n).weights.sum (fun m ηm ↦ ηm • x i m)) atTop (𝓝 (g i)) := by
+    apply Filter.tendsto_of_sub_tendsto_zero
+      (g := fun n ↦ (η n).weights.sum (fun m ηm ↦ ηm • x i m)) (f := fun n ↦ g i)
+    · simp
+    rw [NormedAddGroup.tendsto_nhds_zero]
+    intro ε hε
+    simp only [Pi.sub_apply, eventually_atTop]
+    have ⟨N, hN⟩ := komlos_uniform_convergence_epsilon hx cw g glim i ε hε
+    use max N i
+    intro k _
+    replace hN := hN k (by grind) k (by grind)
+    exact hN
+  use η
+  refine ⟨?_, ?_⟩
+  · intro n m hm
+    unfold η
+    sorry -- should be easy
+  · exact fun i ↦ Exists.intro (g i) (lim i)
 
 lemma komlos_convergence_L2
     (f : ℕ → Ω → E) {P : Measure Ω} :