PL1/DyadicCoordinateDomination.lean

All source files · Download exact source

SHA-256: 1da8fc2acaf1f12dc7d34e683d5e186d631fc15b5664a932dc3a870d471490f0

1import Mathlib.Analysis.Normed.Group.Tannery2import Mathlib.Topology.Order.MonotoneConvergence3import Mathlib.Topology.Algebra.InfiniteSum.Real45/-! Uniform summable coordinate domination for increasing finite variations. -/67noncomputable section8open Filter9open scoped BigOperators Topology1011namespace PL1.DyadicCoordinateDomination1213theorem exists_summable_majorant (a : ℕ → ℕ → ℝ) (C : ℝ)14    (ha : ∀ m n, 0 ≤ a m n)15    (hmono : ∀ n, Monotone (fun m => a m n))16    (hbound : ∀ m (s : Finset ℕ), ∑ n ∈ s, a m n ≤ C) :17    ∃ b : ℕ → ℝ, Summable b ∧ (∀ n, 0 ≤ b n) ∧18      (∀ m n, a m n ≤ b n) ∧ ∑' n, b n ≤ C := by19  classical20  have hab (m n : ℕ) : a m n ≤ C := by21    simpa using hbound m {n}22  have hbdd (n : ℕ) : BddAbove (Set.range (fun m => a m n)) :=23    ⟨C, by rintro y ⟨m, rfl⟩; exact hab m n⟩24  let b : ℕ → ℝ := fun n => sSup (Set.range (fun m => a m n))25  have hle (m n : ℕ) : a m n ≤ b n := le_csSup (hbdd n) (Set.mem_range_self m)26  have hb (n : ℕ) : 0 ≤ b n := (ha 0 n).trans (hle 0 n)27  have ht (n : ℕ) : Tendsto (fun m => a m n) atTop (𝓝 (b n)) :=28    tendsto_atTop_ciSup (hmono n) (hbdd n)29  have hsum (s : Finset ℕ) : ∑ n ∈ s, b n ≤ C := by30    apply le_of_tendsto (tendsto_finsetSum s (fun n _ => ht n))31    exact Filter.Eventually.of_forall (fun m => hbound m s)32  have hs : Summable b := summable_of_sum_le hb hsum33  exact ⟨b, hs, hb, hle, hs.tsum_le_of_sum_le hsum⟩3435theorem tendsto_tsum_zero_of_increasing_majorants36    (a u : ℕ → ℕ → ℝ) (C : ℝ)37    (ha : ∀ m n, 0 ≤ a m n)38    (hmono : ∀ n, Monotone (fun m => a m n))39    (hbound : ∀ m (s : Finset ℕ), ∑ n ∈ s, a m n ≤ C)40    (hu : ∀ m n, 0 ≤ u m n) (hua : ∀ m n, u m n ≤ a m n)41    (ht : ∀ n, Tendsto (fun m => u m n) atTop (𝓝 0)) :42    Tendsto (fun m => ∑' n, u m n) atTop (𝓝 0) := by43  obtain ⟨b, hb, hb0, hab, _⟩ := exists_summable_majorant a C ha hmono hbound44  have hd (m n : ℕ) : ‖u m n‖ ≤ b n := by45    rw [Real.norm_eq_abs, abs_of_nonneg (hu m n)]46    exact (hua m n).trans (hab m n)47  simpa only [tsum_zero] using tendsto_tsum_of_dominated_convergence hb ht48    (Filter.Eventually.of_forall (fun m n => hd m n))4950end PL1.DyadicCoordinateDomination51