PL1/UnconditionalDecomposition.lean

All source files · Download exact source

SHA-256: dec11808fdc9fcb01de5a4195db733b9cdbc7fadb2a826833e31deae16b065e6

1import PL1.SchurBoundedCompleteness23/-! # Bounded completeness from unconditional sign bounds in Schur spaces -/45noncomputable section6open Filter7open scoped Topology BigOperators89namespace PL1.UnconditionalDecomposition1011variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]1213/-- The constant block followed by successive differences of partial-sum projections. -/14def difference (P : ℕ → E →L[ℝ] E) : ℕ → E →L[ℝ] E15  | 0 => P 016  | n + 1 => P (n + 1) - P n1718/-- Differences of a coherent branch, including its initial vector. -/19def branchDifference (x : ℕ → E) : ℕ → E20  | 0 => x 021  | n + 1 => x (n + 1) - x n2223theorem difference_branch (P : ℕ → E →L[ℝ] E) (x : ℕ → E)24    (hx : ∀ m n, m ≤ n → P m (x n) = x m)25    (N j : ℕ) (hj : j ≤ N) : difference P j (x N) = branchDifference x j := by26  cases j with27  | zero => exact hx 0 N (Nat.zero_le _)28  | succ j =>29    simp only [difference, branchDifference, sub_apply, hx (j + 1) N hj,30      hx j N (Nat.le_trans (Nat.le_succ j) hj)]3132omit [NormedSpace ℝ E] in33theorem sum_branchDifference (x : ℕ → E) (N : ℕ) :34    (∑ j ∈ Finset.range (N + 1), branchDifference x j) = x N := by35  induction N with36  | zero => simp [branchDifference]37  | succ N ih =>38    rw [Finset.sum_range_succ, ih, branchDifference]39    abel4041/-- A bounded coherent branch has bounded signed sums of its successive differences. -/42theorem signedSumsBounded_branchDifference43    (P : ℕ → E →L[ℝ] E) (C : ℝ) (hC : 0 ≤ C)44    (htransform : ∀ (N : ℕ) (ε : ℕ → ℝ) (y : E),45      (∀ j, ε j = 1 ∨ ε j = -1) →46        ‖∑ j ∈ Finset.range (N + 1), ε j • difference P j y‖ ≤ C * ‖y‖)47    (x : ℕ → E) (hx : ∀ m n, m ≤ n → P m (x n) = x m)48    (M : ℝ) (hM : ∀ n, ‖x n‖ ≤ M) :49    SchurBoundedCompleteness.SignedSumsBounded (branchDifference x) (C * M) := by50  intro N ε hε51  cases N with52  | zero =>53    have hM0 : 0 ≤ M := (norm_nonneg (x 0)).trans (hM 0)54    simpa using mul_nonneg hC hM055  | succ N =>56    calc57      _ = ‖∑ j ∈ Finset.range (N + 1), ε j • difference P j (x N)‖ := by58        congr 159        apply Finset.sum_congr rfl60        intro j hj61        rw [difference_branch P x hx N j (by have := Finset.mem_range.mp hj; omega)]62      _ ≤ C * ‖x N‖ := htransform N ε (x N) hε63      _ ≤ C * M := mul_le_mul_of_nonneg_left (hM N) hC6465/-- In a complete real Schur space, a uniform unconditional sign bound forces every66bounded coherent branch of partial-sum projections to converge in norm. -/67theorem bounded_branch_converges [CompleteSpace E]68    (hS : HasSchurProperty ℝ E)69    (P : ℕ → E →L[ℝ] E) (C : ℝ) (hC : 0 ≤ C)70    (htransform : ∀ (N : ℕ) (ε : ℕ → ℝ) (y : E),71      (∀ j, ε j = 1 ∨ ε j = -1) →72        ‖∑ j ∈ Finset.range (N + 1), ε j • difference P j y‖ ≤ C * ‖y‖)73    (x : ℕ → E) (hx : ∀ m n, m ≤ n → P m (x n) = x m)74    (hbounded : ∃ M : ℝ, ∀ n, ‖x n‖ ≤ M) :75    ∃ a : E, Tendsto x atTop (𝓝 a) := by76  obtain ⟨M, hM⟩ := hbounded77  obtain ⟨a, ha⟩ := SchurBoundedCompleteness.exists_tendsto_partialSums_of_signed_sums_bounded78    hS (branchDifference x) (C * M)79      (signedSumsBounded_branchDifference P C hC htransform x hx M hM)80  refine ⟨a, ?_⟩81  have h := ha.comp (tendsto_add_atTop_nat 1)82  simpa only [Function.comp_def, sum_branchDifference] using h8384end PL1.UnconditionalDecomposition85