PL1/ConcreteResolvents.lean
All source files · Download exact source
SHA-256: 69f3544dd93d94b5493ae5b8a1fce4a55d6a0c28026704fd9146b38833c7ae9c
1import PL1.NoiseMeasures2import PL1.ExponentialTime3import PL1.ConvolutionL14import PL1.StrongConvergence5import PL1.DyadicProjection6import Mathlib.Probability.Kernel.Composition.IntegralCompProd78/-!9# Concrete convolution resolvents and their dyadic projection1011The resolvent measure is the exponential average of the actual product-noise12kernel. Its L1 operator is the genuine probability convolution constructed13on equivalence classes. The scalar multiplier formula, contraction bound,14commutation, resolvent identity, and density supply all the dyadic-system15hypotheses. No resolvent or projection existence is assumed here.16-/1718noncomputable section19open MeasureTheory ProbabilityTheory Filter20open scoped Topology NNReal ENNReal BigOperators2122namespace PL1.Noise2324open Walsh ExponentialTime ResolventEstimates2526def resolventMeasure (rates : ℕ → ℝ≥0) (t : ℝ) : Measure Walsh.Group :=27 kernel rates ∘ₘ timeMeasure t2829theorem isProbabilityMeasure_resolventMeasure (rates : ℕ → ℝ≥0) {t : ℝ} (ht : 0 < t) :30 IsProbabilityMeasure (resolventMeasure rates t) := by31 let := isProbabilityMeasure_timeMeasure ht32 unfold resolventMeasure33 infer_instance3435/-- Fourier multipliers of the genuine exponentially averaged noise measure. -/36theorem integral_character_resolventMeasure (rates : ℕ → ℝ≥0)37 {t : ℝ} (ht : 0 < t) (F : Finset ℕ) :38 ∫ x, character F x ∂resolventMeasure rates t = (1 + t * rateSum rates F)⁻¹ := by39 let := isProbabilityMeasure_timeMeasure ht40 let := isProbabilityMeasure_resolventMeasure rates ht41 have hi : Integrable (character F) (resolventMeasure rates t) :=42 Integrable.of_bound (continuous_character F).aestronglyMeasurable 143 (ae_of_all _ (fun x => (norm_character F x).le))44 have havg : (∫ x, character F x ∂resolventMeasure rates t) =45 ∫ u, ∫ x, character F x ∂measure rates u ∂timeMeasure t := by46 change Integrable (character F) ((kernel rates ∘ₖ Kernel.const Unit (timeMeasure t)) ()) at hi47 change (∫ x, character F x ∂((kernel rates ∘ₖ Kernel.const Unit (timeMeasure t)) ())) = _48 simpa only [Kernel.const_apply, kernel_apply] using ProbabilityTheory.Kernel.integral_comp hi49 rw [havg]50 simp only [integral_character]51 exact integral_laplace ht _ (rateSum_nonneg rates F)5253abbrev PositiveTime := {t : ℝ // 0 < t}5455/-- Resolvent convolution on the actual Haar L1 space, over either scalar field. -/56def resolventL1 (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0) (t : PositiveTime) :57 Lp 𝕜 1 haar →L[𝕜] Lp 𝕜 1 haar := by58 letI := isProbabilityMeasure_resolventMeasure rates t.property59 exact convolutionL1 (resolventMeasure rates t)6061variable (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0)6263theorem norm_resolventL1_le_one (t : PositiveTime) : ‖resolventL1 𝕜 rates t‖ ≤ 1 := by64 let := isProbabilityMeasure_resolventMeasure rates t.property65 exact norm_convolutionL1_le_one _6667@[simp]68theorem resolventL1_scalarCharacter (t : PositiveTime) (F : Finset ℕ) :69 resolventL1 𝕜 rates t (scalarCharacterLp 𝕜 1 F) =70 (((1 + (t : ℝ) * rateSum rates F)⁻¹ : ℝ) : 𝕜) • scalarCharacterLp 𝕜 1 F := by71 let := isProbabilityMeasure_resolventMeasure rates t.property72 change convolutionL1 _ _ = _73 rw [convolutionL1_scalarCharacter]74 congr 275 exact integral_character_resolventMeasure rates t.property F7677theorem resolventL1_commute (s t : PositiveTime) :78 (resolventL1 𝕜 rates s).comp (resolventL1 𝕜 rates t) =79 (resolventL1 𝕜 rates t).comp (resolventL1 𝕜 rates s) := by80 apply continuousLinearMap_ext_on_scalarCharacterL181 intro F82 simp only [ContinuousLinearMap.comp_apply, resolventL1_scalarCharacter,83 map_smul, smul_smul, mul_comm]8485theorem resolventL1_identity (s t : PositiveTime) :86 (ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 haar) - resolventL1 𝕜 rates s).comp87 (resolventL1 𝕜 rates t) =88 (((s : ℝ) / (t : ℝ) : ℝ) : 𝕜) • (resolventL1 𝕜 rates s).comp89 (ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 haar) - resolventL1 𝕜 rates t) := by90 apply continuousLinearMap_ext_on_scalarCharacterL191 intro F92 have hscalar := scalar_resolvent_identity s.property t.property (rateSum_nonneg rates F)93 simp only [ContinuousLinearMap.comp_apply, sub_apply,94 ContinuousLinearMap.id_apply, smul_apply,95 resolventL1_scalarCharacter, map_sub, map_smul]96 calc97 _ = ((1 - (((1 + (s : ℝ) * rateSum rates F)⁻¹ : ℝ) : 𝕜)) *98 (((1 + (t : ℝ) * rateSum rates F)⁻¹ : ℝ) : 𝕜)) •99 scalarCharacterLp 𝕜 1 F := by module100 _ = ((((s : ℝ) / (t : ℝ) : ℝ) : 𝕜) *101 (((1 + (s : ℝ) * rateSum rates F)⁻¹ : ℝ) : 𝕜) *102 (1 - (((1 + (t : ℝ) * rateSum rates F)⁻¹ : ℝ) : 𝕜))) •103 scalarCharacterLp 𝕜 1 F := by104 congr 1105 exact_mod_cast hscalar106 _ = _ := by module107108def dyadicTime (n : ℕ) : PositiveTime :=109 ⟨(dyadicRatio ^ 2) ^ n, pow_pos (pow_pos dyadicRatio_pos 2) n⟩110111theorem tendsto_dyadicTime :112 Tendsto (fun n => (dyadicTime n : ℝ)) atTop (𝓝 0) := by113 apply tendsto_pow_atTop_nhds_zero_of_lt_one (sq_nonneg _)114 rw [dyadicRatio_sq]115 norm_num116117theorem dyadic_resolvent_strong (f : Lp 𝕜 1 haar) :118 Tendsto (fun n => resolventL1 𝕜 rates (dyadicTime n) f) atTop (𝓝 f) := by119 apply tendsto_apply_of_dense_span (scalarCharacterLp 𝕜 1)120 (dense_span_scalarCharacterLp 𝕜 1 (by norm_num))121 (fun n => resolventL1 𝕜 rates (dyadicTime n))122 (ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 haar)) atTop 1123 (fun n => norm_resolventL1_le_one 𝕜 rates (dyadicTime n))124 intro F125 have hreal : Tendsto (fun n => (1 + (dyadicTime n : ℝ) * rateSum rates F)⁻¹)126 atTop (𝓝 (1 : ℝ)) := by127 simpa using ((tendsto_dyadicTime.mul_const (rateSum rates F)).const_add 1).inv₀ (by norm_num)128 have hcast := ((RCLike.continuous_ofReal : Continuous (fun x : ℝ => (x : 𝕜))).tendsto129 (1 : ℝ)).comp hreal130 change Tendsto (fun n => (((1 + (dyadicTime n : ℝ) * rateSum rates F)⁻¹ : ℝ) : 𝕜))131 atTop (𝓝 ((1 : ℝ) : 𝕜)) at hcast132 simpa only [resolventL1_scalarCharacter, RCLike.ofReal_one,133 one_smul, ContinuousLinearMap.id_apply] using hcast.smul_const (scalarCharacterLp 𝕜 1 F)134135/-- Every nonnegative rate sequence gives a concrete dyadic system on Haar L1. -/136def dyadicSystem : DyadicSystem 𝕜 (Lp 𝕜 1 haar) where137 operator n := resolventL1 𝕜 rates (dyadicTime n)138 contractive n := norm_resolventL1_le_one 𝕜 rates (dyadicTime n)139 commute i j := resolventL1_commute 𝕜 rates (dyadicTime i) (dyadicTime j)140 resolvent i j := resolventL1_identity 𝕜 rates (dyadicTime i) (dyadicTime j)141 strong := dyadic_resolvent_strong 𝕜 rates142143/-- The actual projection for the specified rates, on the ell1 sum of Haar L1. -/144def projection : L1Sum (Lp 𝕜 1 haar) →L[𝕜] L1Sum (Lp 𝕜 1 haar) :=145 (dyadicSystem 𝕜 rates).projection146147theorem projection_isProjection : IsProjection (projection 𝕜 rates) :=148 (dyadicSystem 𝕜 rates).isProjection149150theorem norm_projection_le : ‖projection 𝕜 rates‖ ≤ projectionBound :=151 (dyadicSystem 𝕜 rates).norm_projection_le152153theorem projection_range_isClosed :154 IsClosed ((projection 𝕜 rates).range : Set (L1Sum (Lp 𝕜 1 haar))) :=155 (dyadicSystem 𝕜 rates).isClosed_projection_range156157end PL1.Noise158