PL1/SchurLattice.lean
All source files · Download exact source
SHA-256: 4de48bcbfb9a508dabe6b02196dc2c1e68e3bbd11da5177d2f7236f4e9732f3e
1import PL1.SchurBoundedCompleteness2import BanLat.Disjoint3import BanLat.OrderComplete45/-!6# Order-bounded disjoint sequences in Schur lattices78This proves the first step of the paper's Schur-lattice lemma. It does not9assert the full structural Radon-Nikodym theorem for Schur Banach lattices.10-/1112noncomputable section13open Filter Finset14open scoped Topology1516namespace PL1.SchurLattice1718variable {E : Type*} [NormedAddCommGroup E] [Lattice E]19 [IsOrderedAddMonoid E] [NormedVectorLattice E]2021/-- The lattice absolute value of every signed finite sum stays below the22common order bound of a pairwise disjoint sequence. -/23theorem abs_signed_sum_le (x : ℕ → E)24 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))25 (u : E) (hbound : ∀ n, |x n| ≤ u)26 (N : ℕ) (ε : ℕ → ℝ) (hε : ∀ n, ε n = 1 ∨ ε n = -1) :27 |∑ n ∈ Finset.range N, ε n • x n| ≤ u := by28 classical29 have hu : 0 ≤ u := (abs_nonneg (x 0)).trans (hbound 0)30 by_cases hN : N = 031 · subst N32 simpa using hu33 have hd : Pairwise (fun i j : Fin N => IsVLDisjoint (x i) (x j)) := by34 intro i j hij35 exact hdisj (fun h => hij (Fin.ext h))36 have hdabs : Pairwise (fun i j : Fin N => IsVLDisjoint |x i| |x j|) := by37 intro i j hij38 simpa only [IsVLDisjoint, abs_abs] using hd hij39 have hsign (i : Fin N) : |ε i| = 1 := by40 rcases hε i with hi | hi <;> simp [hi]41 have hfin : |∑ i : Fin N, ε i • x i| ≤ u := by42 rw [abs_sum_of_pairwise_isVLDisjoint hd]43 simp only [hsign, one_smul]44 rw [sum_eq_sup_of_pairwise_isVLDisjoint_of_nonneg (Nat.pos_of_ne_zero hN)45 (fun i : Fin N => abs_nonneg (x i)) hdabs]46 exact Finset.sup'_le _ _ (fun i _ => hbound i)47 rw [← Fin.sum_univ_eq_sum_range (fun n => ε n • x n)]48 exact hfin4950/-- Uniform norm bound for all signed partial sums, with no factor depending51on the number of terms. -/52theorem norm_signed_sum_le (x : ℕ → E)53 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))54 (u : E) (hbound : ∀ n, |x n| ≤ u)55 (N : ℕ) (ε : ℕ → ℝ) (hε : ∀ n, ε n = 1 ∨ ε n = -1) :56 ‖∑ n ∈ Finset.range N, ε n • x n‖ ≤ ‖u‖ :=57 norm_le_norm_of_abs_le_abs ((abs_signed_sum_le x hdisj u hbound N ε hε).trans (le_abs_self u))5859/-- Every continuous real functional is absolutely summable on an order-bounded,60pairwise lattice-disjoint sequence. -/61theorem dual_summable_norm (x : ℕ → E)62 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))63 (u : E) (hbound : ∀ n, |x n| ≤ u) (φ : E →L[ℝ] ℝ) :64 Summable (fun n => ‖φ (x n)‖) :=65 SchurBoundedCompleteness.dual_summable_norm_of_signed_sums_bounded66 x ‖u‖ (norm_signed_sum_le x hdisj u hbound) φ6768/-- An order-bounded disjoint sequence is weakly null, whether or not the69ambient normed lattice has the Schur property. -/70theorem weaklyConverges_zero (x : ℕ → E)71 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))72 (u : E) (hbound : ∀ n, |x n| ≤ u) : WeaklyConverges ℝ E x 0 :=73 SchurBoundedCompleteness.weaklyConverges_zero_of_signed_sums_bounded74 x ‖u‖ (norm_signed_sum_le x hdisj u hbound)7576/-- Consequently every order-bounded disjoint sequence in a Schur normed77lattice tends to zero in norm. -/78theorem tendsto_zero (hS : HasSchurProperty ℝ E) (x : ℕ → E)79 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))80 (u : E) (hbound : ∀ n, |x n| ≤ u) : Tendsto x atTop (𝓝 0) :=81 hS x 0 (weaklyConverges_zero x hdisj u hbound)8283theorem tendsto_norm_zero (hS : HasSchurProperty ℝ E) (x : ℕ → E)84 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))85 (u : E) (hbound : ∀ n, |x n| ≤ u) :86 Tendsto (fun n => ‖x n‖) atTop (𝓝 0) := by87 simpa only [norm_zero] using (tendsto_zero hS x hdisj u hbound).norm8889/-- In the complete case the same sequence is unconditionally summable;90the conclusion uses all finite subsets, not just initial partial sums. -/91theorem summable [CompleteSpace E] (hS : HasSchurProperty ℝ E) (x : ℕ → E)92 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))93 (u : E) (hbound : ∀ n, |x n| ≤ u) : Summable x :=94 SchurBoundedCompleteness.summable_of_signed_sums_bounded hS x ‖u‖95 (norm_signed_sum_le x hdisj u hbound)9697omit [NormedVectorLattice E] in98/-- An arbitrary common order interval supplies an absolute order bound. -/99theorem abs_le_of_mem_Icc {a b z : E} (hz : z ∈ Set.Icc a b) :100 |z| ≤ |a| ⊔ |b| := by101 rw [abs]102 exact sup_le (hz.2.trans ((le_abs_self b).trans le_sup_right))103 ((neg_le_neg hz.1).trans ((neg_le_abs a).trans le_sup_left))104105theorem weaklyConverges_zero_of_mem_Icc (x : ℕ → E)106 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))107 (a b : E) (hbound : ∀ n, x n ∈ Set.Icc a b) : WeaklyConverges ℝ E x 0 :=108 weaklyConverges_zero x hdisj (|a| ⊔ |b|) (fun n => abs_le_of_mem_Icc (hbound n))109110theorem tendsto_norm_zero_of_mem_Icc (hS : HasSchurProperty ℝ E) (x : ℕ → E)111 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))112 (a b : E) (hbound : ∀ n, x n ∈ Set.Icc a b) :113 Tendsto (fun n => ‖x n‖) atTop (𝓝 0) :=114 tendsto_norm_zero hS x hdisj (|a| ⊔ |b|) (fun n => abs_le_of_mem_Icc (hbound n))115116/-- Disjoint expansions have an exact unconditional norm identity. -/117theorem norm_signed_sum_eq (x : ℕ → E)118 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))119 (N : ℕ) (ε : ℕ → ℝ) (hε : ∀ n, ε n = 1 ∨ ε n = -1) :120 ‖∑ n ∈ Finset.range N, ε n • x n‖ = ‖∑ n ∈ Finset.range N, x n‖ := by121 classical122 have hd : Pairwise (fun i j : Fin N => IsVLDisjoint (x i) (x j)) := by123 intro i j hij124 exact hdisj (fun h => hij (Fin.ext h))125 have hsign (i : Fin N) : |ε i| = 1 := by126 rcases hε i with hi | hi <;> simp [hi]127 have hsigned : |∑ i : Fin N, ε i • x i| = ∑ i : Fin N, |x i| := by128 rw [abs_sum_of_pairwise_isVLDisjoint hd]129 simp only [hsign, one_smul]130 have hplain : |∑ i : Fin N, x i| = ∑ i : Fin N, |x i| := by131 simpa only [one_smul, abs_one] using132 (abs_sum_of_pairwise_isVLDisjoint (α := fun _ => (1 : ℝ)) hd)133 rw [← Fin.sum_univ_eq_sum_range (fun n => ε n • x n),134 ← Fin.sum_univ_eq_sum_range x]135 rw [← norm_abs_eq_norm (∑ i : Fin N, ε i • x i),136 ← norm_abs_eq_norm (∑ i : Fin N, x i), hsigned, hplain]137138/-- Every disjoint expansion with norm-bounded ordinary partial sums is139unconditionally summable in a Schur Banach lattice. -/140theorem summable_of_partialSums_bounded [CompleteSpace E]141 (hS : HasSchurProperty ℝ E) (x : ℕ → E)142 (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))143 (M : ℝ) (hM : ∀ N, ‖∑ n ∈ Finset.range N, x n‖ ≤ M) : Summable x := by144 apply SchurBoundedCompleteness.summable_of_signed_sums_bounded hS x M145 intro N ε hε146 rw [norm_signed_sum_eq x hdisj N ε hε]147 exact hM N148149/-- Positive expansions also have uniformly bounded sign transformations. -/150theorem norm_signed_sum_le_of_nonneg (x : ℕ → E) (hx : ∀ n, 0 ≤ x n)151 (N : ℕ) (ε : ℕ → ℝ) (hε : ∀ n, ε n = 1 ∨ ε n = -1) :152 ‖∑ n ∈ Finset.range N, ε n • x n‖ ≤ ‖∑ n ∈ Finset.range N, x n‖ := by153 classical154 apply norm_le_norm_of_abs_le_abs155 rw [abs_of_nonneg (Finset.sum_nonneg (fun n _ => hx n)), abs]156 apply sup_le157 · apply Finset.sum_le_sum158 intro n hn159 rcases hε n with he | he160 · simp only [he, one_smul, le_refl]161 · simpa only [he, neg_smul, one_smul] using (neg_nonpos.mpr (hx n)).trans (hx n)162 · rw [← Finset.sum_neg_distrib]163 apply Finset.sum_le_sum164 intro n hn165 rcases hε n with he | he166 · simpa only [he, one_smul] using (neg_nonpos.mpr (hx n)).trans (hx n)167 · simp only [he, neg_smul, one_smul, neg_neg, le_refl]168169/-- A positive series with bounded partial sums is unconditionally summable170in a Schur Banach lattice. -/171theorem summable_of_nonneg_partialSums_bounded [CompleteSpace E]172 (hS : HasSchurProperty ℝ E) (x : ℕ → E) (hx : ∀ n, 0 ≤ x n)173 (M : ℝ) (hM : ∀ N, ‖∑ n ∈ Finset.range N, x n‖ ≤ M) : Summable x := by174 apply SchurBoundedCompleteness.summable_of_signed_sums_bounded hS x M175 intro N ε hε176 exact (norm_signed_sum_le_of_nonneg x hx N ε hε).trans (hM N)177178/-- Every norm-bounded increasing sequence in a Schur Banach lattice converges179in norm. This includes the usual KB property for positive increasing sequences. -/180theorem exists_tendsto_of_monotone_norm_bounded [CompleteSpace E]181 (hS : HasSchurProperty ℝ E) (x : ℕ → E) (hmono : Monotone x)182 (M : ℝ) (hM : ∀ n, ‖x n‖ ≤ M) : ∃ a : E, Tendsto x atTop (𝓝 a) := by183 let d : ℕ → E := fun n => x (n + 1) - x n184 have hd : ∀ n, 0 ≤ d n := fun n => sub_nonneg.mpr (hmono (Nat.le_succ n))185 have hsum (N : ℕ) : (∑ n ∈ Finset.range N, d n) = x N - x 0 :=186 Finset.sum_range_sub x N187 have hb : ∀ N, ‖∑ n ∈ Finset.range N, d n‖ ≤ M + ‖x 0‖ := by188 intro N189 rw [hsum]190 exact (norm_sub_le _ _).trans (add_le_add (hM N) le_rfl)191 have hs := summable_of_nonneg_partialSums_bounded hS d hd (M + ‖x 0‖) hb192 refine ⟨(∑' n, d n) + x 0, ?_⟩193 simpa only [hsum, sub_add_cancel] using hs.hasSum.tendsto_sum_nat.add_const (x 0)194195/-- The decreasing formulation of monotone convergence. -/196theorem exists_tendsto_of_antitone_norm_bounded [CompleteSpace E]197 (hS : HasSchurProperty ℝ E) (x : ℕ → E) (hanti : Antitone x)198 (M : ℝ) (hM : ∀ n, ‖x n‖ ≤ M) : ∃ a : E, Tendsto x atTop (𝓝 a) := by199 obtain ⟨a, ha⟩ := exists_tendsto_of_monotone_norm_bounded hS (fun n => -x n)200 (fun i j hij => neg_le_neg (hanti hij)) M (fun n => by simpa using hM n)201 exact ⟨-a, by simpa only [neg_neg] using ha.neg⟩202203/-- Sequential order continuity: a decreasing positive sequence with greatest204lower bound zero is norm null in a Schur Banach lattice. -/205theorem tendsto_zero_of_antitone_isGLB [CompleteSpace E]206 (hS : HasSchurProperty ℝ E) (x : ℕ → E) (hanti : Antitone x)207 (hglb : IsGLB (Set.range x) 0) : Tendsto x atTop (𝓝 0) := by208 have hx : ∀ n, 0 ≤ x n := fun n => hglb.1 (Set.mem_range_self n)209 obtain ⟨a, ha⟩ := exists_tendsto_of_antitone_norm_bounded hS x hanti ‖x 0‖ (by210 intro n211 apply norm_le_norm_of_abs_le_abs212 simpa only [abs_of_nonneg (hx n), abs_of_nonneg (hx 0)] using hanti (Nat.zero_le n))213 have heq : a = 0 := (isGLB_of_tendsto_atTop hanti ha).unique hglb214 exact heq ▸ ha215216private theorem cauchy_map_atTop_of_near_base {ι Y : Type*}217 [Preorder ι] [IsDirectedOrder ι] [Nonempty ι] [PseudoMetricSpace Y]218 (x : ι → Y)219 (h : ∀ ε : ℝ, 0 < ε → ∃ i, ∀ j, i ≤ j → dist (x j) (x i) < ε) :220 Cauchy (Filter.map x atTop) := by221 rw [Metric.cauchy_iff]222 refine ⟨inferInstance, fun ε hε => ?_⟩223 obtain ⟨i, hi⟩ := h (ε / 2) (half_pos hε)224 refine ⟨x '' Set.Ici i, Filter.image_mem_map (Ici_mem_atTop i), ?_⟩225 rintro _ ⟨j, hj, rfl⟩ _ ⟨k, hk, rfl⟩226 have hj' := hi j hj227 have hk' := hi k hk228 have ht := dist_triangle (x j) (x i) (x k)229 rw [dist_comm (x i) (x k)] at ht230 linarith231232/-- The KB convergence property holds for arbitrary directed nets as well as233sequences: a failure of the Cauchy condition would give a divergent monotone234sequence by recursive index selection. -/235theorem exists_tendsto_of_monotone_net_norm_bounded [CompleteSpace E]236 {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]237 (hS : HasSchurProperty ℝ E) (x : ι → E) (hmono : Monotone x)238 (M : ℝ) (hM : ∀ i, ‖x i‖ ≤ M) : ∃ a : E, Tendsto x atTop (𝓝 a) := by239 classical240 apply cauchy_map_iff_exists_tendsto.mp241 by_contra hbad242 have hfail : ¬ (∀ ε : ℝ, 0 < ε → ∃ i, ∀ j, i ≤ j → dist (x j) (x i) < ε) :=243 fun h => hbad (cauchy_map_atTop_of_near_base x h)244 push Not at hfail245 obtain ⟨ε, hε, hfail⟩ := hfail246 choose next hnext hdist using hfail247 let i : ℕ → ι := fun n => next^[n] (Classical.choice ‹Nonempty ι›)248 have hi (n : ℕ) : i (n + 1) = next (i n) := Function.iterate_succ_apply' _ _ _249 have hinc : Monotone i := monotone_nat_of_le_succ (fun n => by rw [hi]; exact hnext _)250 obtain ⟨a, ha⟩ := exists_tendsto_of_monotone_norm_bounded hS (fun n => x (i n))251 (hmono.comp hinc) M (fun n => hM _)252 obtain ⟨N, hN⟩ := Metric.cauchySeq_iff.mp ha.cauchySeq ε hε253 have hclose := hN (N + 1) (Nat.le_succ N) N le_rfl254 rw [hi] at hclose255 exact (not_lt_of_ge (hdist (i N))) hclose256257theorem exists_tendsto_of_antitone_net_norm_bounded [CompleteSpace E]258 {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]259 (hS : HasSchurProperty ℝ E) (x : ι → E) (hanti : Antitone x)260 (M : ℝ) (hM : ∀ i, ‖x i‖ ≤ M) : ∃ a : E, Tendsto x atTop (𝓝 a) := by261 obtain ⟨a, ha⟩ := exists_tendsto_of_monotone_net_norm_bounded hS (fun i => -x i)262 (fun i j hij => neg_le_neg (hanti hij)) M (fun i => by simpa using hM i)263 exact ⟨-a, by simpa only [neg_neg] using ha.neg⟩264265/-- Full norm order continuity, stated explicitly for every decreasing net266whose greatest lower bound is zero. -/267theorem tendsto_zero_of_antitone_net_isGLB [CompleteSpace E]268 {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]269 (hS : HasSchurProperty ℝ E) (x : ι → E) (hanti : Antitone x)270 (hglb : IsGLB (Set.range x) 0) : Tendsto x atTop (𝓝 0) := by271 classical272 let i₀ : ι := Classical.choice ‹Nonempty ι›273 let : Nonempty (Set.Ici i₀) := ⟨⟨i₀, le_rfl⟩⟩274 let : IsDirectedOrder (Set.Ici i₀) := ⟨fun i j => by275 obtain ⟨k, hik, hjk⟩ := exists_ge_ge (i : ι) (j : ι)276 exact ⟨⟨k, i.prop.trans hik⟩, hik, hjk⟩⟩277 let y : Set.Ici i₀ → E := fun i => x i278 have hy : Antitone y := fun i j hij => hanti hij279 have hx : ∀ i, 0 ≤ x i := fun i => hglb.1 (Set.mem_range_self i)280 obtain ⟨a, ha⟩ := exists_tendsto_of_antitone_net_norm_bounded hS y hy ‖x i₀‖ (by281 intro i282 apply norm_le_norm_of_abs_le_abs283 simpa only [y, abs_of_nonneg (hx i), abs_of_nonneg (hx i₀)] using hanti i.prop)284 have htail : Tendsto x atTop (𝓝 a) := tendsto_comp_val_Ici_atTop.mp ha285 have heq : a = 0 := (isGLB_of_tendsto_atTop hanti htail).unique hglb286 exact heq ▸ htail287288/-- A Schur Banach lattice is Dedekind complete. The construction extends the289given lattice structure; it does not replace its order or norm. -/290@[reducible]291def conditionallyCompleteLattice [CompleteSpace E] (hS : HasSchurProperty ℝ E) :292 ConditionallyCompleteLattice E :=293 conditionallyCompleteLatticeOfPosNet E (by294 intro ι _ _ _ x hmono hx hbdd295 obtain ⟨b, hb⟩ := hbdd296 obtain ⟨a, ha⟩ := exists_tendsto_of_monotone_net_norm_bounded hS x hmono ‖b‖ (by297 intro i298 apply norm_le_norm_of_abs_le_abs299 rw [abs_of_nonneg (hx i)]300 exact (hb (Set.mem_range_self i)).trans (le_abs_self b))301 exact ⟨a, isLUB_of_tendsto_atTop hmono ha⟩)302303/-- Explicit coherence with the pre-existing lattice instance. -/304theorem conditionallyCompleteLattice_toLattice [CompleteSpace E]305 (hS : HasSchurProperty ℝ E) :306 (conditionallyCompleteLattice hS).toLattice = (inferInstance : Lattice E) := rfl307308theorem exists_isLUB [CompleteSpace E] (hS : HasSchurProperty ℝ E)309 (s : Set E) (hne : s.Nonempty) (hbdd : BddAbove s) : ∃ a, IsLUB s a := by310 let := conditionallyCompleteLattice hS311 exact ⟨sSup s, isLUB_csSup hne hbdd⟩312313end PL1.SchurLattice314