PL1/WalshExpectations.lean
All source files · Download exact source
SHA-256: 784f2081f3cc022b8dde31013a6661ad2e183fa7e6b446cd9ea82f36aa62513f
1import PL1.ConcreteResolvents2import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension34/-! # Actual finite-coordinate averaging on the sign group -/56noncomputable section7open MeasureTheory Filter8open scoped ENNReal NNReal Topology BigOperators910namespace PL1.WalshExpectations1112open Walsh1314/-- Erase the first m coordinates, retaining the tail. -/15def tailProjection (m : ℕ) (x : Walsh.Group) : Walsh.Group :=16 fun j => if j < m then 1 else x j1718theorem continuous_tailProjection (m : ℕ) : Continuous (tailProjection m) := by19 apply continuous_pi20 intro j21 by_cases h : j < m22 · simpa only [tailProjection, h, ite_true] using continuous_const23 · simpa only [tailProjection, h, ite_false] using continuous_apply j2425theorem character_tailProjection (m : ℕ) (F : Finset ℕ) (x : Walsh.Group) :26 character F (tailProjection m x) = character (F.filter (fun j => m ≤ j)) x := by27 unfold character28 rw [Finset.prod_filter]29 apply Finset.prod_congr rfl30 intro j hj31 by_cases h : j < m32 · simp [tailProjection, h, Nat.not_le.mpr h]33 · simp [tailProjection, h, Nat.le_of_not_gt h]3435/-- Haar probability on the subgroup whose first m coordinates are one. -/36def tailMeasure (m : ℕ) : Measure Walsh.Group := haar.map (tailProjection m)3738instance (m : ℕ) : IsProbabilityMeasure (tailMeasure m) := by39 unfold tailMeasure40 infer_instance4142theorem coefficient_tailMeasure (m : ℕ) (F : Finset ℕ) :43 coefficient (tailMeasure m) F = if F ⊆ Finset.range m then 1 else 0 := by44 rw [coefficient, tailMeasure, integral_map (continuous_tailProjection m).measurable.aemeasurable45 (continuous_character F).aestronglyMeasurable]46 simp_rw [character_tailProjection]47 rw [Walsh.integral_character]48 have h : F.filter (fun j => m ≤ j) = ∅ ↔ F ⊆ Finset.range m := by49 simp only [Finset.filter_eq_empty_iff, Finset.subset_iff, Finset.mem_range]50 constructor51 · intro h j hj52 exact Nat.lt_of_not_ge (h hj)53 · intro h j hj54 exact Nat.not_le.mpr (h hj)55 simp only [h]5657variable (K : Type*) [RCLike K]5859/-- The genuine contractive finite-coordinate expectation on Haar L1. -/60def expectationL1 (m : ℕ) : Lp K 1 haar →L[K] Lp K 1 haar :=61 convolutionL1 (tailMeasure m)6263theorem norm_expectationL1_le_one (m : ℕ) : ‖expectationL1 K m‖ ≤ 1 :=64 norm_convolutionL1_le_one (tailMeasure m)6566theorem expectationL1_character (m : ℕ) (F : Finset ℕ) :67 expectationL1 K m (scalarCharacterLp K 1 F) =68 if F ⊆ Finset.range m then scalarCharacterLp K 1 F else 0 := by69 rw [expectationL1, convolutionL1_scalarCharacter, coefficient_tailMeasure]70 split_ifs <;> simp7172/-- Finite-coordinate averaging commutes with every probability convolution. -/73theorem expectationL1_commute (m : ℕ) (ν : Measure Walsh.Group) [IsProbabilityMeasure ν] :74 (expectationL1 K m).comp (convolutionL1 ν) =75 (convolutionL1 ν).comp (expectationL1 K m) := by76 apply continuousLinearMap_ext_on_scalarCharacterL177 intro F78 simp only [ContinuousLinearMap.comp_apply, convolutionL1_scalarCharacter,79 map_smul, expectationL1_character]80 split_ifs81 · exact (convolutionL1_scalarCharacter ν F).symm82 · simp8384theorem expectationL1_resolvent_commute (m : ℕ) (rates : ℕ → ℝ≥0) (t : Noise.PositiveTime) :85 (expectationL1 K m).comp (Noise.resolventL1 K rates t) =86 (Noise.resolventL1 K rates t).comp (expectationL1 K m) := by87 let := Noise.isProbabilityMeasure_resolventMeasure rates t.property88 exact expectationL1_commute K m (Noise.resolventMeasure rates t)8990theorem expectationL1_comp_of_le (m n : ℕ) (hmn : m ≤ n) :91 (expectationL1 K m).comp (expectationL1 K n) = expectationL1 K m := by92 apply continuousLinearMap_ext_on_scalarCharacterL193 intro F94 simp only [ContinuousLinearMap.comp_apply, expectationL1_character]95 by_cases hm : F ⊆ Finset.range m96 · have hn : F ⊆ Finset.range n := hm.trans (Finset.range_mono hmn)97 simp [hm, hn, expectationL1_character]98 · by_cases hn : F ⊆ Finset.range n <;> simp [hm, hn, expectationL1_character]99100theorem expectationL1_idempotent (m : ℕ) :101 (expectationL1 K m).comp (expectationL1 K m) = expectationL1 K m :=102 expectationL1_comp_of_le K m m le_rfl103104/-- These actual contractions converge strongly to the identity. -/105theorem tendsto_expectationL1 (f : Lp K 1 haar) :106 Tendsto (fun m => expectationL1 K m f) atTop (𝓝 f) := by107 apply tendsto_apply_of_dense_span (scalarCharacterLp K 1)108 (dense_span_scalarCharacterLp K 1 (by norm_num)) (expectationL1 K)109 (ContinuousLinearMap.id K _) atTop 1 (norm_expectationL1_le_one K)110 intro F111 apply tendsto_const_nhds.congr'112 filter_upwards [eventually_ge_atTop (F.sup id + 1)] with m hm113 have hF : F ⊆ Finset.range m := by114 intro j hj115 simp only [Finset.mem_range]116 exact lt_of_le_of_lt (Finset.le_sup (f := id) hj) (by omega)117 simp only [expectationL1_character, hF, ite_true]118 rfl119120/-- The finite-dimensional space of Walsh polynomials using the first m coordinates. -/121def finiteSpan (m : ℕ) : Submodule K (Lp K 1 haar) :=122 Submodule.span K ((scalarCharacterLp K 1) '' ((Finset.range m).powerset : Set (Finset ℕ)))123124instance (m : ℕ) : FiniteDimensional K (finiteSpan K m) :=125 FiniteDimensional.span_of_finite K126 ((Finset.finite_toSet (Finset.range m).powerset).image (scalarCharacterLp K 1))127128theorem character_mem_finiteSpan (m : ℕ) (F : Finset ℕ) (hF : F ⊆ Finset.range m) :129 scalarCharacterLp K 1 F ∈ finiteSpan K m := by130 apply Submodule.subset_span131 exact ⟨F, Finset.mem_powerset.mpr hF, rfl⟩132133theorem expectationL1_mem_finiteSpan (m : ℕ) (f : Lp K 1 haar) :134 expectationL1 K m f ∈ finiteSpan K m := by135 let S := (finiteSpan K m).comap (expectationL1 K m).toLinearMap136 have hclosed : IsClosed (S : Set (Lp K 1 haar)) :=137 (finiteSpan K m).closed_of_finiteDimensional.preimage (expectationL1 K m).continuous138 have hs : Submodule.span K (Set.range (scalarCharacterLp K 1)) ≤ S := by139 apply Submodule.span_le.mpr140 rintro x ⟨F, rfl⟩141 change expectationL1 K m (scalarCharacterLp K 1 F) ∈ finiteSpan K m142 rw [expectationL1_character]143 split_ifs with hF144 · exact character_mem_finiteSpan K m F hF145 · exact Submodule.zero_mem _146 exact hclosed.closure_subset_iff.mpr hs (dense_span_scalarCharacterLp K 1 (by norm_num) f)147148theorem range_expectationL1_le (m : ℕ) :149 (expectationL1 K m).range ≤ finiteSpan K m := by150 rintro x ⟨f, rfl⟩151 exact expectationL1_mem_finiteSpan K m f152153/-- The actual expectation operator has finite rank. -/154instance (m : ℕ) : FiniteDimensional K (expectationL1 K m).range :=155 FiniteDimensional.of_injective (Submodule.inclusion (range_expectationL1_le K m))156 (Submodule.inclusion_injective _)157158end PL1.WalshExpectations159