PL1/IntervalSumming.lean

All source files · Download exact source

SHA-256: 40cba9454c48c465b67e3f35b4124a7b550db8f4e23e0751612ed5231d5ccae0

1import PL1.FiniteGrothendieck2import PL1.SummingTransport3import PL1.IntervalDyadicApproximation4import PL1.DyadicL1Coordinates56/-! Stability of summing estimates under pointwise norm convergence. -/7noncomputable section8open scoped BigOperators9open Filter10namespace PL1.ComplementedLattice1112section PointwiseLimits13variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]14  [NormedAddCommGroup F] [NormedSpace ℝ F]1516theorem OneSummingWith.of_pointwise_tendsto (T : ℕ → E →L[ℝ] F)17    (S : E →L[ℝ] F) (C : ℝ) (hT : ∀ m, OneSummingWith (T m) C)18    (hlim : ∀ x, Tendsto (fun m => T m x) atTop (nhds (S x))) : OneSummingWith S C := by19  refine ⟨(hT 0).1, ?_⟩20  intro n x M hx21  apply le_of_tendsto' (tendsto_finsetSum Finset.univ (fun i _ => (hlim (x i)).norm))22  exact fun m => (hT m).2 n x M hx2324theorem TwoSummingWith.of_pointwise_tendsto (T : ℕ → E →L[ℝ] F)25    (S : E →L[ℝ] F) (C : ℝ) (hT : ∀ m, TwoSummingWith (T m) C)26    (hlim : ∀ x, Tendsto (fun m => T m x) atTop (nhds (S x))) : TwoSummingWith S C := by27  refine ⟨(hT 0).1, ?_⟩28  intro n x M hM hx29  apply le_of_tendsto' (tendsto_finsetSum Finset.univ (fun i _ => ((hlim (x i)).norm).pow 2))30  exact fun m => (hT m).2 n x M hM hx3132end PointwiseLimits33end PL1.ComplementedLattice3435namespace PL1.IntervalSumming36open PL1.DyadicTrace PL1.DyadicL1Coordinates PL1.FiniteSumming PL1.ComplementedLattice3738theorem oneSumming_interval (k : ℕ) (S : IntervalL1 ℝ →L[ℝ] EuclideanSpace ℝ (Fin k)) :39    OneSummingWith S (128 * ‖S‖) := by40  let T := fun m => (S.comp (synthesis m)).comp (analysis m)41  apply OneSummingWith.of_pointwise_tendsto T S (128 * ‖S‖)42  · intro m43    have ht := (oneSumming_128 (2 ^ m) k (S.comp (synthesis m))).precomp (analysis m)44    apply ht.mono45    have hc : ‖S.comp (synthesis m)‖ ≤ ‖S‖ :=46      (ContinuousLinearMap.opNorm_comp_le _ _).trans (by47        simpa only [mul_one] using mul_le_mul_of_nonneg_left48          (norm_synthesis_le_one m) (norm_nonneg S))49    calc50      _ ≤ (128 * ‖S‖) * ‖analysis m‖ := mul_le_mul_of_nonneg_right51        (mul_le_mul_of_nonneg_left hc (by norm_num)) (norm_nonneg _)52      _ ≤ (128 * ‖S‖) * 1 := mul_le_mul_of_nonneg_left (norm_analysis_le_one m) (by positivity)53      _ = _ := mul_one _54  · intro x55    have h := (S.continuous.tendsto x).comp (dyadicAverage_tendsto x)56    simpa only [T, ContinuousLinearMap.comp_apply, synthesis_analysis, Function.comp_def] using h5758theorem twoSumming_interval (d : ℕ) (S : (Fin d → ℝ) →L[ℝ] IntervalL1 ℝ) :59    TwoSummingWith S (128 * ‖S‖) := by60  let T := fun m => (synthesis m).comp ((analysis m).comp S)61  apply TwoSummingWith.of_pointwise_tendsto T S (128 * ‖S‖)62  · intro m63    have ht := (twoSumming_128 d (2 ^ m) ((analysis m).comp S)).postcomp (synthesis m)64    apply ht.mono65    have hc : ‖(analysis m).comp S‖ ≤ ‖S‖ :=66      (ContinuousLinearMap.opNorm_comp_le _ _).trans (by67        simpa only [one_mul] using mul_le_mul_of_nonneg_right68          (norm_analysis_le_one m) (norm_nonneg S))69    calc70      _ ≤ ‖synthesis m‖ * (128 * ‖S‖) := mul_le_mul_of_nonneg_left71        (mul_le_mul_of_nonneg_left hc (by norm_num)) (norm_nonneg _)72      _ ≤ 1 * (128 * ‖S‖) := mul_le_mul_of_nonneg_right (norm_synthesis_le_one m) (by positivity)73      _ = _ := one_mul _74  · intro x75    simpa only [T, ContinuousLinearMap.comp_apply, synthesis_analysis] using dyadicAverage_tendsto (S x)7677#print axioms oneSumming_interval78#print axioms twoSumming_interval79end PL1.IntervalSumming80818283