PL1/WalshBlocks.lean
All source files · Download exact source
SHA-256: 9455f938c2af99b8b05f4d8193ed4762d17f249e4e58b22a6f4a80938ae555e4
1import PL1.WalshExpectations2import PL1.LpInclusions3import Mathlib.LinearAlgebra.Dimension.Constructions45/-! # Exact dimensions of the finite-coordinate Walsh spaces -/67noncomputable section8open MeasureTheory9open scoped ENNReal Topology BigOperators1011namespace PL1.WalshBlocks1213open Walsh WalshExpectations1415variable (K : Type*) [RCLike K]1617theorem l2ToL1_injective : Function.Injective (l2ToL1 (𝕜 := K)) := by18 intro f g h19 apply Lp.ext20 filter_upwards [ProbabilityLp.coeFn_inclusion haar 1 2 (by norm_num) f,21 ProbabilityLp.coeFn_inclusion haar 1 2 (by norm_num) g] with x hf hg22 change l2ToL1 f x = f x at hf23 change l2ToL1 g x = g x at hg24 rw [← hf, ← hg, h]2526/-- Walsh characters remain linearly independent in actual L1. -/27theorem linearIndependent_characterL1 : LinearIndependent K (scalarCharacterLp K 1) := by28 have h := (orthonormal_scalarCharacterL2 K).linearIndependent.map'29 (l2ToL1 (𝕜 := K)).toLinearMap (LinearMap.ker_eq_bot.mpr (l2ToL1_injective K))30 simpa only [Function.comp_def, ContinuousLinearMap.coe_coe, l2ToL1_scalarCharacter] using h3132theorem range_expectationL1_eq (m : ℕ) :33 (expectationL1 K m).range = finiteSpan K m := by34 apply le_antisymm (range_expectationL1_le K m)35 apply Submodule.span_le.mpr36 rintro x ⟨F, hF, rfl⟩37 refine ⟨scalarCharacterLp K 1 F, ?_⟩38 change expectationL1 K m (scalarCharacterLp K 1 F) = scalarCharacterLp K 1 F39 simp only [expectationL1_character, Finset.mem_powerset.mp hF, ite_true]4041theorem finiteSpan_eq_span_range (m : ℕ) :42 finiteSpan K m = Submodule.span K43 (Set.range (fun F : (Finset.range m).powerset => scalarCharacterLp K 1 F)) := by44 unfold finiteSpan45 congr 146 ext x47 constructor48 · rintro ⟨F, hF, rfl⟩49 exact ⟨⟨F, hF⟩, rfl⟩50 · rintro ⟨F, rfl⟩51 exact ⟨F, F.property, rfl⟩5253theorem finrank_finiteSpan (m : ℕ) : Module.finrank K (finiteSpan K m) = 2 ^ m := by54 rw [finiteSpan_eq_span_range]55 have h := (linearIndependent_characterL1 K).comp56 (fun F : (Finset.range m).powerset => (F : Finset ℕ)) Subtype.val_injective57 simp only [Function.comp_def] at h58 rw [finrank_span_eq_card h]59 simp6061/-- The genuine m-coordinate expectation has rank exactly 2^m. -/62theorem finrank_range_expectationL1 (m : ℕ) :63 Module.finrank K (expectationL1 K m).range = 2 ^ m := by64 rw [range_expectationL1_eq, finrank_finiteSpan]6566/-- The next-coordinate Walsh block. -/67def blockL1 (m : ℕ) : Lp K 1 haar →L[K] Lp K 1 haar :=68 expectationL1 K (m + 1) - expectationL1 K m6970theorem blockL1_character (m : ℕ) (F : Finset ℕ) :71 blockL1 K m (scalarCharacterLp K 1 F) =72 if m ∈ F ∧ F ⊆ Finset.range (m + 1) then scalarCharacterLp K 1 F else 0 := by73 simp only [blockL1, sub_apply, expectationL1_character]74 by_cases hs : F ⊆ Finset.range (m + 1)75 · by_cases hm : m ∈ F76 · have hn : ¬ F ⊆ Finset.range m := by77 intro h78 exact (Nat.lt_irrefl m) (Finset.mem_range.mp (h hm))79 simp [hs, hm, hn]80 · have hn : F ⊆ Finset.range m := by81 intro j hj82 have hjm := Finset.mem_range.mp (hs hj)83 have hjne : j ≠ m := by intro h; exact hm (h ▸ hj)84 exact Finset.mem_range.mpr (by omega)85 simp [hs, hm, hn]86 · have hn : ¬ F ⊆ Finset.range m :=87 fun h => hs (h.trans (Finset.range_mono (Nat.le_succ m)))88 simp [hs, hn]8990def blockFamily (m : ℕ) (F : (Finset.range m).powerset) : Lp K 1 haar :=91 scalarCharacterLp K 1 (insert m F)9293def blockSpan (m : ℕ) : Submodule K (Lp K 1 haar) :=94 Submodule.span K (Set.range (blockFamily K m))9596theorem not_mem_support (m : ℕ) (F : (Finset.range m).powerset) : m ∉ (F : Finset ℕ) := by97 intro h98 exact (Nat.lt_irrefl m) (Finset.mem_range.mp (Finset.mem_powerset.mp F.property h))99100theorem blockSupport_injective (m : ℕ) :101 Function.Injective (fun F : (Finset.range m).powerset => insert m (F : Finset ℕ)) := by102 intro F H h103 apply Subtype.ext104 have he := congrArg (fun S : Finset ℕ => S.erase m) h105 simpa [not_mem_support m F, not_mem_support m H] using he106107theorem linearIndependent_blockFamily (m : ℕ) : LinearIndependent K (blockFamily K m) :=108 (linearIndependent_characterL1 K).comp _ (blockSupport_injective m)109110instance (m : ℕ) : FiniteDimensional K (blockSpan K m) :=111 FiniteDimensional.span_of_finite K (Set.finite_range (blockFamily K m))112113theorem finrank_blockSpan (m : ℕ) : Module.finrank K (blockSpan K m) = 2 ^ m := by114 rw [blockSpan, finrank_span_eq_card (linearIndependent_blockFamily K m)]115 simp116117theorem character_mem_blockSpan (m : ℕ) (F : Finset ℕ)118 (hm : m ∈ F) (hF : F ⊆ Finset.range (m + 1)) :119 scalarCharacterLp K 1 F ∈ blockSpan K m := by120 apply Submodule.subset_span121 have he : F.erase m ⊆ Finset.range m := by122 intro j hj123 have hjF := Finset.mem_of_mem_erase hj124 have hjne := Finset.ne_of_mem_erase hj125 have hjm := Finset.mem_range.mp (hF hjF)126 exact Finset.mem_range.mpr (by omega)127 refine ⟨⟨F.erase m, Finset.mem_powerset.mpr he⟩, ?_⟩128 change scalarCharacterLp K 1 (insert m (F.erase m)) = _129 rw [Finset.insert_erase hm]130131theorem blockL1_mem_blockSpan (m : ℕ) (f : Lp K 1 haar) :132 blockL1 K m f ∈ blockSpan K m := by133 let S := (blockSpan K m).comap (blockL1 K m).toLinearMap134 have hc : IsClosed (S : Set (Lp K 1 haar)) :=135 (blockSpan K m).closed_of_finiteDimensional.preimage (blockL1 K m).continuous136 have hs : Submodule.span K (Set.range (scalarCharacterLp K 1)) ≤ S := by137 apply Submodule.span_le.mpr138 rintro x ⟨F, rfl⟩139 change blockL1 K m (scalarCharacterLp K 1 F) ∈ blockSpan K m140 rw [blockL1_character]141 split_ifs with h142 · exact character_mem_blockSpan K m F h.1 h.2143 · exact Submodule.zero_mem _144 exact hc.closure_subset_iff.mpr hs (dense_span_scalarCharacterLp K 1 (by norm_num) f)145146theorem blockL1_blockFamily (m : ℕ) (F : (Finset.range m).powerset) :147 blockL1 K m (blockFamily K m F) = blockFamily K m F := by148 rw [blockFamily, blockL1_character]149 have hs : insert m (F : Finset ℕ) ⊆ Finset.range (m + 1) := by150 apply Finset.insert_subset_iff.mpr151 exact ⟨Finset.mem_range.mpr (Nat.lt_succ_self m),152 (Finset.mem_powerset.mp F.property).trans (Finset.range_mono (Nat.le_succ m))⟩153 simp only [Finset.mem_insert_self, hs, and_self, ite_true]154155theorem range_blockL1_eq (m : ℕ) : (blockL1 K m).range = blockSpan K m := by156 apply le_antisymm157 · rintro x ⟨f, rfl⟩158 exact blockL1_mem_blockSpan K m f159 · apply Submodule.span_le.mpr160 rintro x ⟨F, rfl⟩161 exact ⟨blockFamily K m F, blockL1_blockFamily K m F⟩162163theorem finrank_range_blockL1 (m : ℕ) : Module.finrank K (blockL1 K m).range = 2 ^ m := by164 rw [range_blockL1_eq, finrank_blockSpan]165166end PL1.WalshBlocks167