PL1/SingularConvolution.lean
All source files · Download exact source
SHA-256: 9a5c41a807c2d2e1bf3654ff570845623a6eb8e5cf3695d093f1ada2612d2d9e
1import PL1.WalshModel2import PL1.ConvolutionL13import PL1.RNPBridge4import Mathlib.MeasureTheory.Function.Holder5import Mathlib.MeasureTheory.Function.AEEqOfIntegral6import Mathlib.MeasureTheory.Measure.HasOuterApproxClosed7import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap89/-!10# Singular measures and the Walsh spectral obstruction1112For a finite positive measure, all Walsh coefficients determine the measure.13A measure charging a Haar-null set therefore cannot have the Walsh coefficients14of an integrable real density. This is the scalar obstruction needed for the15nonrepresentability of singular convolution.16-/1718noncomputable section19universe u2021open MeasureTheory22open scoped ENNReal Topology BigOperators2324namespace PL125namespace SingularConvolution2627open Walsh2829/-- Integration on continuous functions on the compact sign group, as a bounded functional. -/30def continuousIntegral (μ : Measure Walsh.Group) [IsFiniteMeasure μ] : C(Walsh.Group, ℝ) →L[ℝ] ℝ :=31 (L1.integralCLM : Lp ℝ 1 μ →L[ℝ] ℝ).comp (ContinuousMap.toLp 1 μ ℝ)3233theorem continuousIntegral_apply (μ : Measure Walsh.Group) [IsFiniteMeasure μ]34 (f : C(Walsh.Group, ℝ)) : continuousIntegral μ f = ∫ x, f x ∂μ := by35 change L1.integralCLM (ContinuousMap.toLp 1 μ ℝ f) = _36 rw [← L1.integral_eq, L1.integral_eq_integral]37 exact integral_congr_ae (ContinuousMap.coeFn_toLp μ f)3839/-- All Walsh coefficients determine a finite positive Borel measure. -/40theorem measure_eq_of_walsh_integrals (μ ν : Measure Walsh.Group)41 [IsFiniteMeasure μ] [IsFiniteMeasure ν]42 (h : ∀ F : Finset ℕ, ∫ x, character F x ∂μ = ∫ x, character F x ∂ν) : μ = ν := by43 have hi : continuousIntegral μ = continuousIntegral ν := by44 apply ContinuousLinearMap.ext_on (s := Set.range characterContinuous)45 · rw [← polynomials_toSubmodule]46 exact polynomials_dense47 · rintro f ⟨F, rfl⟩48 rw [continuousIntegral_apply, continuousIntegral_apply]49 exact h F50 apply ext_of_forall_integral_eq_of_IsFiniteMeasure51 intro f52 have hh := congrArg (fun T => T f.toContinuousMap) hi53 rw [continuousIntegral_apply, continuousIntegral_apply] at hh54 exact hh5556theorem integrable_character_measure (μ : Measure Walsh.Group) [IsFiniteMeasure μ]57 (F : Finset ℕ) : Integrable (character F) μ := by58 apply Integrable.of_bound (continuous_character F).aestronglyMeasurable 159 exact ae_of_all _ (fun x => (norm_character F x).le)6061/-- The measure with positive part of a real density. -/62def positiveDensityMeasure (g : Walsh.Group → ℝ) : Measure Walsh.Group :=63 haar.withDensity (fun x => ENNReal.ofReal (g x))6465theorem positiveDensityMeasure_finite {g : Walsh.Group → ℝ} (hg : Integrable g haar) :66 IsFiniteMeasure (positiveDensityMeasure g) := by67 exact isFiniteMeasure_withDensity_ofReal hg.hasFiniteIntegral6869theorem integral_positiveDensityMeasure {g : Walsh.Group → ℝ} (hg : Integrable g haar)70 (f : Walsh.Group → ℝ) :71 ∫ x, f x ∂positiveDensityMeasure g = ∫ x, max (g x) 0 * f x ∂haar := by72 rw [positiveDensityMeasure, integral_withDensity_eq_integral_toReal_smul₀73 hg.aestronglyMeasurable.aemeasurable.ennreal_ofReal74 (ae_of_all _ (fun _ => ENNReal.ofReal_lt_top))]75 simp only [ENNReal.toReal_ofReal', smul_eq_mul]7677/-- Matching Walsh moments of an integrable density gives equality after moving its negative78part to the positive-measure side. -/79theorem measure_add_negativeDensity_eq_positiveDensity80 (ν : Measure Walsh.Group) [IsFiniteMeasure ν]81 {g : Walsh.Group → ℝ} (hg : Integrable g haar)82 (hMom : ∀ F : Finset ℕ,83 ∫ x, character F x * g x ∂haar = ∫ x, character F x ∂ν) :84 ν + positiveDensityMeasure (fun x => -g x) = positiveDensityMeasure g := by85 let := positiveDensityMeasure_finite hg86 let := positiveDensityMeasure_finite hg.neg87 apply measure_eq_of_walsh_integrals88 intro F89 rw [integral_add_measure (integrable_character_measure ν F)90 (integrable_character_measure _ F)]91 rw [integral_positiveDensityMeasure (g := fun x => -g x) hg.neg,92 integral_positiveDensityMeasure hg, ← hMom F]93 have hchar : AEStronglyMeasurable (character F) haar := (continuous_character F).aestronglyMeasurable94 have hb : ∀ᵐ x ∂haar, ‖character F x‖ ≤ 1 := ae_of_all _ (fun x => (norm_character F x).le)95 rw [← integral_add (hg.bdd_mul hchar hb) (hg.neg_part.mul_bdd hchar hb)]96 apply integral_congr_ae97 exact ae_of_all _ (fun x => by98 have hparts : g x + max (-g x) 0 = max (g x) 0 := by99 linarith [max_zero_sub_max_neg_zero_eq_self (g x)]100 calc101 character F x * g x + max (-g x) 0 * character F x =102 (g x + max (-g x) 0) * character F x := by ring103 _ = max (g x) 0 * character F x := by rw [hparts])104105/-- A finite measure charging a Haar-null set cannot have the Walsh moments of an L1 density. -/106theorem no_integrable_density_of_null_carrier107 (ν : Measure Walsh.Group) [IsFiniteMeasure ν] (N : Set Walsh.Group)108 (hmN : haar N = 0) (hνN : ν N ≠ 0) :109 ¬ ∃ g : Walsh.Group → ℝ, Integrable g haar ∧110 ∀ F : Finset ℕ, ∫ x, character F x * g x ∂haar = ∫ x, character F x ∂ν := by111 rintro ⟨g, hg, hMom⟩112 have heq := measure_add_negativeDensity_eq_positiveDensity ν hg hMom113 have hp : positiveDensityMeasure g N = 0 :=114 withDensity_absolutelyContinuous haar _ hmN115 have hn : positiveDensityMeasure (fun x => -g x) N = 0 :=116 withDensity_absolutelyContinuous haar _ hmN117 have hev := congrArg (fun μ : Measure Walsh.Group => μ N) heq118 rw [Measure.add_apply, hp, hn, add_zero] at hev119 exact hνN hev120121/-- The Walsh coefficient functional on actual Haar L1. -/122def fourierFunctional (F : Finset ℕ) : Lp ℝ 1 haar →L[ℝ] ℝ :=123 (ContinuousLinearMap.mul ℝ ℝ).lpPairing haar ∞ 1 (characterLp ∞ F)124125theorem fourierFunctional_apply (F : Finset ℕ) (f : Lp ℝ 1 haar) :126 fourierFunctional F f = ∫ x, character F x * f x ∂haar := by127 rw [fourierFunctional, ContinuousLinearMap.lpPairing_eq_integral]128 apply integral_congr_ae129 filter_upwards [coeFn_characterLp ∞ F] with x hx130 simp only [ContinuousLinearMap.mul_apply', hx]131132theorem fourierFunctional_character (F H : Finset ℕ) :133 fourierFunctional F (characterLp 1 H) = if F = H then 1 else 0 := by134 rw [fourierFunctional_apply, ← integral_character_mul F H]135 apply integral_congr_ae136 filter_upwards [coeFn_characterLp 1 H] with x hx137 rw [hx]138139/-- The Fourier functionals diagonalize probability convolution on all of L1. -/140theorem fourierFunctional_convolution (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]141 (F : Finset ℕ) :142 (fourierFunctional F).comp (convolutionL1 ν) = coefficient ν F • fourierFunctional F := by143 apply ContinuousLinearMap.ext_on (dense_span_characterLp 1 (by norm_num))144 rintro x ⟨H, rfl⟩145 simp only [ContinuousLinearMap.comp_apply, convolutionL1_character, map_smul,146 smul_apply, fourierFunctional_character, smul_eq_mul]147 split_ifs with h148 · rw [h]149 · simp150151theorem fourierFunctional_convolution_apply (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]152 (F : Finset ℕ) (f : Lp ℝ 1 haar) :153 fourierFunctional F (convolutionL1 ν f) = coefficient ν F * fourierFunctional F f := by154 exact congrArg (fun T : Lp ℝ 1 haar →L[ℝ] ℝ => T f)155 (fourierFunctional_convolution ν F)156157theorem fourierFunctional_indicator (F : Finset ℕ) (A : Set Walsh.Group)158 (hA : MeasurableSet A) :159 fourierFunctional F (RNPBridge.indicatorL1 haar A) = ∫ x in A, character F x ∂haar := by160 rw [fourierFunctional_apply, ← integral_indicator hA]161 apply integral_congr_ae162 filter_upwards [RNPBridge.indicatorL1_coeFn haar hA] with x hx163 rw [hx]164 by_cases hxA : x ∈ A <;> simp [hxA]165166/-- A setwise Bochner density for convolution forces every Walsh coefficient of that density. -/167theorem fourier_setwise_density (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]168 {b : Walsh.Group → Lp ℝ 1 haar} (hb : Integrable b haar)169 (hrep : ∀ A : Set Walsh.Group, MeasurableSet A →170 convolutionL1 ν (RNPBridge.indicatorL1 haar A) = ∫ x in A, b x ∂haar)171 (F : Finset ℕ) :172 (fun x => fourierFunctional F (b x)) =ᵐ[haar]173 fun x => coefficient ν F * character F x := by174 apply Integrable.ae_eq_of_forall_setIntegral_eq _ _175 ((fourierFunctional F).integrable_comp hb) ((integrable_character F).const_mul _)176 intro A hA _177 rw [(fourierFunctional F).integral_comp_comm hb.integrableOn, ← hrep A hA,178 fourierFunctional_convolution_apply, fourierFunctional_indicator F A hA,179 integral_const_mul]180181theorem integral_character_translate (F : Finset ℕ) (f : Lp ℝ 1 haar) (s : Walsh.Group) :182 ∫ x, character F x * f (s * x) ∂haar = character F s * fourierFunctional F f := by183 calc184 _ = ∫ x, character F s * (character F (s * x) * f (s * x)) ∂haar := by185 apply integral_congr_ae186 exact ae_of_all _ (fun x => by187 simp only [character_mul, ← mul_assoc, character_mul_self, one_mul])188 _ = character F s * ∫ x, character F (s * x) * f (s * x) ∂haar :=189 integral_const_mul _ _190 _ = character F s * ∫ x, character F x * f x ∂haar := by191 rw [integral_mul_left_eq_self (fun x => character F x * f x) s]192 _ = _ := by rw [fourierFunctional_apply]193194/-- Countability of the Walsh system turns a setwise L1-valued density into a scalar density195with the same Fourier coefficients as the convolving measure. -/196theorem exists_integrable_density_of_setwise_representation197 (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]198 {b : Walsh.Group → Lp ℝ 1 haar} (hb : Integrable b haar)199 (hrep : ∀ A : Set Walsh.Group, MeasurableSet A →200 convolutionL1 ν (RNPBridge.indicatorL1 haar A) = ∫ x in A, b x ∂haar) :201 ∃ g : Walsh.Group → ℝ, Integrable g haar ∧202 ∀ F : Finset ℕ, ∫ x, character F x * g x ∂haar = ∫ x, character F x ∂ν := by203 have hsim : ∀ᵐ x ∂haar, ∀ F : Finset ℕ,204 fourierFunctional F (b x) = coefficient ν F * character F x := by205 exact ae_all_iff.mpr (fun F => fourier_setwise_density ν hb hrep F)206 obtain ⟨s, hs⟩ := hsim.exists207 refine ⟨fun x => b s (s * x), (L1.integrable_coeFn (b s)).comp_mul_left s, ?_⟩208 intro F209 rw [integral_character_translate, hs F]210 calc211 character F s * (coefficient ν F * character F s) =212 coefficient ν F * (character F s * character F s) := by ring213 _ = _ := by rw [character_mul_self, mul_one]; rfl214215/-- Singular probability convolution admits no integrable setwise Bochner density into L1. -/216theorem no_setwise_density_of_null_carrier217 (ν : Measure Walsh.Group) [IsProbabilityMeasure ν] (N : Set Walsh.Group)218 (hmN : haar N = 0) (hνN : ν N ≠ 0) :219 ¬ ∃ b : Walsh.Group → Lp ℝ 1 haar, Integrable b haar ∧220 ∀ A : Set Walsh.Group, MeasurableSet A →221 convolutionL1 ν (RNPBridge.indicatorL1 haar A) = ∫ x in A, b x ∂haar := by222 rintro ⟨b, hb, hrep⟩223 exact no_integrable_density_of_null_carrier ν N hmN hνN224 (exists_integrable_density_of_setwise_representation ν hb hrep)225226/-- Every Banach space through which singular probability convolution factors fails the227reviewed Radon–Nikodym property. -/228theorem not_RNP_of_convolution_factorization229 (ν : Measure Walsh.Group) [IsProbabilityMeasure ν] (N : Set Walsh.Group)230 (hmN : haar N = 0) (hνN : ν N ≠ 0)231 {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]232 (S : Lp ℝ 1 haar →L[ℝ] E) (T : E →L[ℝ] Lp ℝ 1 haar)233 (hfac : T.comp S = convolutionL1 ν) : ¬ HasRadonNikodymProperty.{u, 0} E := by234 intro hE235 obtain ⟨b, hb, hrep⟩ := RNPBridge.exists_setwise_density_of_RNP haar hE S236 apply no_setwise_density_of_null_carrier ν N hmN hνN237 refine ⟨fun x => T (b x), T.integrable_comp hb, ?_⟩238 intro A hA239 rw [T.integral_comp_comm hb.integrableOn, ← hrep A hA, ← hfac]240 rfl241242end SingularConvolution243end PL1244