PL1/ConvolutionL1.lean
All source files · Download exact source
SHA-256: feac4e1ed4938f58b599f01078e91719f0ce160b4f9a9339716d42209a5eb6e6
1import PL1.WalshModel2import Mathlib.MeasureTheory.Integral.Prod3import Mathlib.MeasureTheory.Group.Prod4import Mathlib.Analysis.RCLike.Basic56/-!7# Probability convolution on the actual Haar L1 space89The construction uses a product measure and Fubini, so it acts on genuine L110equivalence classes. It applies to arbitrary probability measures, including11measures singular with respect to Haar measure.12-/1314noncomputable section1516open MeasureTheory MeasureTheory.Measure17open scoped ENNReal1819namespace PL1.Walsh2021variable {𝕜 : Type*} [RCLike 𝕜]2223/-- Every element of the sign group is its own inverse. -/24@[simp] theorem group_inv_eq_self (x : Group) : x⁻¹ = x := by25 funext j26 exact congrArg Multiplicative.ofAdd (ZMod.neg_eq_self_mod_two (x j).toAdd)2728/-- Multiplication sends Haar × ν to Haar when ν is a probability measure. -/29theorem measurePreserving_multiply (ν : Measure Group) [IsProbabilityMeasure ν] :30 MeasurePreserving (fun z : Group × Group => z.1 * z.2) (haar.prod ν) haar :=31 measurePreserving_fst.comp (measurePreserving_mul_prod haar ν)3233/-- The scalar integral representative used in probability convolution. -/34def convolutionFunction (ν : Measure Group) (f : Lp 𝕜 1 haar) (x : Group) : 𝕜 :=35 ∫ y, f (x * y) ∂ν3637theorem integrable_convolution_integrand (ν : Measure Group) [IsProbabilityMeasure ν]38 (f : Lp 𝕜 1 haar) :39 Integrable (fun z : Group × Group => f (z.1 * z.2)) (haar.prod ν) :=40 (measurePreserving_multiply ν).integrable_comp_of_integrable (L1.integrable_coeFn f)4142theorem integrable_convolutionFunction (ν : Measure Group) [IsProbabilityMeasure ν]43 (f : Lp 𝕜 1 haar) : Integrable (convolutionFunction ν f) haar :=44 (integrable_convolution_integrand ν f).integral_prod_left4546/-- Probability convolution as a function between actual L1 quotient spaces. -/47def convolutionL1Fun (ν : Measure Group) [IsProbabilityMeasure ν]48 (f : Lp 𝕜 1 haar) : Lp 𝕜 1 haar :=49 (integrable_convolutionFunction ν f).toL1 (convolutionFunction ν f)5051theorem coeFn_convolutionL1Fun (ν : Measure Group) [IsProbabilityMeasure ν]52 (f : Lp 𝕜 1 haar) :53 convolutionL1Fun ν f =ᵐ[haar] convolutionFunction ν f :=54 (integrable_convolutionFunction ν f).coeFn_toL15556theorem convolutionFunction_add (ν : Measure Group) [IsProbabilityMeasure ν]57 (f g : Lp 𝕜 1 haar) :58 convolutionFunction ν (f + g) =ᵐ[haar]59 fun x => convolutionFunction ν f x + convolutionFunction ν g x := by60 have hae := (measurePreserving_multiply ν).quasiMeasurePreserving.ae_eq_comp61 (Lp.coeFn_add f g)62 filter_upwards [ae_ae_of_ae_prod hae,63 (integrable_convolution_integrand ν f).prod_right_ae,64 (integrable_convolution_integrand ν g).prod_right_ae] with x hx hf hg65 change (∫ y, (f + g) (x * y) ∂ν) = _66 calc67 _ = ∫ y, (f (x * y) + g (x * y)) ∂ν := integral_congr_ae hx68 _ = _ := integral_add hf hg6970theorem convolutionFunction_smul (ν : Measure Group) [IsProbabilityMeasure ν]71 (c : 𝕜) (f : Lp 𝕜 1 haar) :72 convolutionFunction ν (c • f) =ᵐ[haar] fun x => c • convolutionFunction ν f x := by73 have hae := (measurePreserving_multiply ν).quasiMeasurePreserving.ae_eq_comp74 (Lp.coeFn_smul c f)75 filter_upwards [ae_ae_of_ae_prod hae] with x hx76 change (∫ y, (c • f) (x * y) ∂ν) = _77 calc78 _ = ∫ y, c • f (x * y) ∂ν := integral_congr_ae hx79 _ = _ := integral_smul c _8081theorem convolutionL1Fun_add (ν : Measure Group) [IsProbabilityMeasure ν]82 (f g : Lp 𝕜 1 haar) :83 convolutionL1Fun ν (f + g) = convolutionL1Fun ν f + convolutionL1Fun ν g := by84 apply Lp.ext85 filter_upwards [coeFn_convolutionL1Fun ν (f + g), coeFn_convolutionL1Fun ν f,86 coeFn_convolutionL1Fun ν g, convolutionFunction_add ν f g,87 Lp.coeFn_add (convolutionL1Fun ν f) (convolutionL1Fun ν g)] with x hfg hf hg hconv hadd88 simpa only [hfg, hadd, Pi.add_apply, hf, hg] using hconv8990theorem convolutionL1Fun_smul (ν : Measure Group) [IsProbabilityMeasure ν]91 (c : 𝕜) (f : Lp 𝕜 1 haar) :92 convolutionL1Fun ν (c • f) = c • convolutionL1Fun ν f := by93 apply Lp.ext94 filter_upwards [coeFn_convolutionL1Fun ν (c • f), coeFn_convolutionL1Fun ν f,95 convolutionFunction_smul ν c f, Lp.coeFn_smul c (convolutionL1Fun ν f)] with x hcf hf hconv hsmul96 simpa only [hcf, hf, hsmul, Pi.smul_apply] using hconv9798/-- Convolution by a probability measure is an L1 contraction. -/99theorem norm_convolutionL1Fun_le (ν : Measure Group) [IsProbabilityMeasure ν]100 (f : Lp 𝕜 1 haar) : ‖convolutionL1Fun ν f‖ ≤ ‖f‖ := by101 have hprod := integrable_convolution_integrand ν f102 have hmap : AEStronglyMeasurable (fun x => ‖f x‖)103 (Measure.map (fun z : Group × Group => z.1 * z.2) (haar.prod ν)) := by104 rw [(measurePreserving_multiply ν).map_eq]105 exact (Lp.aestronglyMeasurable f).norm106 calc107 ‖convolutionL1Fun ν f‖ = ∫ x, ‖convolutionFunction ν f x‖ ∂haar :=108 L1.norm_of_fun_eq_integral_norm (integrable_convolutionFunction ν f)109 _ ≤ ∫ x, ∫ y, ‖f (x * y)‖ ∂ν ∂haar := by110 apply integral_mono (integrable_convolutionFunction ν f).norm hprod.integral_norm_prod_left111 intro x112 exact norm_integral_le_integral_norm _113 _ = ∫ z : Group × Group, ‖f (z.1 * z.2)‖ ∂(haar.prod ν) :=114 integral_integral hprod.norm115 _ = ∫ x, ‖f x‖ ∂haar := by116 have h := integral_map (measurePreserving_multiply ν).measurable.aemeasurable hmap117 rw [(measurePreserving_multiply ν).map_eq] at h118 exact h.symm119 _ = ‖f‖ := (L1.norm_eq_integral_norm f).symm120121/-- The bounded linear probability-convolution operator used by the construction. -/122def convolutionL1 (ν : Measure Group) [IsProbabilityMeasure ν] :123 Lp 𝕜 1 haar →L[𝕜] Lp 𝕜 1 haar :=124 LinearMap.mkContinuous125 { toFun := convolutionL1Fun ν126 map_add' := convolutionL1Fun_add ν127 map_smul' := convolutionL1Fun_smul ν }128 1 (fun f => by129 change ‖convolutionL1Fun ν f‖ ≤ 1 * ‖f‖130 simpa only [one_mul] using norm_convolutionL1Fun_le ν f)131132theorem convolutionL1_apply (ν : Measure Group) [IsProbabilityMeasure ν]133 (f : Lp 𝕜 1 haar) : convolutionL1 ν f = convolutionL1Fun ν f := rfl134135theorem coeFn_convolutionL1 (ν : Measure Group) [IsProbabilityMeasure ν]136 (f : Lp 𝕜 1 haar) :137 convolutionL1 ν f =ᵐ[haar] fun x => ∫ y, f (x * y) ∂ν :=138 coeFn_convolutionL1Fun ν f139140theorem norm_convolutionL1_le_one (ν : Measure Group) [IsProbabilityMeasure ν] :141 ‖convolutionL1 (𝕜 := 𝕜) ν‖ ≤ 1 := by142 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one143 intro f144 simpa only [convolutionL1_apply, one_mul] using norm_convolutionL1Fun_le ν f145146/-- Any representative of an L1 class gives the same convolution almost everywhere,147even when the convolving measure is singular. -/148theorem convolutionL1_ae_eq_integral_of_ae_eq (ν : Measure Group) [IsProbabilityMeasure ν]149 {f : Lp 𝕜 1 haar} {g : Group → 𝕜} (hfg : f =ᵐ[haar] g) :150 convolutionL1 ν f =ᵐ[haar] fun x => ∫ y, g (x * y) ∂ν := by151 have hae := (measurePreserving_multiply ν).quasiMeasurePreserving.ae_eq_comp hfg152 filter_upwards [coeFn_convolutionL1 ν f, ae_ae_of_ae_prod hae] with x hx hxy153 exact hx.trans (integral_congr_ae hxy)154155/-- The quotient construction agrees with the raw convolution definition already156used for real-valued Walsh characters. -/157theorem convolutionL1_ae_eq_convolution (ν : Measure Group) [IsProbabilityMeasure ν]158 (f : Lp ℝ 1 haar) : convolutionL1 ν f =ᵐ[haar] convolution ν f := by159 filter_upwards [coeFn_convolutionL1 ν f] with x hx160 change convolutionL1 ν f x = ∫ y, f (x * y⁻¹) ∂ν161 simpa only [group_inv_eq_self] using hx162163/-- Convolution by a probability measure preserves the Haar integral. -/164theorem integral_convolutionL1 (ν : Measure Group) [IsProbabilityMeasure ν]165 (f : Lp 𝕜 1 haar) :166 ∫ x, convolutionL1 ν f x ∂haar = ∫ x, f x ∂haar := by167 have hmap : AEStronglyMeasurable (fun x => f x)168 (Measure.map (fun z : Group × Group => z.1 * z.2) (haar.prod ν)) := by169 rw [(measurePreserving_multiply ν).map_eq]170 exact Lp.aestronglyMeasurable f171 calc172 _ = ∫ x, ∫ y, f (x * y) ∂ν ∂haar := integral_congr_ae (coeFn_convolutionL1 ν f)173 _ = ∫ z : Group × Group, f (z.1 * z.2) ∂(haar.prod ν) :=174 integral_integral (integrable_convolution_integrand ν f)175 _ = _ := by176 have h := integral_map (measurePreserving_multiply ν).measurable.aemeasurable hmap177 rw [(measurePreserving_multiply ν).map_eq] at h178 exact h.symm179180/-- The real Walsh eigenvalue formula for the actual L1 convolution operator. -/181theorem convolutionL1_character (ν : Measure Group) [IsProbabilityMeasure ν]182 (F : Finset ℕ) :183 convolutionL1 ν (characterLp 1 F) = coefficient ν F • characterLp 1 F := by184 apply Lp.ext185 filter_upwards [convolutionL1_ae_eq_integral_of_ae_eq ν (coeFn_characterLp 1 F),186 Lp.coeFn_smul (coefficient ν F) (characterLp 1 F), coeFn_characterLp 1 F]187 with x hconv hsmul hchar188 rw [hconv, hsmul, Pi.smul_apply, hchar]189 simp only [character_mul, integral_const_mul, coefficient, smul_eq_mul, mul_comm]190191/-- The same eigenvalue formula over either scalar field, with the real Fourier192coefficient explicitly embedded into the selected RCLike field. -/193theorem convolutionL1_scalarCharacter (ν : Measure Group) [IsProbabilityMeasure ν]194 (F : Finset ℕ) :195 convolutionL1 ν (scalarCharacterLp 𝕜 1 F) =196 (coefficient ν F : 𝕜) • scalarCharacterLp 𝕜 1 F := by197 apply Lp.ext198 filter_upwards [convolutionL1_ae_eq_integral_of_ae_eq ν (coeFn_scalarCharacterLp 𝕜 1 F),199 Lp.coeFn_smul (coefficient ν F : 𝕜) (scalarCharacterLp 𝕜 1 F),200 coeFn_scalarCharacterLp 𝕜 1 F] with x hconv hsmul hchar201 rw [hconv, hsmul, Pi.smul_apply, hchar]202 simp only [scalarCharacter, character_mul, RCLike.ofReal_mul, integral_const_mul,203 integral_ofReal, coefficient, smul_eq_mul, mul_comm]204205/-- Continuous linear maps on Haar L1 are determined by their Walsh values. -/206theorem continuousLinearMap_ext_on_scalarCharacterL1207 {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]208 {S T : Lp 𝕜 1 haar →L[𝕜] E}209 (h : ∀ F : Finset ℕ, S (scalarCharacterLp 𝕜 1 F) = T (scalarCharacterLp 𝕜 1 F)) :210 S = T := by211 apply ContinuousLinearMap.ext_on (dense_span_scalarCharacterLp 𝕜 1 (by norm_num))212 rintro x ⟨F, rfl⟩213 exact h F214215/-- Equality of Walsh coefficients implies equality of the probability convolution operators. -/216theorem convolutionL1_eq_of_coefficients_eq217 (ν ρ : Measure Group) [IsProbabilityMeasure ν] [IsProbabilityMeasure ρ]218 (h : ∀ F : Finset ℕ, coefficient ν F = coefficient ρ F) :219 convolutionL1 (𝕜 := 𝕜) ν = convolutionL1 ρ := by220 apply continuousLinearMap_ext_on_scalarCharacterL1221 intro F222 rw [convolutionL1_scalarCharacter, convolutionL1_scalarCharacter, h F]223224/-- A product identity for Walsh coefficients induces the corresponding operator225composition identity. This is useful for the noise semigroup. -/226theorem convolutionL1_comp_eq_of_coefficients227 (ν ρ τ : Measure Group) [IsProbabilityMeasure ν] [IsProbabilityMeasure ρ]228 [IsProbabilityMeasure τ]229 (h : ∀ F : Finset ℕ, coefficient τ F = coefficient ν F * coefficient ρ F) :230 (convolutionL1 (𝕜 := 𝕜) ν).comp (convolutionL1 ρ) = convolutionL1 τ := by231 apply continuousLinearMap_ext_on_scalarCharacterL1232 intro F233 simp only [ContinuousLinearMap.comp_apply, convolutionL1_scalarCharacter, map_smul,234 h F, RCLike.ofReal_mul, smul_smul, mul_comm]235236end PL1.Walsh237