PL1/BochnerResolvents.lean
All source files · Download exact source
SHA-256: a1eb5739b5bb4b381f52fbda85d8df15c4a7640b4923d4ceaf65b7e38084c204
1import PL1.NoiseSemigroup2import PL1.SeparableRange3import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap45/-! # Bochner resolvent representation and operator-norm truncation -/67noncomputable section8open Filter MeasureTheory ProbabilityTheory Set9open scoped Topology NNReal ENNReal1011namespace PL1.Noise12open Walsh ExponentialTime1314variable (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0)1516theorem noiseL1_apply_norm_le (u : ℝ≥0) (f : Lp 𝕜 1 haar) :17 ‖noiseL1 𝕜 rates u f‖ ≤ ‖f‖ :=18 ((noiseL1 𝕜 rates u).le_opNorm f).trans (by19 simpa only [one_mul] using mul_le_mul_of_nonneg_right20 (norm_noiseL1_le_one 𝕜 rates u) (norm_nonneg f))2122theorem integrable_noiseL1 (μ : Measure ℝ≥0) [IsFiniteMeasure μ] (f : Lp 𝕜 1 haar) :23 Integrable (fun u => noiseL1 𝕜 rates u f) μ := by24 let := Walsh.separableSpace_scalarL1 𝕜25 exact Integrable.of_bound (continuous_noiseL1_apply 𝕜 rates f).aestronglyMeasurable ‖f‖26 (ae_of_all μ (fun u => noiseL1_apply_norm_le 𝕜 rates u f))2728def averageNoiseLinear (μ : Measure ℝ≥0) [IsFiniteMeasure μ] :29 Lp 𝕜 1 haar →ₗ[𝕜] Lp 𝕜 1 haar where30 toFun f := ∫ u, noiseL1 𝕜 rates u f ∂μ31 map_add' f g := by32 simp only [map_add]33 exact integral_add (integrable_noiseL1 𝕜 rates μ f) (integrable_noiseL1 𝕜 rates μ g)34 map_smul' c f := by35 simp only [map_smul, integral_smul, RingHom.id_apply]3637theorem norm_averageNoiseLinear_le (μ : Measure ℝ≥0) [IsFiniteMeasure μ] (f : Lp 𝕜 1 haar) :38 ‖averageNoiseLinear 𝕜 rates μ f‖ ≤ μ.real univ * ‖f‖ := by39 have h := norm_integral_le_of_norm_le_const40 (ae_of_all μ (fun u => noiseL1_apply_norm_le 𝕜 rates u f))41 exact h.trans_eq (mul_comm _ _)4243def averageNoiseL1 (μ : Measure ℝ≥0) [IsFiniteMeasure μ] :44 Lp 𝕜 1 haar →L[𝕜] Lp 𝕜 1 haar :=45 (averageNoiseLinear 𝕜 rates μ).mkContinuous (μ.real univ) (norm_averageNoiseLinear_le 𝕜 rates μ)4647@[simp] theorem averageNoiseL1_apply (μ : Measure ℝ≥0) [IsFiniteMeasure μ] (f : Lp 𝕜 1 haar) :48 averageNoiseL1 𝕜 rates μ f = ∫ u, noiseL1 𝕜 rates u f ∂μ := rfl4950theorem norm_averageNoiseL1_le (μ : Measure ℝ≥0) [IsFiniteMeasure μ] :51 ‖averageNoiseL1 𝕜 rates μ‖ ≤ μ.real univ :=52 ContinuousLinearMap.opNorm_le_bound _ (measureReal_nonneg) (norm_averageNoiseLinear_le 𝕜 rates μ)5354theorem averageNoiseL1_timeMeasure (t : PositiveTime) :55 letI := isProbabilityMeasure_timeMeasure t.property56 averageNoiseL1 𝕜 rates (timeMeasure t) = resolventL1 𝕜 rates t := by57 let := isProbabilityMeasure_timeMeasure t.property58 apply continuousLinearMap_ext_on_scalarCharacterL159 intro F60 simp only [averageNoiseL1_apply, noiseL1_character, integral_smul_const,61 integral_laplace_ofReal t.property _ (rateSum_nonneg rates F), resolventL1_scalarCharacter]6263/-- The actual convolution resolvent equals the Bochner average on every L1 input. -/64theorem resolventL1_eq_integral (t : PositiveTime) (f : Lp 𝕜 1 haar) :65 resolventL1 𝕜 rates t f = ∫ u, noiseL1 𝕜 rates u f ∂timeMeasure t := by66 let := isProbabilityMeasure_timeMeasure t.property67 exact (DFunLike.congr_fun (averageNoiseL1_timeMeasure 𝕜 rates t) f).symm6869theorem averageNoiseL1_split (μ : Measure ℝ≥0) [IsFiniteMeasure μ]70 (A : Set ℝ≥0) (hA : MeasurableSet A) :71 averageNoiseL1 𝕜 rates μ = averageNoiseL1 𝕜 rates (μ.restrict A) +72 averageNoiseL1 𝕜 rates (μ.restrict Aᶜ) := by73 ext f74 simp only [averageNoiseL1_apply, add_apply]75 rw [← integral_add_measure (integrable_noiseL1 𝕜 rates (μ.restrict A) f)76 (integrable_noiseL1 𝕜 rates (μ.restrict Aᶜ) f), Measure.restrict_add_restrict_compl hA]7778theorem timeMeasure_real_Iic (t : PositiveTime) (ε : ℝ≥0) :79 (timeMeasure t).real (Iic ε) = 1 - Real.exp (-(ε : ℝ) / (t : ℝ)) := by80 let := isProbabilityMeasure_expMeasure (inv_pos.mpr t.property)81 rw [measureReal_def, timeMeasure,82 Measure.map_apply measurable_real_toNNReal measurableSet_Iic]83 have hp : Real.toNNReal ⁻¹' Iic ε = Iic (ε : ℝ) := by84 ext x85 exact Real.toNNReal_le_iff_le_coe86 rw [hp, ← measureReal_def, ← cdf_eq_real,87 cdf_expMeasure_eq (inv_pos.mpr t.property), ite_eq_left ε.coe_nonneg]88 congr 289 ring9091/-- The same noise average with times below ε omitted. -/92def truncatedResolventL1 (t : PositiveTime) (ε : ℝ≥0) :93 Lp 𝕜 1 haar →L[𝕜] Lp 𝕜 1 haar := by94 let := isProbabilityMeasure_timeMeasure t.property95 exact averageNoiseL1 𝕜 rates ((timeMeasure t).restrict (Ici ε))9697theorem norm_resolventL1_sub_truncated_le (t : PositiveTime) (ε : ℝ≥0) :98 ‖resolventL1 𝕜 rates t - truncatedResolventL1 𝕜 rates t ε‖ ≤99 1 - Real.exp (-(ε : ℝ) / (t : ℝ)) := by100 let := isProbabilityMeasure_timeMeasure t.property101 have hs := averageNoiseL1_split 𝕜 rates (timeMeasure t) (Ici ε) measurableSet_Ici102 rw [averageNoiseL1_timeMeasure] at hs103 have he : resolventL1 𝕜 rates t - truncatedResolventL1 𝕜 rates t ε =104 averageNoiseL1 𝕜 rates ((timeMeasure t).restrict (Iio ε)) := by105 rw [hs]106 change averageNoiseL1 𝕜 rates ((timeMeasure t).restrict (Ici ε)) +107 averageNoiseL1 𝕜 rates ((timeMeasure t).restrict (Ici ε)ᶜ) -108 averageNoiseL1 𝕜 rates ((timeMeasure t).restrict (Ici ε)) = _109 rw [add_sub_cancel_left, compl_Ici]110 rw [he]111 apply (norm_averageNoiseL1_le 𝕜 rates ((timeMeasure t).restrict (Iio ε))).trans112 rw [Measure.real, Measure.restrict_apply MeasurableSet.univ, univ_inter]113 rw [← timeMeasure_real_Iic t ε]114 exact measureReal_mono Iio_subset_Iic_self115116theorem truncatedResolventL1_apply (t : PositiveTime) (ε : ℝ≥0) (f : Lp 𝕜 1 haar) :117 truncatedResolventL1 𝕜 rates t ε f =118 ∫ u in Ici ε, noiseL1 𝕜 rates u f ∂timeMeasure t := rfl119120/-- The truncated averages converge in actual L1 operator norm, for any121nonnegative cutoffs tending to zero. -/122theorem truncatedResolventL1_tendsto {α : Type*} (l : Filter α)123 (t : PositiveTime) (ε : α → ℝ≥0) (hε : Tendsto (fun a => (ε a : ℝ)) l (𝓝 0)) :124 Tendsto (fun a => truncatedResolventL1 𝕜 rates t (ε a)) l (𝓝 (resolventL1 𝕜 rates t)) := by125 have hb : Tendsto (fun a => 1 - Real.exp (-(ε a : ℝ) / (t : ℝ))) l (𝓝 (0 : ℝ)) := by126 have he := (Real.continuous_exp.tendsto (-(0 : ℝ) / (t : ℝ))).comp127 (hε.neg.div_const (t : ℝ))128 simpa only [neg_zero, zero_div, Real.exp_zero, sub_self, Function.comp_def] using129 (tendsto_const_nhds (x := (1 : ℝ)) (f := l)).sub he130 have hn : Tendsto (fun a => ‖truncatedResolventL1 𝕜 rates t (ε a) -131 resolventL1 𝕜 rates t‖) l (𝓝 0) :=132 squeeze_zero (fun _ => norm_nonneg _) (fun a => by133 rw [norm_sub_rev]134 exact norm_resolventL1_sub_truncated_le 𝕜 rates t (ε a)) hb135 exact tendsto_iff_norm_sub_tendsto_zero.mpr hn136137end PL1.Noise138