PL1/WalshModel.lean
All source files · Download exact source
SHA-256: 6f46e1cc0f20ab916a5413f1173bbebb95d74b653cec85117d942a33f6d54da5
1import Mathlib.Topology.Instances.ZMod2import Mathlib.Data.ZMod.Basic3import Mathlib.MeasureTheory.Measure.Haar.Basic4import Mathlib.MeasureTheory.Group.Integral5import Mathlib.Tactic.FinCases6import Mathlib.Tactic.NormNum7import Mathlib.Data.Finset.SymmDiff8import Mathlib.MeasureTheory.Function.L2Space9import Mathlib.Topology.ContinuousMap.StoneWeierstrass10import Mathlib.MeasureTheory.Function.ContinuousMapDense11import Mathlib.Analysis.InnerProductSpace.l2Space1213/-!14# The countable sign group and its Walsh characters1516The two-element group is represented by `Multiplicative (ZMod 2)`.17Its elements 0 and 1 correspond to the signs +1 and -1. Thus the group below18is precisely the countable sign group used in the manuscript, with zero-based19coordinates. Its measure is the Haar measure normalized on the whole compact20group, without an assumption of independence.21-/2223noncomputable section2425open MeasureTheory TopologicalSpace26open scoped BigOperators ENNReal symmDiff2728namespace PL129namespace Walsh3031abbrev Sign := Multiplicative (ZMod 2)32instance : MeasurableSpace Sign := borel Sign33instance : BorelSpace Sign := ⟨rfl⟩3435/-- The product uses Mathlib's canonical Pi measurable space. Since the index36is countable and the factors are finite discrete spaces, it is also Borel. -/37abbrev Group := ℕ → Sign3839def haar : Measure Group := Measure.haarMeasure ⊤4041instance : IsProbabilityMeasure haar := by42 constructor43 simpa only [haar, PositiveCompacts.coe_top] using44 (Measure.haarMeasure_self (K₀ := (⊤ : PositiveCompacts Group)))4546instance : Measure.IsHaarMeasure haar := by47 unfold haar48 infer_instance4950instance : haar.Regular := by51 unfold haar52 infer_instance5354def signValue (a : Sign) : ℝ := if a.toAdd = 0 then 1 else -15556@[simp] theorem signValue_one : signValue 1 = 1 := by57 simp [signValue]5859set_option backward.isDefEq.respectTransparency false in60theorem signValue_mul (a b : Sign) : signValue (a * b) = signValue a * signValue b := by61 change (if a.toAdd + b.toAdd = 0 then (1 : ℝ) else -1) = _62 generalize ha : a.toAdd = x63 generalize hb : b.toAdd = y64 simp only [signValue, ha, hb]65 fin_cases x <;> fin_cases y <;> norm_num [Fin.ext_iff, Fin.add_def]66 decide6768@[simp] theorem norm_signValue (a : Sign) : ‖signValue a‖ = 1 := by69 unfold signValue70 split <;> norm_num7172@[simp] theorem signValue_mul_self (a : Sign) : signValue a * signValue a = 1 := by73 unfold signValue74 split <;> norm_num7576theorem signValue_eq_one_or_neg_one (a : Sign) : signValue a = 1 ∨ signValue a = -1 := by77 unfold signValue78 split <;> simp7980set_option backward.isDefEq.respectTransparency false in81theorem signValue_injective : Function.Injective signValue := by82 intro a b hab83 have h : a.toAdd = b.toAdd := by84 generalize hx : a.toAdd = x85 generalize hy : b.toAdd = y86 have hh : (if x = 0 then (1 : ℝ) else -1) = if y = 0 then 1 else -1 := by87 simpa only [signValue, hx, hy] using hab88 fin_cases x <;> fin_cases y <;> norm_num [Fin.ext_iff] at *89 exact congrArg Multiplicative.ofAdd h9091def character (F : Finset ℕ) (x : Group) : ℝ := ∏ j ∈ F, signValue (x j)9293@[simp] theorem character_empty (x : Group) : character ∅ x = 1 := by94 simp [character]9596@[simp] theorem character_one (F : Finset ℕ) : character F 1 = 1 := by97 simp [character]9899@[simp] theorem character_singleton (j : ℕ) (x : Group) :100 character {j} x = signValue (x j) := by101 simp [character]102103theorem character_mul (F : Finset ℕ) (x y : Group) :104 character F (x * y) = character F x * character F y := by105 simp only [character, Pi.mul_apply, signValue_mul, Finset.prod_mul_distrib]106107@[simp] theorem norm_character (F : Finset ℕ) (x : Group) :108 ‖character F x‖ = 1 := by109 rw [character, norm_prod]110 simp only [norm_signValue, Finset.prod_const_one]111112@[simp] theorem character_mul_self (F : Finset ℕ) (x : Group) :113 character F x * character F x = 1 := by114 rw [character, ← Finset.prod_mul_distrib]115 simp116117/-- The Walsh multiplication law: repeated coordinates cancel. -/118theorem character_symmDiff (F H : Finset ℕ) (x : Group) :119 character (F ∆ H) x = character F x * character H x := by120 have hd : Disjoint (F ∆ H) (F ∩ H) := by121 apply Finset.disjoint_left.mpr122 intro j hj hk123 rcases Finset.mem_symmDiff.mp hj with h | h124 · exact h.2 (Finset.mem_inter.mp hk).2125 · exact h.2 (Finset.mem_inter.mp hk).1126 have hu : (F ∆ H) ∪ (F ∩ H) = F ∪ H := by127 ext j128 by_cases hjF : j ∈ F <;> by_cases hjH : j ∈ H <;>129 simp [Finset.mem_symmDiff, hjF, hjH]130 have hp : character (F ∆ H) x * character (F ∩ H) x = character (F ∪ H) x := by131 simpa only [character, hu] using132 (Finset.prod_union hd (f := fun j => signValue (x j))).symm133 calc134 character (F ∆ H) x =135 (character (F ∆ H) x * character (F ∩ H) x) * character (F ∩ H) x := by136 rw [mul_assoc, character_mul_self, mul_one]137 _ = character (F ∪ H) x * character (F ∩ H) x := by rw [hp]138 _ = character F x * character H x := by139 exact Finset.prod_union_inter140141theorem continuous_character (F : Finset ℕ) : Continuous (character F) := by142 apply continuous_finsetProd143 intro j hj144 exact (continuous_of_discreteTopology : Continuous signValue).comp145 (continuous_apply j : Continuous (fun x : Group => x j))146147theorem integrable_character (F : Finset ℕ) : Integrable (character F) haar := by148 apply (integrable_const (1 : ℝ)).mono' (continuous_character F).aestronglyMeasurable149 filter_upwards [] with x150 exact le_of_eq (norm_character F x)151152/-- The group element which flips only coordinate j. -/153def flip (j : ℕ) : Group := Function.update 1 j (Multiplicative.ofAdd 1)154155theorem character_flip_of_mem {F : Finset ℕ} {j : ℕ} (hj : j ∈ F) :156 character F (flip j) = -1 := by157 rw [character, Finset.prod_eq_single j]158 · norm_num [flip, signValue]159 · intro i hi hij160 simp [flip, Function.update_of_ne hij, signValue]161 · intro h162 exact (h hj).elim163164theorem integral_character_eq_zero {F : Finset ℕ} (hF : F.Nonempty) :165 ∫ x, character F x ∂haar = 0 := by166 obtain ⟨j, hj⟩ := hF167 apply integral_eq_zero_of_mul_left_eq_neg (g := flip j)168 intro x169 rw [character_mul, character_flip_of_mem hj, neg_one_mul]170171theorem integral_character (F : Finset ℕ) :172 ∫ x, character F x ∂haar = if F = ∅ then 1 else 0 := by173 by_cases hF : F = ∅174 · simp [hF]175 · simp [hF, integral_character_eq_zero (Finset.nonempty_iff_ne_empty.mpr hF)]176177/-- Orthogonality with respect to the actual normalized Haar measure. -/178theorem integral_character_mul (F H : Finset ℕ) :179 ∫ x, character F x * character H x ∂haar = if F = H then 1 else 0 := by180 simp_rw [← character_symmDiff]181 simp [integral_character]182183@[simp] theorem character_inv (F : Finset ℕ) (x : Group) :184 character F x⁻¹ = character F x := by185 have h : character F x⁻¹ * character F x = 1 := by186 rw [← character_mul, inv_mul_cancel, character_one]187 calc188 character F x⁻¹ = (character F x⁻¹ * character F x) * character F x := by189 rw [mul_assoc, character_mul_self, mul_one]190 _ = character F x := by rw [h, one_mul]191192/-- Fourier coefficient of a positive measure at a Walsh character. -/193def coefficient (τ : Measure Group) (F : Finset ℕ) : ℝ :=194 ∫ x, character F x ∂τ195196/-- Convolution on raw functions, before the later descent to equivalence classes in Lp. -/197def convolution (τ : Measure Group) (f : Group → ℝ) (x : Group) : ℝ :=198 ∫ y, f (x * y⁻¹) ∂τ199200/-- Each Walsh character is an eigenfunction of convolution. -/201theorem convolution_character (τ : Measure Group) (F : Finset ℕ) (x : Group) :202 convolution τ (character F) x = coefficient τ F * character F x := by203 simp only [convolution, character_mul, character_inv, coefficient]204 rw [integral_const_mul, mul_comm]205206/-- Walsh characters belong to every Lp space, including L-infinity. -/207theorem memLp_character (p : ℝ≥0∞) (F : Finset ℕ) : MemLp (character F) p haar := by208 apply MemLp.of_bound (continuous_character F).aestronglyMeasurable 1209 filter_upwards [] with x210 exact le_of_eq (norm_character F x)211212/-- The actual a.e.-equivalence class of a Walsh character. -/213def characterLp (p : ℝ≥0∞) (F : Finset ℕ) : Lp ℝ p haar :=214 (memLp_character p F).toLp (character F)215216theorem coeFn_characterLp (p : ℝ≥0∞) (F : Finset ℕ) :217 characterLp p F =ᵐ[haar] character F :=218 (memLp_character p F).coeFn_toLp219220theorem inner_characterL2 (F H : Finset ℕ) :221 inner ℝ (characterLp 2 F) (characterLp 2 H) = if F = H then 1 else 0 := by222 rw [L2.inner_def]223 calc224 (∫ x, inner ℝ (characterLp 2 F x) (characterLp 2 H x) ∂haar) =225 ∫ x, character F x * character H x ∂haar := by226 apply integral_congr_ae227 filter_upwards [coeFn_characterLp 2 F, coeFn_characterLp 2 H] with x hx hy228 rw [hx, hy]229 simp [RCLike.inner_apply, mul_comm]230 _ = if F = H then 1 else 0 := integral_character_mul F H231232/-- The Walsh vectors form an orthonormal family in genuine Haar L2. -/233theorem orthonormal_characterL2 : Orthonormal ℝ (characterLp 2) :=234 orthonormal_iff_ite.mpr inner_characterL2235236/-- A Walsh character as a continuous function on the compact sign group. -/237def characterContinuous (F : Finset ℕ) : C(Group, ℝ) :=238 ⟨character F, continuous_character F⟩239240@[simp] theorem characterContinuous_empty : characterContinuous ∅ = 1 := by241 ext x242 exact character_empty x243244theorem characterContinuous_symmDiff (F H : Finset ℕ) :245 characterContinuous (F ∆ H) = characterContinuous F * characterContinuous H := by246 ext x247 exact character_symmDiff F H x248249/-- The characters are a multiplicatively closed family containing 1. -/250def characterSubmonoid : Submonoid C(Group, ℝ) where251 carrier := Set.range characterContinuous252 one_mem' := ⟨∅, characterContinuous_empty⟩253 mul_mem' := by254 rintro f g ⟨F, rfl⟩ ⟨H, rfl⟩255 exact ⟨F ∆ H, characterContinuous_symmDiff F H⟩256257/-- The real algebra of finite Walsh polynomials. -/258def polynomials : Subalgebra ℝ C(Group, ℝ) :=259 Algebra.adjoin ℝ (characterSubmonoid : Set C(Group, ℝ))260261theorem polynomials_toSubmodule :262 polynomials.toSubmodule = Submodule.span ℝ (Set.range characterContinuous) := by263 rw [polynomials, Algebra.adjoin_eq_span, characterSubmonoid.closure_eq]264 rfl265266theorem polynomials_separatesPoints : polynomials.SeparatesPoints := by267 intro x y hxy268 have hn : ∃ j, x j ≠ y j := by269 by_contra h270 apply hxy271 funext j272 exact not_not.mp (fun hj => h ⟨j, hj⟩)273 obtain ⟨j, hj⟩ := hn274 refine ⟨character {j}, ⟨characterContinuous {j}, ?_, rfl⟩, ?_⟩275 · exact Algebra.subset_adjoin ⟨{j}, rfl⟩276 · simpa only [character_singleton] using fun h => hj (signValue_injective h)277278/-- Walsh polynomials are uniformly dense in all real continuous functions. -/279theorem polynomials_dense : Dense (polynomials : Set C(Group, ℝ)) := by280 have h := ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints281 polynomials polynomials_separatesPoints282 rw [SetLike.ext'_iff] at h283 change closure (polynomials : Set C(Group, ℝ)) = Set.univ at h284 exact dense_iff_closure_eq.mpr h285286theorem toLp_characterContinuous (p : ℝ≥0∞) [Fact (1 ≤ p)] (F : Finset ℕ) :287 ContinuousMap.toLp p haar ℝ (characterContinuous F) = characterLp p F := by288 apply Lp.ext289 exact (ContinuousMap.coeFn_toLp haar (characterContinuous F)).trans290 (coeFn_characterLp p F).symm291292/-- Finite real Walsh polynomials are dense in every genuine Lp, 1 ≤ p < infinity. -/293theorem dense_span_characterLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : p ≠ ∞) :294 Dense (Submodule.span ℝ (Set.range (characterLp p)) : Set (Lp ℝ p haar)) := by295 apply (ContinuousMap.toLp_denseRange (p := p) ℝ haar ℝ hp).dense_of_mapsTo296 (ContinuousMap.toLp p haar ℝ).continuous polynomials_dense297 intro f hf298 have hf' : f ∈ Submodule.span ℝ (Set.range characterContinuous) := by299 rw [← polynomials_toSubmodule]300 exact hf301 have him := Submodule.image_span_subset_span302 (ContinuousMap.toLp p haar ℝ).toLinearMap (Set.range characterContinuous) ⟨f, hf', rfl⟩303 have hr : (ContinuousMap.toLp p haar ℝ) '' Set.range characterContinuous =304 Set.range (characterLp p) := by305 rw [← Set.range_comp]306 exact congrArg Set.range (funext (toLp_characterContinuous p))307 simpa only [ContinuousLinearMap.coe_coe, hr] using him308309/-- The complete real Walsh Hilbert basis of Haar L2. -/310def hilbertBasis : HilbertBasis (Finset ℕ) ℝ (Lp ℝ 2 haar) :=311 HilbertBasis.mk orthonormal_characterL2 (by312 rw [Submodule.dense_iff_topologicalClosure_eq_top.mp313 (dense_span_characterLp 2 (by norm_num))])314315@[simp] theorem hilbertBasis_apply (F : Finset ℕ) :316 hilbertBasis F = characterLp 2 F := by317 exact congrFun (HilbertBasis.coe_mk _ _) F318319section Scalars320321variable (𝕜 : Type*) [RCLike 𝕜]322323/-- The same sign-valued character, over either scalar field of the manuscript. -/324def scalarCharacter (F : Finset ℕ) (x : Group) : 𝕜 := (character F x : ℝ)325326@[simp] theorem norm_scalarCharacter (F : Finset ℕ) (x : Group) :327 ‖scalarCharacter 𝕜 F x‖ = 1 := by328 simpa only [scalarCharacter, RCLike.norm_ofReal, Real.norm_eq_abs] using norm_character F x329330theorem continuous_scalarCharacter (F : Finset ℕ) : Continuous (scalarCharacter 𝕜 F) :=331 RCLike.continuous_ofReal.comp (continuous_character F)332333theorem scalarCharacter_symmDiff (F H : Finset ℕ) (x : Group) :334 scalarCharacter 𝕜 (F ∆ H) x = scalarCharacter 𝕜 F x * scalarCharacter 𝕜 H x := by335 simp only [scalarCharacter, character_symmDiff, RCLike.ofReal_mul]336337@[simp] theorem star_scalarCharacter (F : Finset ℕ) (x : Group) :338 star (scalarCharacter 𝕜 F x) = scalarCharacter 𝕜 F x := by339 simp [scalarCharacter]340341theorem memLp_scalarCharacter (p : ℝ≥0∞) (F : Finset ℕ) :342 MemLp (scalarCharacter 𝕜 F) p haar := by343 apply MemLp.of_bound (continuous_scalarCharacter 𝕜 F).aestronglyMeasurable 1344 filter_upwards [] with x345 exact le_of_eq (norm_scalarCharacter 𝕜 F x)346347def scalarCharacterLp (p : ℝ≥0∞) (F : Finset ℕ) : Lp 𝕜 p haar :=348 (memLp_scalarCharacter 𝕜 p F).toLp (scalarCharacter 𝕜 F)349350theorem coeFn_scalarCharacterLp (p : ℝ≥0∞) (F : Finset ℕ) :351 scalarCharacterLp 𝕜 p F =ᵐ[haar] scalarCharacter 𝕜 F :=352 (memLp_scalarCharacter 𝕜 p F).coeFn_toLp353354theorem inner_scalarCharacterL2 (F H : Finset ℕ) :355 inner 𝕜 (scalarCharacterLp 𝕜 2 F) (scalarCharacterLp 𝕜 2 H) =356 if F = H then 1 else 0 := by357 rw [L2.inner_def]358 calc359 (∫ x, inner 𝕜 (scalarCharacterLp 𝕜 2 F x) (scalarCharacterLp 𝕜 2 H x) ∂haar) =360 ∫ x, ((character F x * character H x : ℝ) : 𝕜) ∂haar := by361 apply integral_congr_ae362 filter_upwards [coeFn_scalarCharacterLp 𝕜 2 F, coeFn_scalarCharacterLp 𝕜 2 H] with x hx hy363 rw [hx, hy]364 simp [scalarCharacter, RCLike.inner_apply, mul_comm]365 _ = if F = H then 1 else 0 := by366 rw [integral_ofReal, integral_character_mul]367 split <;> simp368369theorem orthonormal_scalarCharacterL2 : Orthonormal 𝕜 (scalarCharacterLp 𝕜 2) :=370 orthonormal_iff_ite.mpr (inner_scalarCharacterL2 𝕜)371372def scalarCharacterContinuous (F : Finset ℕ) : C(Group, 𝕜) :=373 ⟨scalarCharacter 𝕜 F, continuous_scalarCharacter 𝕜 F⟩374375@[simp] theorem scalarCharacterContinuous_empty : scalarCharacterContinuous 𝕜 ∅ = 1 := by376 ext x377 simp [scalarCharacterContinuous, scalarCharacter]378379theorem scalarCharacterContinuous_symmDiff (F H : Finset ℕ) :380 scalarCharacterContinuous 𝕜 (F ∆ H) =381 scalarCharacterContinuous 𝕜 F * scalarCharacterContinuous 𝕜 H := by382 ext x383 exact scalarCharacter_symmDiff 𝕜 F H x384385@[simp] theorem star_scalarCharacterContinuous (F : Finset ℕ) :386 star (scalarCharacterContinuous 𝕜 F) = scalarCharacterContinuous 𝕜 F := by387 ext x388 exact star_scalarCharacter 𝕜 F x389390def scalarCharacterSubmonoid : Submonoid C(Group, 𝕜) where391 carrier := Set.range (scalarCharacterContinuous 𝕜)392 one_mem' := ⟨∅, scalarCharacterContinuous_empty 𝕜⟩393 mul_mem' := by394 rintro f g ⟨F, rfl⟩ ⟨H, rfl⟩395 exact ⟨F ∆ H, scalarCharacterContinuous_symmDiff 𝕜 F H⟩396397theorem star_scalarCharacterSubmonoid :398 star (scalarCharacterSubmonoid 𝕜 : Set C(Group, 𝕜)) =399 (scalarCharacterSubmonoid 𝕜 : Set C(Group, 𝕜)) := by400 ext f401 change star f ∈ Set.range (scalarCharacterContinuous 𝕜) ↔402 f ∈ Set.range (scalarCharacterContinuous 𝕜)403 constructor404 · rintro ⟨F, hF⟩405 exact ⟨F, by simpa only [star_scalarCharacterContinuous, star_star] using congrArg star hF⟩406 · rintro ⟨F, rfl⟩407 exact ⟨F, (star_scalarCharacterContinuous 𝕜 F).symm⟩408409/-- Finite Walsh polynomials over an RCLike field, closed under conjugation. -/410def scalarPolynomials : StarSubalgebra 𝕜 C(Group, 𝕜) :=411 StarAlgebra.adjoin 𝕜 (scalarCharacterSubmonoid 𝕜 : Set C(Group, 𝕜))412413theorem scalarPolynomials_toSubmodule :414 (scalarPolynomials 𝕜).toSubmodule =415 Submodule.span 𝕜 (Set.range (scalarCharacterContinuous 𝕜)) := by416 rw [scalarPolynomials, StarAlgebra.adjoin_eq_span, star_scalarCharacterSubmonoid,417 Set.union_self, (scalarCharacterSubmonoid 𝕜).closure_eq]418 rfl419420theorem scalarPolynomials_separatesPoints : (scalarPolynomials 𝕜).SeparatesPoints := by421 intro x y hxy422 have hn : ∃ j, x j ≠ y j := by423 by_contra h424 apply hxy425 funext j426 exact not_not.mp (fun hj => h ⟨j, hj⟩)427 obtain ⟨j, hj⟩ := hn428 refine ⟨scalarCharacter 𝕜 {j}, ⟨scalarCharacterContinuous 𝕜 {j}, ?_, rfl⟩, ?_⟩429 · exact StarAlgebra.subset_adjoin 𝕜 _ ⟨{j}, rfl⟩430 · intro h431 apply hj432 apply signValue_injective433 apply RCLike.ofReal_injective (K := 𝕜)434 simpa only [scalarCharacter, character_singleton] using h435436theorem scalarPolynomials_dense : Dense (scalarPolynomials 𝕜 : Set C(Group, 𝕜)) := by437 have h := ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints438 (scalarPolynomials 𝕜) (scalarPolynomials_separatesPoints 𝕜)439 rw [SetLike.ext'_iff] at h440 change closure (scalarPolynomials 𝕜 : Set C(Group, 𝕜)) = Set.univ at h441 exact dense_iff_closure_eq.mpr h442443theorem toLp_scalarCharacterContinuous (p : ℝ≥0∞) [Fact (1 ≤ p)] (F : Finset ℕ) :444 ContinuousMap.toLp p haar 𝕜 (scalarCharacterContinuous 𝕜 F) =445 scalarCharacterLp 𝕜 p F := by446 apply Lp.ext447 exact (ContinuousMap.coeFn_toLp haar (scalarCharacterContinuous 𝕜 F)).trans448 (coeFn_scalarCharacterLp 𝕜 p F).symm449450/-- Walsh density, simultaneously covering the real and complex cases. -/451theorem dense_span_scalarCharacterLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : p ≠ ∞) :452 Dense (Submodule.span 𝕜 (Set.range (scalarCharacterLp 𝕜 p)) : Set (Lp 𝕜 p haar)) := by453 apply (ContinuousMap.toLp_denseRange (p := p) 𝕜 haar 𝕜 hp).dense_of_mapsTo454 (ContinuousMap.toLp p haar 𝕜).continuous (scalarPolynomials_dense 𝕜)455 intro f hf456 have hf' : f ∈ Submodule.span 𝕜 (Set.range (scalarCharacterContinuous 𝕜)) := by457 rw [← scalarPolynomials_toSubmodule]458 exact hf459 have him := Submodule.image_span_subset_span460 (ContinuousMap.toLp p haar 𝕜).toLinearMap (Set.range (scalarCharacterContinuous 𝕜)) ⟨f, hf', rfl⟩461 have hr : (ContinuousMap.toLp p haar 𝕜) '' Set.range (scalarCharacterContinuous 𝕜) =462 Set.range (scalarCharacterLp 𝕜 p) := by463 rw [← Set.range_comp]464 exact congrArg Set.range (funext (toLp_scalarCharacterContinuous 𝕜 p))465 simpa only [ContinuousLinearMap.coe_coe, hr] using him466467/-- The complete Walsh Hilbert basis, over either scalar field. -/468def scalarHilbertBasis : HilbertBasis (Finset ℕ) 𝕜 (Lp 𝕜 2 haar) :=469 HilbertBasis.mk (orthonormal_scalarCharacterL2 𝕜) (by470 rw [Submodule.dense_iff_topologicalClosure_eq_top.mp471 (dense_span_scalarCharacterLp 𝕜 2 (by norm_num))])472473@[simp] theorem scalarHilbertBasis_apply (F : Finset ℕ) :474 scalarHilbertBasis 𝕜 F = scalarCharacterLp 𝕜 2 F := by475 exact congrFun (HilbertBasis.coe_mk _ _) F476477end Scalars478479end Walsh480end PL1481