PL1/ConstantNoiseTrace.lean

All source files · Download exact source

SHA-256: 0b3899956c5411c1192c6fef495b2b1e83cf49cf98640ccdfff2de5e23cb2c0e

1import PL1.NoiseTraceObstruction2import PL1.NoiseHypercontractivity3import PL1.PartialMainTheorems45/-!6# Unconditional trace and factorization obstructions for the actual example78The sharp hypercontractivity theorem supplies every smoothing premise.9Consequently these conclusions about the actual constant-rate projection10have no unproved operator-theoretic hypotheses. Excluding all L1 subspaces11still requires the separate subspace-to-complemented-subspace argument.12-/1314noncomputable section15open MeasureTheory Filter16open scoped Topology ENNReal NNReal1718namespace PL1.Noise19open Walsh NoiseHypercontractivity2021def traceCutoff (m : ℕ) : ℝ≥0 := ⟨(dyadicTime m : ℝ), (dyadicTime m).property.le⟩2223theorem traceCutoff_pos (m : ℕ) : 0 < traceCutoff m := (dyadicTime m).property2425theorem tendsto_traceCutoff :26    Tendsto (fun m => (traceCutoff m : ℝ)) atTop (𝓝 0) := tendsto_dyadicTime2728variable (𝕜 : Type*) [RCLike 𝕜]2930theorem constant_resolvent_hasVanishingDyadicTrace (t : PositiveTime) :31    HasVanishingDyadicTrace (resolventL1 𝕜 constantRates t) := by32  apply resolvent_hasVanishingDyadicTrace_of_noise_smoothing 𝕜 constantRates t33    traceCutoff tendsto_traceCutoff (fun m => exponent (traceCutoff m))34    (fun m => exponent_lt_two _ (traceCutoff_pos m))35    (fun m => positiveTimeNoiseL2 𝕜 (traceCutoff m))36  intro m g f hgf37  rw [positiveTimeNoiseL2_overlap]38  congr 139  apply Lp.ext40  exact hgf.trans (ProbabilityLp.coeFn_inclusion haar 1 (exponent (traceCutoff m))41    (exponent_ge_one _) f).symm4243theorem constant_projection_hasVanishingDyadicTrace :44    HasVanishingDyadicTrace (projection 𝕜 constantRates) :=45  projection_hasVanishingDyadicTrace_of_resolvents 𝕜 constantRates46    (constant_resolvent_hasVanishingDyadicTrace 𝕜)4748theorem constant_projection_identity_distance49    (A : L1Sum (Lp 𝕜 1 haar) →L[𝕜] IntervalL1 𝕜)50    (B : IntervalL1 𝕜 →L[𝕜] L1Sum (Lp 𝕜 1 haar)) :51    1 ≤ ‖DyadicTrace.restrictLinfty (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) -52      A.comp ((projection 𝕜 constantRates).comp B))‖ :=53  (constant_projection_hasVanishingDyadicTrace 𝕜).one_le_norm_id_sub A B5455theorem constant_projection_not_factors_identity56    (A : L1Sum (Lp 𝕜 1 haar) →L[𝕜] IntervalL1 𝕜)57    (B : IntervalL1 𝕜 →L[𝕜] L1Sum (Lp 𝕜 1 haar)) :58    A.comp ((projection 𝕜 constantRates).comp B) ≠59      ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) :=60  (constant_projection_hasVanishingDyadicTrace 𝕜).not_factors_identity A B6162theorem constant_intervalProjection_hasVanishingDyadicTrace :63    HasVanishingDyadicTrace (intervalProjection 𝕜 constantRates) :=64  ((constant_projection_hasVanishingDyadicTrace 𝕜).comp_right65    (IntervalWalsh.walshSumContractiveRetract 𝕜).retraction).comp_left66      (IntervalWalsh.walshSumContractiveRetract 𝕜).embedding.toContinuousLinearMap6768theorem constant_intervalProjection_identity_distance69    (A B : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) :70    1 ≤ ‖DyadicTrace.restrictLinfty (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) -71      A.comp ((intervalProjection 𝕜 constantRates).comp B))‖ :=72  (constant_intervalProjection_hasVanishingDyadicTrace 𝕜).one_le_norm_id_sub A B7374theorem constant_intervalProjection_not_factors_identity75    (A B : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) :76    A.comp ((intervalProjection 𝕜 constantRates).comp B) ≠77      ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) :=78  (constant_intervalProjection_hasVanishingDyadicTrace 𝕜).not_factors_identity A B7980end PL1.Noise81