PL1/L1Sum.lean

All source files · Download exact source

SHA-256: afc43b97f2a472e70af1f0ea3d498321276771f3368782eb64e84b9f90524f90

1import PL1.Definitions2import Mathlib.Analysis.Normed.Operator.Basic34/-!5# Operators defined by uniformly bounded columns on an actual ell1 sum67This is a general analytic construction used for K and the matrix projection.8The columns are supplied as continuous linear maps; their uniform bound is9an explicit hypothesis, to be discharged by the dyadic resolvent estimates.10-/1112noncomputable section13open Filter14open scoped Topology ENNReal1516namespace PL11718abbrev L1Sum (Y : Type*) [NormedAddCommGroup Y] := lp (fun _ : ℕ => Y) 11920namespace L1Sum2122variable {𝕜 Y Z : Type*} [RCLike 𝕜]23  [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]24  [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] [CompleteSpace Z]2526theorem summable_norm (x : L1Sum Y) : Summable (fun n => ‖x n‖) := by27  simpa using (lp.memℓp x).summable (by simp : (0 : ℝ) < (1 : ℝ≥0∞).toReal)2829theorem norm_eq_tsum (x : L1Sum Y) : ‖x‖ = ∑' n, ‖x n‖ := by30  simpa using lp.norm_eq_tsum_rpow (by simp : (0 : ℝ) < (1 : ℝ≥0∞).toReal) x3132variable (T : ℕ → Y →L[𝕜] Z) (C : ℝ) (hT : ∀ n, ‖T n‖ ≤ C)3334include hT3536omit [CompleteSpace Z] in37theorem column_norm_le (x : L1Sum Y) (n : ℕ) :38    ‖T n (x n)‖ ≤ C * ‖x n‖ :=39  (T n).le_opNorm (x n) |>.trans40    (mul_le_mul_of_nonneg_right (hT n) (norm_nonneg _))4142theorem summable_norm_columns (x : L1Sum Y) :43    Summable (fun n => ‖T n (x n)‖) :=44  Summable.of_nonneg_of_le (fun _ => norm_nonneg _) (column_norm_le T C hT x)45    ((summable_norm x).mul_left C)4647theorem summable_columns (x : L1Sum Y) :48    Summable (fun n => T n (x n)) :=49  (summable_norm_columns T C hT x).of_norm5051theorem norm_tsum_columns_le (x : L1Sum Y) :52    ‖∑' n, T n (x n)‖ ≤ C * ‖x‖ := by53  calc54    ‖∑' n, T n (x n)‖ ≤ ∑' n, ‖T n (x n)‖ :=55      norm_tsum_le_tsum_norm (summable_norm_columns T C hT x)56    _ ≤ ∑' n, C * ‖x n‖ :=57      Summable.tsum_le_tsum (column_norm_le T C hT x)58        (summable_norm_columns T C hT x) ((summable_norm x).mul_left C)59    _ = C * ‖x‖ := by rw [tsum_mul_left, norm_eq_tsum]6061/-- Synthesis of an ell1 input by uniformly bounded operator columns. -/62def synthesis : L1Sum Y →L[𝕜] Z :=63  LinearMap.mkContinuous64    { toFun := fun x => ∑' n, T n (x n)65      map_add' := by66        intro x y67        simp only [lp.coeFn_add, Pi.add_apply, map_add]68        exact (summable_columns T C hT x).tsum_add (summable_columns T C hT y)69      map_smul' := by70        intro c x71        simp only [lp.coeFn_smul, Pi.smul_apply, map_smul, RingHom.id_apply]72        exact (summable_columns T C hT x).tsum_const_smul c }73    C (norm_tsum_columns_le T C hT)7475@[simp]76theorem synthesis_apply (x : L1Sum Y) :77    synthesis T C hT x = ∑' n, T n (x n) := rfl7879theorem norm_synthesis_le (hC : 0 ≤ C) : ‖synthesis T C hT‖ ≤ C :=80  ContinuousLinearMap.opNorm_le_bound _ hC (norm_tsum_columns_le T C hT)8182@[simp]83theorem synthesis_single (j : ℕ) (y : Y) :84    synthesis T C hT (lp.single 1 j y) = T j y := by85  rw [synthesis_apply, tsum_eq_single j]86  · simp87  · intro n hn88    simp [Pi.single_eq_of_ne hn]8990end L1Sum91end PL192