PL1/LatticeRademacherWeak.lean
All source files · Download exact source
SHA-256: b8ea8430f7c78cec7fe4919ff5676bf5f348d1f6c813fb815a0586624337f92b
1import PL1.LatticeRademacher23/-!4# Weak nullness from finite Rademacher square estimates56The estimate is required on every finite family of distinct indices.7Consequently the proof tests convergence against every continuous functional,8not merely a selected countable norming family.9-/1011noncomputable section12open Filter TopologicalSpace Finset13open scoped Topology1415namespace PL1.SchurLattice1617variable {E : Type*} [NormedAddCommGroup E] [Lattice E]18 [IsOrderedAddMonoid E] [NormedVectorLattice E]1920/-- Signed averages always contain a positive number of terms. -/21def signedAverage (r : ℕ → E) (q : ℕ → ℕ) (ε : ℕ → ℝ) (N : ℕ) : E :=22 ((N + 1 : ℕ) : ℝ)⁻¹ • ∑ i : Fin (N + 1), ε i • r (q i)2324theorem abs_signedAverage_le (r : ℕ → E) (u : E)25 (hr : ∀ n, |r n| ≤ u) (q : ℕ → ℕ) (ε : ℕ → ℝ)26 (hε : ∀ n, ε n = 1 ∨ ε n = -1) (N : ℕ) :27 |signedAverage r q ε N| ≤ u := by28 classical29 have hu : 0 ≤ u := (abs_nonneg (r 0)).trans (hr 0)30 have hterm (i : Fin (N + 1)) : |ε i • r (q i)| ≤ u := by31 rw [abs_smul']32 rcases hε i with h | h <;> simpa [h] using hr (q i)33 have hsum : |∑ i : Fin (N + 1), ε i • r (q i)| ≤34 ((N + 1 : ℕ) : ℝ) • u := by35 rw [abs]36 have heq : (∑ _ : Fin (N + 1), u) = ((N + 1 : ℕ) : ℝ) • u := by37 simp [← Nat.cast_smul_eq_nsmul ℝ]38 rw [← heq]39 apply sup_le40 · exact sum_le_sum (fun i _ => (le_abs_self _).trans (hterm i))41 · rw [← sum_neg_distrib]42 exact sum_le_sum (fun i _ => (neg_le_abs _).trans (hterm i))43 have hN : (0 : ℝ) < (N + 1 : ℕ) := by positivity44 rw [signedAverage, abs_smul', abs_of_nonneg (inv_nonneg.mpr hN.le)]45 simpa only [inv_smul_smul₀ hN.ne'] using46 smul_le_smul_of_nonneg_left hsum (inv_nonneg.mpr hN.le)4748/-- All finite signed square bounds, including every subsequence. -/49def HasRademacherSquareBound (φ : E →L[ℝ] ℝ) (u : E) (r : ℕ → E) : Prop :=50 ∀ (N : ℕ) (q : Fin N → ℕ), Function.Injective q →51 ∀ ε : Fin N → ℝ, (∀ i, ε i = 1 ∨ ε i = -1) →52 (φ |∑ i, ε i • r (q i)|) ^ 2 ≤ (φ u) ^ 2 * N5354/-- Normalizing the finite square estimate makes the positive functional55of the absolute signed average tend to zero. -/56theorem tendsto_dual_abs_signedAverage (φ : E →L[ℝ] ℝ) (hφ : 0 ≤ φ)57 (u : E) (r : ℕ → E) (hsq : HasRademacherSquareBound φ u r)58 (q : ℕ → ℕ) (hq : Function.Injective q) (ε : ℕ → ℝ)59 (hε : ∀ n, ε n = 1 ∨ ε n = -1) :60 Tendsto (fun N => φ |signedAverage r q ε N|) atTop (𝓝 0) := by61 have hN (N : ℕ) : (0 : ℝ) < (N + 1 : ℕ) := by positivity62 have hbound (N : ℕ) : (φ |signedAverage r q ε N|) ^ 2 ≤63 (φ u) ^ 2 * ((N + 1 : ℕ) : ℝ)⁻¹ := by64 have h := hsq (N + 1) (fun i => q i)65 (fun i j hij => Fin.ext (hq hij)) (fun i => ε i) (fun i => hε i)66 rw [signedAverage, abs_smul', abs_of_nonneg (inv_nonneg.mpr (hN N).le),67 map_smul, smul_eq_mul, mul_pow]68 calc69 _ ≤ (((N + 1 : ℕ) : ℝ)⁻¹) ^ 2 * ((φ u) ^ 2 * (N + 1 : ℕ)) :=70 mul_le_mul_of_nonneg_left h (sq_nonneg _)71 _ = _ := by field_simp72 have hinv : Tendsto (fun N : ℕ => ((N + 1 : ℕ) : ℝ)⁻¹) atTop (𝓝 0) :=73 tendsto_inv_atTop_zero.comp (tendsto_natCast_atTop_atTop.comp (tendsto_add_atTop_nat 1))74 have hsquares : Tendsto (fun N => (φ |signedAverage r q ε N|) ^ 2) atTop (𝓝 0) :=75 squeeze_zero (fun _ => sq_nonneg _) hbound (by simpa using hinv.const_mul ((φ u) ^ 2))76 have h := Real.continuous_sqrt.continuousAt.tendsto.comp hsquares77 convert h using 178 · funext N79 exact (Real.sqrt_sq (StrongDual.apply_nonneg_of_nonneg hφ (abs_nonneg _))).symm80 · simp8182/-- In a Schur Banach lattice, the finite square bound forces all signed83averages along every injective subsequence to tend to zero in norm. -/84theorem tendsto_signedAverage [CompleteSpace E] (hS : HasSchurProperty ℝ E)85 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) (u : E) (r : ℕ → E)86 (hr : ∀ n, |r n| ≤ u) (hsq : HasRademacherSquareBound φ u r)87 (q : ℕ → ℕ) (hq : Function.Injective q) (ε : ℕ → ℝ)88 (hε : ∀ n, ε n = 1 ∨ ε n = -1) :89 Tendsto (signedAverage r q ε) atTop (𝓝 0) := by90 have h := (tendsto_zero_iff_strictlyPositive hS φ hφ91 (fun N => |signedAverage r q ε N|) u ((abs_nonneg (r 0)).trans (hr 0))92 (fun N => ⟨abs_nonneg _, abs_signedAverage_le r u hr q ε hε N⟩)).mpr93 (tendsto_dual_abs_signedAverage φ hφ.nonneg u r hsq q hq ε hε)94 apply tendsto_zero_iff_norm_tendsto_zero.mpr95 simpa only [norm_abs_eq_norm, norm_zero] using h.norm9697/-- Vanishing signed averages along all injective subsequences imply weak98nullness against the entire real continuous dual. -/99theorem weaklyConverges_zero_of_signedAverage (r : ℕ → E)100 (havg : ∀ (q : ℕ → ℕ), Function.Injective q →101 ∀ ε : ℕ → ℝ, (∀ n, ε n = 1 ∨ ε n = -1) →102 Tendsto (signedAverage r q ε) atTop (𝓝 0)) : WeaklyConverges ℝ E r 0 := by103 classical104 intro ψ105 rw [map_zero]106 by_contra hbad107 rw [Metric.tendsto_atTop] at hbad108 push Not at hbad109 obtain ⟨δ, hδ, hbad⟩ := hbad110 choose k hk hkδ using hbad111 let next : ℕ → ℕ := fun n => k (n + 1)112 let q : ℕ → ℕ := fun n => next^[n] (k 0)113 have hqstep (n : ℕ) : q (n + 1) = k (q n + 1) := Function.iterate_succ_apply' _ _ _114 have hq : StrictMono q := strictMono_nat_of_lt_succ (fun n => by115 rw [hqstep]116 exact (Nat.lt_succ_self _).trans_le (hk _))117 have hqδ (n : ℕ) : δ ≤ |ψ (r (q n))| := by118 cases n with119 | zero => simpa [q, Real.dist_eq] using hkδ 0120 | succ n => simpa only [hqstep, Real.dist_eq, sub_zero] using hkδ (q n + 1)121 let ε : ℕ → ℝ := fun n => if 0 ≤ ψ (r (q n)) then 1 else -1122 have hε (n : ℕ) : ε n = 1 ∨ ε n = -1 := by dsimp [ε]; split <;> simp123 have heq (n : ℕ) : ε n * ψ (r (q n)) = |ψ (r (q n))| := by124 by_cases h : 0 ≤ ψ (r (q n))125 · simp [ε, h, abs_of_nonneg h]126 · simp [ε, h, abs_of_neg (lt_of_not_ge h)]127 have havgδ (N : ℕ) : δ ≤ ψ (signedAverage r q ε N) := by128 have hN : (0 : ℝ) < (N + 1 : ℕ) := by positivity129 have hs : ((N + 1 : ℕ) : ℝ) * δ ≤ ∑ i : Fin (N + 1), |ψ (r (q i))| := by130 simpa using sum_le_sum (s := (univ : Finset (Fin (N + 1)))) (fun i _ => hqδ i)131 rw [signedAverage, map_smul, smul_eq_mul, map_sum]132 simp_rw [map_smul, smul_eq_mul, heq]133 have h := mul_le_mul_of_nonneg_left hs (inv_nonneg.mpr hN.le)134 simpa only [← mul_assoc, inv_mul_cancel₀ hN.ne', one_mul] using h135 have ht : Tendsto (fun N => ψ (signedAverage r q ε N)) atTop (𝓝 0) := by136 rw [← map_zero ψ]137 exact (ψ.continuous.tendsto 0).comp (havg q hq.injective ε hε)138 obtain ⟨N, hN⟩ := (ht.eventually_lt_const hδ).exists139 exact (not_lt_of_ge (havgδ N)) hN140141/-- Actual square estimates for all distinct finite index families imply142weak nullness in a Schur Banach lattice. -/143theorem weaklyConverges_zero_of_rademacherSquareBound [CompleteSpace E]144 (hS : HasSchurProperty ℝ E) (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ)145 (u : E) (r : ℕ → E) (hr : ∀ n, |r n| ≤ u)146 (hsq : HasRademacherSquareBound φ u r) : WeaklyConverges ℝ E r 0 :=147 weaklyConverges_zero_of_signedAverage r148 (tendsto_signedAverage hS φ hφ u r hr hsq)149150/-- A nonzero constant-modulus Rademacher system contradicts the Schur151property once its finite square estimates have been established. -/152theorem eq_zero_of_constant_abs_rademacherSquareBound [CompleteSpace E]153 (hS : HasSchurProperty ℝ E) (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ)154 (u : E) (r : ℕ → E) (hr : ∀ n, |r n| = u)155 (hsq : HasRademacherSquareBound φ u r) : u = 0 := by156 have h := hS r 0 (weaklyConverges_zero_of_rademacherSquareBound hS φ hφ u r157 (fun n => (hr n).le) hsq)158 have hnorm (n : ℕ) : ‖r n‖ = ‖u‖ := by rw [← norm_abs_eq_norm (r n), hr n]159 have hn : Tendsto (fun _ : ℕ => ‖u‖) atTop (𝓝 0) := by160 simpa only [hnorm, norm_zero] using h.norm161 exact norm_eq_zero.mp (tendsto_nhds_unique tendsto_const_nhds hn)162163end PL1.SchurLattice164