PL1/SchurExample.lean

All source files · Download exact source

SHA-256: a113cce8156eb5886d8331f4adc416a044f033b7d2ebc61b9a6970550683cee7

1import PL1.L1Truncation2import PL1.CompactWalshMultiplier3import PL1.DyadicSchur4import PL1.NonSchurExample56/-!7# The concrete infinite-dimensional Schur projection89Unbounded coordinate rates give compact L-infinity restrictions of the10concrete convolution resolvents. The fully proved L1 restriction criterion11makes these resolvents Dunford-Pettis, and the dyadic construction gives an12actual Schur range and a Dunford-Pettis projection with the paper's bound.13-/1415noncomputable section16open Filter MeasureTheory17open scoped Topology ENNReal NNReal1819namespace PL1.Noise2021variable (𝕜 : Type*) [RCLike 𝕜]2223/-- The actual Haar L1 convolution resolvent is Dunford-Pettis whenever the24coordinate rates diverge. No analytic compactness hypothesis remains. -/25theorem resolventL1_isDunfordPettis_of_rates_tendsto (rates : ℕ → ℝ≥0)26    (hRateTop : Tendsto (fun j => (rates j : ℝ)) cofinite atTop) (t : PositiveTime) :27    IsDunfordPettis (resolventL1 𝕜 rates t) :=28  L1Truncation.isDunfordPettis_of_compact_Linfty_restriction Walsh.haar _29    (WalshMultiplier.compact_resolventL1_restriction 𝕜 rates t hRateTop)3031theorem schurRates_resolventL1_isDunfordPettis (t : PositiveTime) :32    IsDunfordPettis (resolventL1 𝕜 schurRates t) :=33  resolventL1_isDunfordPettis_of_rates_tendsto 𝕜 schurRates34    WalshMultiplier.tendsto_schurRates t3536theorem intrinsic_hasSchurProperty_of_rates_tendsto (rates : ℕ → ℝ≥0)37    (hRateTop : Tendsto (fun j => (rates j : ℝ)) cofinite atTop) :38    HasSchurProperty 𝕜 (dyadicSystem 𝕜 rates).IntrinsicSpace :=39  (dyadicSystem 𝕜 rates).hasSchurProperty_intrinsic40    (fun n => resolventL1_isDunfordPettis_of_rates_tendsto 𝕜 rates hRateTop (dyadicTime n))4142theorem projection_range_hasSchurProperty_of_rates_tendsto (rates : ℕ → ℝ≥0)43    (hRateTop : Tendsto (fun j => (rates j : ℝ)) cofinite atTop) :44    HasSchurProperty 𝕜 (projection 𝕜 rates).range :=45  (dyadicSystem 𝕜 rates).hasSchurProperty_projection_range46    (fun n => resolventL1_isDunfordPettis_of_rates_tendsto 𝕜 rates hRateTop (dyadicTime n))4748theorem projection_isDunfordPettis_of_rates_tendsto (rates : ℕ → ℝ≥0)49    (hRateTop : Tendsto (fun j => (rates j : ℝ)) cofinite atTop) :50    IsDunfordPettis (projection 𝕜 rates) :=51  (dyadicSystem 𝕜 rates).projection_isDunfordPettis52    (fun n => resolventL1_isDunfordPettis_of_rates_tendsto 𝕜 rates hRateTop (dyadicTime n))5354theorem schurRates_intrinsic_hasSchurProperty :55    HasSchurProperty 𝕜 (dyadicSystem 𝕜 schurRates).IntrinsicSpace :=56  intrinsic_hasSchurProperty_of_rates_tendsto 𝕜 schurRates WalshMultiplier.tendsto_schurRates5758theorem schurRates_projection_range_hasSchurProperty :59    HasSchurProperty 𝕜 (projection 𝕜 schurRates).range :=60  projection_range_hasSchurProperty_of_rates_tendsto 𝕜 schurRates WalshMultiplier.tendsto_schurRates6162theorem schurRates_projection_isDunfordPettis :63    IsDunfordPettis (projection 𝕜 schurRates) :=64  projection_isDunfordPettis_of_rates_tendsto 𝕜 schurRates WalshMultiplier.tendsto_schurRates6566/-- The completely concrete Schur projection on the countable sum of Haar L167has infinite-dimensional closed range and the manuscript's quantitative bound. -/68theorem schurRates_projection_spec :69    IsProjection (projection 𝕜 schurRates) ∧70      ‖projection 𝕜 schurRates‖ ≤ projectionBound ∧71      IsClosed ((projection 𝕜 schurRates).range : Set (L1Sum (Lp 𝕜 1 Walsh.haar))) ∧72      ¬ FiniteDimensional 𝕜 (projection 𝕜 schurRates).range ∧73      HasSchurProperty 𝕜 (projection 𝕜 schurRates).range ∧74      IsDunfordPettis (projection 𝕜 schurRates) :=75  ⟨projection_isProjection 𝕜 schurRates, norm_projection_le 𝕜 schurRates,76    projection_range_isClosed 𝕜 schurRates, projection_range_infiniteDimensional 𝕜 schurRates,77    schurRates_projection_range_hasSchurProperty 𝕜, schurRates_projection_isDunfordPettis 𝕜⟩7879end PL1.Noise80