PL1/NoiseSemigroup.lean

All source files · Download exact source

SHA-256: 4fe36d0f7841a376d9decfc76c29a65c57a03bf52c5684355cfab0df3c5d374a

1import PL1.ConcreteResolvents23/-! # The genuine strongly continuous noise semigroup and full resolvent limit -/45noncomputable section6open Filter MeasureTheory7open scoped Topology NNReal ENNReal89namespace PL1.Noise10open Walsh1112variable (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0)1314def noiseL1 (u : ℝ≥0) : Lp 𝕜 1 haar →L[𝕜] Lp 𝕜 1 haar :=15  convolutionL1 (measure rates u)1617theorem norm_noiseL1_le_one (u : ℝ≥0) : ‖noiseL1 𝕜 rates u‖ ≤ 1 :=18  norm_convolutionL1_le_one _1920@[simp] theorem noiseL1_character (u : ℝ≥0) (F : Finset ℕ) :21    noiseL1 𝕜 rates u (scalarCharacterLp 𝕜 1 F) =22      ((Real.exp (-(u : ℝ) * rateSum rates F) : ℝ) : 𝕜) • scalarCharacterLp 𝕜 1 F := by23  rw [noiseL1, convolutionL1_scalarCharacter]24  congr 225  exact integral_character rates u F2627@[simp] theorem noiseL1_zero : noiseL1 𝕜 rates 0 = ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 haar) := by28  apply continuousLinearMap_ext_on_scalarCharacterL129  intro F30  simp only [noiseL1_character, NNReal.coe_zero, neg_zero, zero_mul, Real.exp_zero,31    RCLike.ofReal_one, one_smul, ContinuousLinearMap.id_apply]3233theorem noiseL1_add (u v : ℝ≥0) :34    noiseL1 𝕜 rates (u + v) = (noiseL1 𝕜 rates u).comp (noiseL1 𝕜 rates v) := by35  apply continuousLinearMap_ext_on_scalarCharacterL136  intro F37  simp only [ContinuousLinearMap.comp_apply, noiseL1_character, map_smul, smul_smul]38  congr 139  rw [NNReal.coe_add, neg_add, add_mul, Real.exp_add, RCLike.ofReal_mul]40  exact mul_comm _ _4142theorem continuous_noiseL1_apply (f : Lp 𝕜 1 haar) : Continuous (fun u => noiseL1 𝕜 rates u f) := by43  apply continuous_iff_continuousAt.mpr44  intro u45  apply tendsto_apply_of_dense_span (scalarCharacterLp 𝕜 1)46    (dense_span_scalarCharacterLp 𝕜 1 (by norm_num)) (noiseL1 𝕜 rates)47    (noiseL1 𝕜 rates u) (𝓝 u) 1 (norm_noiseL1_le_one 𝕜 rates)48  intro F49  simp only [noiseL1_character]50  exact (show Continuous (fun v : ℝ≥0 =>51    ((Real.exp (-(v : ℝ) * rateSum rates F) : ℝ) : 𝕜) • scalarCharacterLp 𝕜 1 F) by52    fun_prop).tendsto u5354theorem noiseL1_strong_zero (f : Lp 𝕜 1 haar) :55    Tendsto (fun u => noiseL1 𝕜 rates u f) (𝓝 0) (𝓝 f) := by56  simpa only [noiseL1_zero, ContinuousLinearMap.id_apply] using57    (continuous_noiseL1_apply 𝕜 rates f).tendsto 05859theorem noiseL1_resolvent_commute (u : ℝ≥0) (t : PositiveTime) :60    (noiseL1 𝕜 rates u).comp (resolventL1 𝕜 rates t) =61      (resolventL1 𝕜 rates t).comp (noiseL1 𝕜 rates u) := by62  apply continuousLinearMap_ext_on_scalarCharacterL163  intro F64  simp only [ContinuousLinearMap.comp_apply, noiseL1_character,65    resolventL1_scalarCharacter, map_smul, smul_smul, mul_comm]6667/-- Full strong resolvent convergence along every positive time family tending68to zero, extending the dyadic convergence used in the main construction. -/69theorem resolventL1_strong_zero {α : Type*} (l : Filter α) (t : α → PositiveTime)70    (ht : Tendsto (fun a => (t a : ℝ)) l (𝓝 0)) (f : Lp 𝕜 1 haar) :71    Tendsto (fun a => resolventL1 𝕜 rates (t a) f) l (𝓝 f) := by72  apply tendsto_apply_of_dense_span (scalarCharacterLp 𝕜 1)73    (dense_span_scalarCharacterLp 𝕜 1 (by norm_num))74    (fun a => resolventL1 𝕜 rates (t a)) (ContinuousLinearMap.id 𝕜 _) l 175    (fun a => norm_resolventL1_le_one 𝕜 rates (t a))76  intro F77  have hreal : Tendsto (fun a => (1 + (t a : ℝ) * rateSum rates F)⁻¹) l (𝓝 (1 : ℝ)) := by78    simpa using ((ht.mul_const (rateSum rates F)).const_add 1).inv₀ (by norm_num)79  have hcast := ((RCLike.continuous_ofReal : Continuous (fun x : ℝ => (x : 𝕜))).tendsto80    (1 : ℝ)).comp hreal81  simpa only [Function.comp_def, resolventL1_scalarCharacter, RCLike.ofReal_one, one_smul,82    ContinuousLinearMap.id_apply] using hcast.smul_const (scalarCharacterLp 𝕜 1 F)8384end PL1.Noise85