PL1/DyadicSchur.lean

All source files · Download exact source

SHA-256: ccedb3a6d5a1307ffbec5bc51e1de9b894129d2ff0087ceb6f24cd7c125016ca

1import PL1.DyadicProjection2import PL1.DunfordPettis3import PL1.SchurApproximation45/-!6# The Schur conclusion from Dunford–Pettis resolvents78On the intrinsic graph, smoothing approximates the underlying-vector map in9operator norm. Hence Dunford–Pettis resolvents imply that map is DP. The full10countable ell1 gliding-hump argument then proves the intrinsic space Schur.11The DP property of the concrete Haar L1 resolvents remains to be discharged12by the measure-theoretic compact-restriction criterion.13-/1415noncomputable section16open Filter17open scoped Topology1819namespace PL1.DyadicSystem2021open ResolventEstimates IntrinsicGraph2223variable {𝕜 Y : Type*} [RCLike 𝕜]24  [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [CompleteSpace Y]2526variable (S : DyadicSystem 𝕜 Y)2728omit [CompleteSpace Y] in29theorem norm_coordinate_le (n : ℕ) (x : S.IntrinsicSpace) :30    ‖coord S.analysis n x‖ ≤ ‖x‖ :=31  lp.norm_apply_le_norm (by simp) (x : L1Sum Y) n3233omit [CompleteSpace Y] in34theorem norm_smoothing_error_apply_le (n : ℕ) (x : S.IntrinsicSpace) :35    ‖S.operator (n + 1) (evalZero S.analysis x) - evalZero S.analysis x‖ ≤36      dyadicRatio ^ (n + 1) * ‖x‖ := by37  have hc : (dyadicRatio ^ (n + 1))⁻¹ *38      ‖evalZero S.analysis x - S.operator (n + 1) (evalZero S.analysis x)‖ ≤ ‖x‖ := by39    have hn := S.norm_coordinate_le (n + 1) x40    rw [coord_eq] at hn41    simpa only [analysis, analysisCoordinate, smul_apply, sub_apply,42      ContinuousLinearMap.id_apply, norm_smul, RCLike.norm_ofReal,43      abs_of_nonneg (inv_nonneg.mpr (pow_nonneg dyadicRatio_nonneg _))] using hn44  have hmul := mul_le_mul_of_nonneg_left hc (pow_nonneg dyadicRatio_nonneg (n + 1))45  rw [← mul_assoc, mul_inv_cancel₀ (dyadicRatio_pow_ne_zero _), one_mul] at hmul46  simpa only [norm_sub_rev] using hmul4748omit [CompleteSpace Y] in49theorem norm_smoothing_error_le (n : ℕ) :50    ‖(S.operator (n + 1)).comp (evalZero S.analysis) - evalZero S.analysis‖ ≤51      dyadicRatio ^ (n + 1) :=52  ContinuousLinearMap.opNorm_le_bound _ (pow_nonneg dyadicRatio_nonneg _)53    (S.norm_smoothing_error_apply_le n)5455set_option backward.isDefEq.respectTransparency false in56theorem smoothing_evalZero_tendsto :57    Tendsto (fun n => (S.operator (n + 1)).comp (evalZero S.analysis))58      atTop (𝓝 (evalZero S.analysis)) := by59  refine (@Metric.tendsto_atTop (S.IntrinsicSpace →L[𝕜] Y) ℕ60    inferInstance inferInstance inferInstance61    (fun n => (S.operator (n + 1)).comp (evalZero S.analysis))62    (evalZero S.analysis)).mpr ?_63  intro ε hε64  have hp : Tendsto (fun n : ℕ => dyadicRatio ^ (n + 1)) atTop (𝓝 0) :=65    (tendsto_pow_atTop_nhds_zero_of_lt_one dyadicRatio_nonneg dyadicRatio_lt_one).comp66      (tendsto_add_atTop_nat 1)67  obtain ⟨N, hN⟩ := eventually_atTop.mp (hp.eventually (gt_mem_nhds hε))68  refine ⟨N, fun n hn => ?_⟩69  rw [show dist ((S.operator (n + 1)).comp (evalZero S.analysis)) (evalZero S.analysis) =70    ‖(S.operator (n + 1)).comp (evalZero S.analysis) - evalZero S.analysis‖ from71    @dist_eq_norm (S.IntrinsicSpace →L[𝕜] Y) inferInstance72      ((S.operator (n + 1)).comp (evalZero S.analysis)) (evalZero S.analysis)]73  exact (S.norm_smoothing_error_le n).trans_lt (hN n hn)7475theorem evalZero_isDunfordPettis (hS : ∀ n, IsDunfordPettis (S.operator n)) :76    IsDunfordPettis (evalZero S.analysis) :=77  isDunfordPettis_of_tendsto (fun n => (hS (n + 1)).comp_right (evalZero S.analysis))78    S.smoothing_evalZero_tendsto7980theorem hasSchurProperty_intrinsic (hS : ∀ n, IsDunfordPettis (S.operator n)) :81    HasSchurProperty 𝕜 S.IntrinsicSpace :=82  (IntrinsicGraph.hasSchurProperty_iff_evalZero_isDunfordPettis S.analysis).mpr83    (S.evalZero_isDunfordPettis hS)8485theorem hasSchurProperty_projection_range (hS : ∀ n, IsDunfordPettis (S.operator n)) :86    HasSchurProperty 𝕜 S.projection.range := by87  rw [S.projection_range]88  exact S.hasSchurProperty_intrinsic hS8990theorem projection_isDunfordPettis (hS : ∀ n, IsDunfordPettis (S.operator n)) :91    IsDunfordPettis S.projection :=92  isDunfordPettis_of_hasSchurProperty_range _ (S.hasSchurProperty_projection_range hS)9394end PL1.DyadicSystem95