PL1/LatticeAbsoluteContinuity.lean
All source files · Download exact source
SHA-256: fcd5270ca6446b1cfd2097113ca897cfce031bc3c7ac8baf4909c0a3a24d5cac
1import PL1.LatticeStrictPositive23/-!4# Uniform absolute continuity on order intervals56In a Schur Banach lattice, a strictly positive continuous functional controls7the norm uniformly on each fixed order interval. This uses actual monotone8norm convergence, rather than assuming compactness of the interval.9-/1011noncomputable section12open Filter TopologicalSpace Finset13open scoped Topology1415namespace PL1.SchurLattice1617variable {E : Type*} [NormedAddCommGroup E] [Lattice E]18 [IsOrderedAddMonoid E] [NormedVectorLattice E] [CompleteSpace E]1920private def partialSup (x : ℕ → E) : ℕ → E21 | 0 => 022 | n + 1 => partialSup x n ⊔ x n2324omit [IsOrderedAddMonoid E] [NormedVectorLattice E] [CompleteSpace E] in25private theorem partialSup_nonneg (x : ℕ → E) (n : ℕ) : 0 ≤ partialSup x n := by26 induction n with27 | zero => exact le_rfl28 | succ n hn => exact hn.trans le_sup_left2930omit [IsOrderedAddMonoid E] [NormedVectorLattice E] [CompleteSpace E] in31private theorem partialSup_le (x : ℕ → E) (u : E) (hu : 0 ≤ u)32 (hx : ∀ n, x n ≤ u) (n : ℕ) : partialSup x n ≤ u := by33 induction n with34 | zero => exact hu35 | succ n hn => exact sup_le hn (hx n)3637omit [IsOrderedAddMonoid E] [NormedVectorLattice E] [CompleteSpace E] in38private theorem partialSup_monotone (x : ℕ → E) : Monotone (partialSup x) :=39 monotone_nat_of_le_succ (fun _ => le_sup_left)4041/-- The supremum of a dominated positive sequence exists, and its value at42any positive functional is bounded by the sum of that functional's values. -/43theorem exists_isLUB_with_dual_bound (hS : HasSchurProperty ℝ E)44 (φ : E →L[ℝ] ℝ) (hφ : 0 ≤ φ) (x : ℕ → E) (u : E) (hu : 0 ≤ u)45 (hx : ∀ n, 0 ≤ x n ∧ x n ≤ u) (hsum : Summable (fun n => φ (x n))) :46 ∃ z : E, IsLUB (Set.range x) z ∧ 0 ≤ z ∧ z ≤ u ∧47 φ z ≤ ∑' n, φ (x n) := by48 have hpos := partialSup_nonneg x49 have hle := partialSup_le x u hu (fun n => (hx n).2)50 obtain ⟨z, hz⟩ := exists_tendsto_of_monotone_norm_bounded hS (partialSup x)51 (partialSup_monotone x) ‖u‖ (fun n => by52 apply norm_le_norm_of_abs_le_abs53 simpa only [abs_of_nonneg (hpos n), abs_of_nonneg hu] using hle n)54 have hz0 : 0 ≤ z := ge_of_tendsto' hz hpos55 have hzu : z ≤ u := le_of_tendsto' hz hle56 have hlub := isLUB_of_tendsto_atTop (partialSup_monotone x) hz57 have hzx (n : ℕ) : x n ≤ z :=58 le_sup_right.trans (hlub.1 (Set.mem_range_self (n + 1)))59 have hlubx : IsLUB (Set.range x) z := by60 refine ⟨?_, ?_⟩61 · rintro _ ⟨n, rfl⟩62 exact hzx n63 · intro b hb64 apply hlub.265 rintro _ ⟨n, rfl⟩66 exact partialSup_le x b ((hx 0).1.trans (hb (Set.mem_range_self 0)))67 (fun n => hb (Set.mem_range_self n)) n68 have hfinite (N : ℕ) : φ (partialSup x N) ≤ ∑ n ∈ range N, φ (x n) := by69 induction N with70 | zero => simp [partialSup]71 | succ N ih =>72 have hsuple : partialSup x N ⊔ x N ≤ partialSup x N + x N :=73 sup_le (le_add_of_nonneg_right (hx N).1) (le_add_of_nonneg_left (hpos N))74 calc75 φ (partialSup x (N + 1)) ≤ φ (partialSup x N + x N) :=76 StrongDual.apply_le_apply_of_nonneg hφ hsuple77 _ = φ (partialSup x N) + φ (x N) := map_add _ _ _78 _ ≤ (∑ n ∈ range N, φ (x n)) + φ (x N) := add_le_add ih le_rfl79 _ = ∑ n ∈ range (N + 1), φ (x n) := (sum_range_succ _ _).symm80 refine ⟨z, hlubx, hz0, hzu, ?_⟩81 exact le_of_tendsto' ((φ.continuous.tendsto z).comp hz) (fun N =>82 (hfinite N).trans (hsum.sum_le_tsum (range N) (fun n _ =>83 StrongDual.apply_nonneg_of_nonneg hφ (hx n).1)))8485/-- A dominated positive sequence whose values at a strictly positive86functional are summable converges to zero in the original norm. -/87theorem tendsto_zero_of_summable_strictlyPositive (hS : HasSchurProperty ℝ E)88 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ)89 (x : ℕ → E) (u : E) (hu : 0 ≤ u)90 (hx : ∀ n, 0 ≤ x n ∧ x n ≤ u) (hsum : Summable (fun n => φ (x n))) :91 Tendsto x atTop (𝓝 0) := by92 classical93 choose z hz using (fun N : ℕ =>94 exists_isLUB_with_dual_bound hS φ hφ.nonneg (fun n => x (n + N)) u hu95 (fun n => hx (n + N)) (hsum.comp_injective (add_left_injective N)))96 have hz0 (N : ℕ) : 0 ≤ z N := (hz N).2.197 have hzu (N : ℕ) : z N ≤ u := (hz N).2.2.198 have hanti : Antitone z := by99 intro N M hNM100 apply (hz M).1.2101 rintro _ ⟨n, rfl⟩102 exact (hz N).1.1 ⟨n + (M - N), by dsimp; rw [Nat.add_assoc, Nat.sub_add_cancel hNM]⟩103 obtain ⟨a, ha⟩ := exists_tendsto_of_antitone_norm_bounded hS z hanti ‖u‖ (by104 intro N105 apply norm_le_norm_of_abs_le_abs106 simpa only [abs_of_nonneg (hz0 N), abs_of_nonneg hu] using hzu N)107 have hφz : Tendsto (fun N => φ (z N)) atTop (𝓝 0) :=108 squeeze_zero (fun N => StrongDual.apply_nonneg_of_nonneg hφ.nonneg (hz0 N))109 (fun N => (hz N).2.2.2) (tendsto_sum_nat_add (fun n => φ (x n)))110 have hφa : φ a = 0 := tendsto_nhds_unique ((φ.continuous.tendsto a).comp ha) hφz111 have ha0 : a = 0 := hφ.eq_zero_of_nonneg (ge_of_tendsto' ha hz0) hφa112 subst a113 apply squeeze_zero_norm _ (by simpa only [norm_zero] using ha.norm)114 intro N115 apply norm_le_norm_of_abs_le_abs116 rw [abs_of_nonneg (hx N).1, abs_of_nonneg (hz0 N)]117 exact (hz N).1.1 ⟨0, by simp⟩118119/-- Uniform absolute continuity of the lattice norm on a fixed positive120order interval with respect to a strictly positive continuous functional. -/121theorem norm_lt_of_strictlyPositive_lt (hS : HasSchurProperty ℝ E)122 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) (u : E) (hu : 0 ≤ u)123 (ε : ℝ) (hε : 0 < ε) :124 ∃ δ : ℝ, 0 < δ ∧ ∀ x : E, 0 ≤ x → x ≤ u → φ x < δ → ‖x‖ < ε := by125 classical126 by_contra hbad127 push Not at hbad128 choose x hx0 hxu hφx hnorm using fun n : ℕ =>129 hbad ((1 / 2 : ℝ) ^ n) (by positivity)130 have hs : Summable (fun n => φ (x n)) :=131 (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num)).of_nonneg_of_le132 (fun n => StrongDual.apply_nonneg_of_nonneg hφ.nonneg (hx0 n))133 (fun n => (hφx n).le)134 have ht := (tendsto_zero_of_summable_strictlyPositive hS φ hφ x u hu135 (fun n => ⟨hx0 n, hxu n⟩) hs).norm136 obtain ⟨n, hn⟩ := (ht.eventually_lt_const (by simpa using hε)).exists137 exact (not_lt_of_ge (hnorm n)) hn138139/-- For dominated positive sequences, convergence to zero at one strictly140positive functional is equivalent to convergence in the original norm. -/141theorem tendsto_zero_iff_strictlyPositive (hS : HasSchurProperty ℝ E)142 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) (x : ℕ → E)143 (u : E) (hu : 0 ≤ u) (hx : ∀ n, 0 ≤ x n ∧ x n ≤ u) :144 Tendsto x atTop (𝓝 0) ↔ Tendsto (fun n => φ (x n)) atTop (𝓝 0) := by145 constructor146 · intro h147 rw [← map_zero φ]148 exact (φ.continuous.tendsto 0).comp h149 · intro h150 apply Metric.tendsto_atTop.mpr151 intro ε hε152 obtain ⟨δ, hδ, hcontrol⟩ := norm_lt_of_strictlyPositive_lt hS φ hφ u hu ε hε153 obtain ⟨N, hN⟩ := eventually_atTop.mp (h.eventually_lt_const hδ)154 refine ⟨N, fun n hn => ?_⟩155 simpa only [dist_zero_right] using hcontrol (x n) (hx n).1 (hx n).2 (hN n hn)156157end PL1.SchurLattice158