PL1/L1Multiplication.lean
All source files · Download exact source
SHA-256: ce6e3a48ad7f2e9c8cbdf6461fd9aba94eb035d507802bf3d0b1d5a8596794c1
1import PL1.ConvolutionL123/-! # Actual multiplication by continuous real functions on Haar L1 -/45noncomputable section6open MeasureTheory7open scoped ENNReal89namespace PL1.L1Multiplication10open Walsh1112variable (K : Type*) [RCLike K]1314theorem integrable_product (q : C(Walsh.Group, ℝ)) (f : Lp K 1 haar) :15 Integrable (fun x => q x • f x) haar :=16 (L1.integrable_coeFn f).bdd_smul (𝕜 := ℝ) ‖q‖ q.continuous.aestronglyMeasurable17 (ae_of_all _ (fun x => q.norm_coe_le_norm x))1819def product (q : C(Walsh.Group, ℝ)) (f : Lp K 1 haar) : Lp K 1 haar :=20 (integrable_product K q f).toL1 (fun x => q x • f x)2122theorem coeFn_product (q : C(Walsh.Group, ℝ)) (f : Lp K 1 haar) :23 product K q f =ᵐ[haar] fun x => q x • f x :=24 (integrable_product K q f).coeFn_toL12526theorem product_add (q : C(Walsh.Group, ℝ)) (f g : Lp K 1 haar) :27 product K q (f + g) = product K q f + product K q g := by28 apply Lp.ext29 filter_upwards [coeFn_product K q (f + g), coeFn_product K q f,30 coeFn_product K q g, Lp.coeFn_add f g, Lp.coeFn_add (product K q f) (product K q g)]31 with x hsum hf hg hadd hprod32 simp only [hsum, hprod, hf, hg, hadd, Pi.add_apply, smul_add]3334theorem product_smul (q : C(Walsh.Group, ℝ)) (c : K) (f : Lp K 1 haar) :35 product K q (c • f) = c • product K q f := by36 apply Lp.ext37 filter_upwards [coeFn_product K q (c • f), coeFn_product K q f,38 Lp.coeFn_smul c f, Lp.coeFn_smul c (product K q f)] with x hcf hf hsm hprod39 simp only [hcf, hprod, hsm, Pi.smul_apply, hf]40 exact smul_comm (q x) c (f x)4142theorem norm_product_le (q : C(Walsh.Group, ℝ)) (f : Lp K 1 haar) :43 ‖product K q f‖ ≤ ‖q‖ * ‖f‖ := by44 apply Lp.norm_le_mul_norm_of_ae_le_mul45 filter_upwards [coeFn_product K q f] with x hx46 rw [hx, norm_smul]47 exact mul_le_mul_of_nonneg_right (q.norm_coe_le_norm x) (norm_nonneg _)4849def multiplier (q : C(Walsh.Group, ℝ)) : Lp K 1 haar →L[K] Lp K 1 haar :=50 LinearMap.mkContinuous51 { toFun := product K q52 map_add' := product_add K q53 map_smul' := product_smul K q }54 ‖q‖ (norm_product_le K q)5556theorem multiplier_apply (q : C(Walsh.Group, ℝ)) (f : Lp K 1 haar) :57 multiplier K q f = product K q f := rfl5859theorem coeFn_multiplier (q : C(Walsh.Group, ℝ)) (f : Lp K 1 haar) :60 multiplier K q f =ᵐ[haar] fun x => q x • f x := coeFn_product K q f6162theorem norm_multiplier_le (q : C(Walsh.Group, ℝ)) : ‖multiplier K q‖ ≤ ‖q‖ :=63 ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg q) (norm_product_le K q)6465def continuousProduct (q : C(Walsh.Group, ℝ)) (f : C(Walsh.Group, K)) :66 C(Walsh.Group, K) := ⟨fun x => q x • f x,67 Continuous.smul (M := ℝ) q.continuous f.continuous⟩6869theorem multiplier_toLp (q : C(Walsh.Group, ℝ)) (f : C(Walsh.Group, K)) :70 multiplier K q (ContinuousMap.toLp 1 haar K f) =71 ContinuousMap.toLp 1 haar K (continuousProduct K q f) := by72 apply Lp.ext73 filter_upwards [coeFn_multiplier K q (ContinuousMap.toLp 1 haar K f),74 ContinuousMap.coeFn_toLp (p := 1) (𝕜 := K) haar f,75 ContinuousMap.coeFn_toLp (p := 1) (𝕜 := K) haar (continuousProduct K q f)]76 with x hx hf hprod77 rw [hx, hf, hprod]78 rfl7980theorem multiplier_add (q r : C(Walsh.Group, ℝ)) :81 multiplier K (q + r) = multiplier K q + multiplier K r := by82 apply ContinuousLinearMap.ext83 intro f84 apply Lp.ext85 filter_upwards [coeFn_multiplier K (q + r) f, coeFn_multiplier K q f,86 coeFn_multiplier K r f, Lp.coeFn_add (multiplier K q f) (multiplier K r f)]87 with x hsum hq hr hadd88 simp only [add_apply, hsum, hadd, hq, hr,89 ContinuousMap.add_apply, Pi.add_apply, add_smul]9091theorem multiplier_one : multiplier K 1 = ContinuousLinearMap.id K (Lp K 1 haar) := by92 apply ContinuousLinearMap.ext93 intro f94 apply Lp.ext95 filter_upwards [coeFn_multiplier K 1 f] with x hx96 simpa only [ContinuousMap.one_apply, one_smul, ContinuousLinearMap.id_apply] using hx9798theorem multiplier_sub (q r : C(Walsh.Group, ℝ)) (f : Lp K 1 haar) :99 multiplier K (q - r) f = multiplier K q f - multiplier K r f := by100 apply Lp.ext101 filter_upwards [coeFn_multiplier K (q - r) f, coeFn_multiplier K q f,102 coeFn_multiplier K r f, Lp.coeFn_sub (multiplier K q f) (multiplier K r f)]103 with x hsum hq hr hadd104 simp only [hsum, hadd, hq, hr, ContinuousMap.sub_apply, Pi.sub_apply, sub_smul]105106end PL1.L1Multiplication107