PL1/HeadTailNoise.lean
All source files · Download exact source
SHA-256: 4899c913b0e752e43bce481e4b01eeed4c0c5231ac3c9f9b502c79449d86255d
1import PL1.HeadTail2import PL1.L1Multiplication34/-! # Exact noise factorization on disjoint finite coordinates -/56noncomputable section7open MeasureTheory8open scoped ENNReal NNReal9namespace PL1.HeadTail10open Walsh1112variable {K : Type*} [RCLike K]1314theorem DependsOn.convolution {S : Finset ℕ} {f : Walsh.Group → K}15 (hf : DependsOn S f) (ν : Measure Walsh.Group) :16 DependsOn S (fun x => ∫ y, f (x * y) ∂ν) := by17 intro x z hxz18 apply integral_congr_ae19 exact ae_of_all _ (fun y => hf _ _ (fun j hj =>20 congrArg (fun a => a * y j) (hxz j hj)))2122/-- The continuous representative of the actual product-noise convolution. -/23def noiseContinuous (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0) (u : ℝ≥0)24 (S : Finset ℕ) (f : C(Walsh.Group, K)) (hf : DependsOn S f) : C(Walsh.Group, K) :=25 ⟨fun x => ∫ y, f (x * y) ∂Noise.measure rates u, (hf.convolution _).continuous⟩2627theorem noiseContinuous_apply (rates : ℕ → ℝ≥0) (u : ℝ≥0)28 (S : Finset ℕ) (f : C(Walsh.Group, K)) (hf : DependsOn S f) (x : Walsh.Group) :29 noiseContinuous K rates u S f hf x = ∫ y, f (x * y) ∂Noise.measure rates u := rfl3031theorem noiseContinuous_dependsOn (rates : ℕ → ℝ≥0) (u : ℝ≥0)32 (S : Finset ℕ) (f : C(Walsh.Group, K)) (hf : DependsOn S f) :33 DependsOn S (noiseContinuous K rates u S f hf) := hf.convolution _3435theorem noiseContinuous_toLp (rates : ℕ → ℝ≥0) (u : ℝ≥0)36 (S : Finset ℕ) (f : C(Walsh.Group, K)) (hf : DependsOn S f) :37 ContinuousMap.toLp 1 haar K (noiseContinuous K rates u S f hf) =38 Noise.noiseL1 K rates u (ContinuousMap.toLp 1 haar K f) := by39 apply Lp.ext40 filter_upwards [ContinuousMap.coeFn_toLp (p := 1) (𝕜 := K) haar (noiseContinuous K rates u S f hf),41 convolutionL1_ae_eq_integral_of_ae_eq (Noise.measure rates u)42 (ContinuousMap.coeFn_toLp (p := 1) (𝕜 := K) haar f)] with x hx hy43 exact hx.trans hy.symm4445/-- Product-noise factorization is valid for the actual independent coordinate measures. -/46theorem integral_noise_smul (rates : ℕ → ℝ≥0) (u : ℝ≥0)47 {S T : Finset ℕ} (hST : Disjoint S T)48 (f : C(Walsh.Group, K)) (q : C(Walsh.Group, ℝ))49 (hf : DependsOn S f) (hq : DependsOn T q) (x : Walsh.Group) :50 (∫ y, q (x * y) • f (x * y) ∂Noise.measure rates u) =51 (∫ y, q (x * y) ∂Noise.measure rates u) •52 ∫ y, f (x * y) ∂Noise.measure rates u := by53 borelize K54 exact (indepFun_noise rates u hST.symm (hq.translate x) (hf.translate x)).integral_fun_smul_eq_smul_integral55 (hq.translate x).continuous.aestronglyMeasurable (hf.translate x).continuous.aestronglyMeasurable5657/-- The factorization descends to the actual Haar L1 quotient and multiplier operator. -/58theorem noiseL1_multiplier_toLp (rates : ℕ → ℝ≥0) (u : ℝ≥0)59 {S T : Finset ℕ} (hST : Disjoint S T)60 (f : C(Walsh.Group, K)) (q : C(Walsh.Group, ℝ))61 (hf : DependsOn S f) (hq : DependsOn T q) :62 Noise.noiseL1 K rates u (L1Multiplication.multiplier K q (ContinuousMap.toLp 1 haar K f)) =63 L1Multiplication.multiplier K (noiseContinuous ℝ rates u T q hq)64 (Noise.noiseL1 K rates u (ContinuousMap.toLp 1 haar K f)) := by65 have hprod : L1Multiplication.multiplier K q (ContinuousMap.toLp 1 haar K f) =ᵐ[haar]66 fun x => q x • f x := by67 filter_upwards [L1Multiplication.coeFn_multiplier K q (ContinuousMap.toLp 1 haar K f),68 ContinuousMap.coeFn_toLp (p := 1) (𝕜 := K) haar f] with x hx hy69 rw [hx, hy]70 apply Lp.ext71 filter_upwards [convolutionL1_ae_eq_integral_of_ae_eq (Noise.measure rates u) hprod,72 L1Multiplication.coeFn_multiplier K (noiseContinuous ℝ rates u T q hq)73 (Noise.noiseL1 K rates u (ContinuousMap.toLp 1 haar K f)),74 convolutionL1_ae_eq_integral_of_ae_eq (Noise.measure rates u)75 (ContinuousMap.coeFn_toLp (p := 1) (𝕜 := K) haar f)] with x hx hy hz76 change _ = (L1Multiplication.multiplier K (noiseContinuous ℝ rates u T q hq) _) x77 rw [hy]78 change _ = (∫ y, q (x * y) ∂Noise.measure rates u) •79 (Noise.noiseL1 K rates u (ContinuousMap.toLp 1 haar K f)) x80 rw [show (Noise.noiseL1 K rates u (ContinuousMap.toLp 1 haar K f)) x = _ from hz]81 exact hx.trans (integral_noise_smul rates u hST f q hf hq x)8283#print axioms noiseL1_multiplier_toLp84end PL1.HeadTail85