On complemented subspaces of L1[0,1]L_1[0,1]

PL1/IntrinsicWalshBlocks.lean

All source files · Download exact source

SHA-256: 3887a94d5f4dff237f62103651adb0a39a0ce7b0e3df372dd9ddbc8099c09f3b

1import PL1.IntrinsicWalsh2import PL1.WalshBlocks34/-! # Exact dimensions of the intrinsic finite-coordinate projections and blocks -/56noncomputable section7open MeasureTheory Filter8open scoped ENNReal NNReal Topology BigOperators910namespace PL1.Noise1112open Walsh WalshExpectations IntrinsicGraph1314variable (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0)1516/-- Each Walsh character is an actual vector of the intrinsic space. The17zeroth resolvent column supplies it after multiplication by its inverse eigenvalue. -/18def intrinsicCharacter (F : Finset ℕ) : (dyadicSystem 𝕜 rates).IntrinsicSpace :=19  (((1 + rateSum rates F : ℝ) : 𝕜)) •20    (dyadicSystem 𝕜 rates).column 0 (scalarCharacterLp 𝕜 1 F)2122@[simp] theorem evalZero_intrinsicCharacter (F : Finset ℕ) :23    evalZero (dyadicSystem 𝕜 rates).analysis (intrinsicCharacter 𝕜 rates F) =24      scalarCharacterLp 𝕜 1 F := by25  rw [intrinsicCharacter, map_smul, DyadicSystem.evalZero_column]26  change ((1 + rateSum rates F : ℝ) : 𝕜) •27    resolventL1 𝕜 rates (dyadicTime 0) (scalarCharacterLp 𝕜 1 F) = _28  rw [resolventL1_scalarCharacter]29  simp only [dyadicTime, pow_zero, one_mul, smul_smul]30  rw [← RCLike.ofReal_mul, mul_inv_cancel₀31    (ne_of_gt (add_pos_of_pos_of_nonneg zero_lt_one (rateSum_nonneg rates F))),32    RCLike.ofReal_one, one_smul]3334theorem linearIndependent_intrinsicCharacter : LinearIndependent 𝕜 (intrinsicCharacter 𝕜 rates) := by35  apply LinearIndependent.of_comp (evalZero (dyadicSystem 𝕜 rates).analysis).toLinearMap36  simpa only [Function.comp_def, ContinuousLinearMap.coe_coe, evalZero_intrinsicCharacter] using37    WalshBlocks.linearIndependent_characterL1 𝕜3839theorem intrinsicExpectation_character (m : ℕ) (F : Finset ℕ) :40    intrinsicExpectation 𝕜 rates m (intrinsicCharacter 𝕜 rates F) =41      if F ⊆ Finset.range m then intrinsicCharacter 𝕜 rates F else 0 := by42  apply evalZero_injective (dyadicSystem 𝕜 rates).analysis43  rw [evalZero_intrinsicExpectation, evalZero_intrinsicCharacter, expectationL1_character]44  split_ifs <;> simp only [evalZero_intrinsicCharacter, map_zero]4546theorem finrank_intrinsicExpectation (m : ℕ) :47    Module.finrank 𝕜 (intrinsicExpectation 𝕜 rates m).range = 2 ^ m := by48  have hu : Module.finrank 𝕜 (intrinsicExpectation 𝕜 rates m).range ≤ 2 ^ m := by49    have h := finrank_commutingLift_range_le (dyadicSystem 𝕜 rates).analysis rfl50      (expectationL1 𝕜 m) (expectation_analysis_commute 𝕜 rates m)51    exact h.trans_eq (WalshBlocks.finrank_range_expectationL1 𝕜 m)52  let v : (Finset.range m).powerset → (intrinsicExpectation 𝕜 rates m).range := fun F =>53    ⟨intrinsicCharacter 𝕜 rates F, ⟨intrinsicCharacter 𝕜 rates F, by54      change intrinsicExpectation 𝕜 rates m (intrinsicCharacter 𝕜 rates F) = _55      simp only [intrinsicExpectation_character, Finset.mem_powerset.mp F.property, ite_true]⟩⟩56  have hi : LinearIndependent 𝕜 v := by57    apply LinearIndependent.of_comp (intrinsicExpectation 𝕜 rates m).range.subtype58    exact (linearIndependent_intrinsicCharacter 𝕜 rates).comp59      (fun F : (Finset.range m).powerset => (F : Finset ℕ)) Subtype.val_injective60  have hl : 2 ^ m ≤ Module.finrank 𝕜 (intrinsicExpectation 𝕜 rates m).range := by61    simpa using hi.fintype_card_le_finrank62  exact le_antisymm hu hl6364theorem block_analysis_commute (m n : ℕ) (f : Lp 𝕜 1 haar) :65    WalshBlocks.blockL1 𝕜 m ((dyadicSystem 𝕜 rates).analysis n f) =66      (dyadicSystem 𝕜 rates).analysis n (WalshBlocks.blockL1 𝕜 m f) := by67  simp only [WalshBlocks.blockL1, sub_apply, map_sub, expectation_analysis_commute]6869/-- The next-coordinate difference projection in the actual intrinsic norm. -/70theorem intrinsicAnalysis_zero :71    (dyadicSystem 𝕜 rates).analysis 0 = ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 haar) := rfl7273def intrinsicBlock (m : ℕ) :74    (dyadicSystem 𝕜 rates).IntrinsicSpace →L[𝕜] (dyadicSystem 𝕜 rates).IntrinsicSpace :=75  commutingLift (dyadicSystem 𝕜 rates).analysis (intrinsicAnalysis_zero 𝕜 rates) (WalshBlocks.blockL1 𝕜 m)76    (block_analysis_commute 𝕜 rates m)7778@[simp] theorem evalZero_intrinsicBlock (m : ℕ) (x : (dyadicSystem 𝕜 rates).IntrinsicSpace) :79    evalZero (dyadicSystem 𝕜 rates).analysis (intrinsicBlock 𝕜 rates m x) =80      WalshBlocks.blockL1 𝕜 m (evalZero (dyadicSystem 𝕜 rates).analysis x) :=81  evalZero_commutingLift _ _ _ _ _8283theorem intrinsicBlock_eq_sub (m : ℕ) :84    intrinsicBlock 𝕜 rates m = intrinsicExpectation 𝕜 rates (m + 1) - intrinsicExpectation 𝕜 rates m := by85  ext1 x86  apply evalZero_injective (dyadicSystem 𝕜 rates).analysis87  simp only [evalZero_intrinsicBlock, sub_apply, map_sub,88    evalZero_intrinsicExpectation, WalshBlocks.blockL1]8990instance intrinsicBlock_range_finiteDimensional (m : ℕ) :91    FiniteDimensional 𝕜 (intrinsicBlock 𝕜 rates m).range := by92  let : FiniteDimensional 𝕜 (WalshBlocks.blockL1 𝕜 m).range := by93    rw [WalshBlocks.range_blockL1_eq]94    infer_instance95  exact commutingLift_range_finiteDimensional _ _ _ _9697theorem intrinsicBlock_character (m : ℕ) (F : Finset ℕ) :98    intrinsicBlock 𝕜 rates m (intrinsicCharacter 𝕜 rates F) =99      if m ∈ F ∧ F ⊆ Finset.range (m + 1) then intrinsicCharacter 𝕜 rates F else 0 := by100  apply evalZero_injective (dyadicSystem 𝕜 rates).analysis101  rw [evalZero_intrinsicBlock, evalZero_intrinsicCharacter, WalshBlocks.blockL1_character]102  split_ifs <;> simp only [evalZero_intrinsicCharacter, map_zero]103104theorem finrank_intrinsicBlock (m : ℕ) :105    Module.finrank 𝕜 (intrinsicBlock 𝕜 rates m).range = 2 ^ m := by106  let : FiniteDimensional 𝕜 (WalshBlocks.blockL1 𝕜 m).range := by107    rw [WalshBlocks.range_blockL1_eq]108    infer_instance109  have hu : Module.finrank 𝕜 (intrinsicBlock 𝕜 rates m).range ≤ 2 ^ m := by110    have h := finrank_commutingLift_range_le (dyadicSystem 𝕜 rates).analysis rfl111      (WalshBlocks.blockL1 𝕜 m) (block_analysis_commute 𝕜 rates m)112    exact h.trans_eq (WalshBlocks.finrank_range_blockL1 𝕜 m)113  let v : (Finset.range m).powerset → (intrinsicBlock 𝕜 rates m).range := fun F =>114    ⟨intrinsicCharacter 𝕜 rates (insert m F), ⟨intrinsicCharacter 𝕜 rates (insert m F), by115      change intrinsicBlock 𝕜 rates m (intrinsicCharacter 𝕜 rates (insert m F)) = _116      rw [intrinsicBlock_character]117      apply ite_eq_left118      exact ⟨Finset.mem_insert_self _ _, Finset.insert_subset_iff.mpr119        ⟨Finset.mem_range.mpr (Nat.lt_succ_self m),120          (Finset.mem_powerset.mp F.property).trans (Finset.range_mono (Nat.le_succ m))⟩⟩⟩⟩121  have hi : LinearIndependent 𝕜 v := by122    apply LinearIndependent.of_comp (intrinsicBlock 𝕜 rates m).range.subtype123    exact (linearIndependent_intrinsicCharacter 𝕜 rates).comp _124      (WalshBlocks.blockSupport_injective m)125  have hl : 2 ^ m ≤ Module.finrank 𝕜 (intrinsicBlock 𝕜 rates m).range := by126    simpa using hi.fintype_card_le_finrank127  exact le_antisymm hu hl128129theorem intrinsicExpectation_commute (m n : ℕ) :130    (intrinsicExpectation 𝕜 rates m).comp (intrinsicExpectation 𝕜 rates n) =131      (intrinsicExpectation 𝕜 rates n).comp (intrinsicExpectation 𝕜 rates m) := by132  ext1 x133  apply evalZero_injective (dyadicSystem 𝕜 rates).analysis134  simp only [ContinuousLinearMap.comp_apply, evalZero_intrinsicExpectation]135  exact DFunLike.congr_fun (expectationL1_commute 𝕜 m (tailMeasure n))136    (evalZero (dyadicSystem 𝕜 rates).analysis x)137138theorem intrinsicExpectation_comp_min (m n : ℕ) :139    (intrinsicExpectation 𝕜 rates m).comp (intrinsicExpectation 𝕜 rates n) =140      intrinsicExpectation 𝕜 rates (min m n) := by141  rcases le_total m n with h | h142  · rw [min_eq_left h, intrinsicExpectation_comp_of_le 𝕜 rates m n h]143  · rw [intrinsicExpectation_commute, min_eq_right h,144      intrinsicExpectation_comp_of_le 𝕜 rates n m h]145146/-- Distinct Walsh blocks annihilate one another, and each block is a projection. -/147theorem intrinsicBlock_comp (m n : ℕ) :148    (intrinsicBlock 𝕜 rates m).comp (intrinsicBlock 𝕜 rates n) =149      if m = n then intrinsicBlock 𝕜 rates m else 0 := by150  simp only [intrinsicBlock_eq_sub, ContinuousLinearMap.sub_comp, ContinuousLinearMap.comp_sub,151    intrinsicExpectation_comp_min]152  rcases lt_trichotomy m n with h | h | h153  · have h1 : min (m + 1) (n + 1) = m + 1 := min_eq_left (by omega)154    have h2 : min (m + 1) n = m + 1 := min_eq_left (by omega)155    have h3 : min m (n + 1) = m := min_eq_left (by omega)156    have h4 : min m n = m := min_eq_left (by omega)157    simp only [h.ne, ite_false, h1, h2, h3, h4]158    ext1 x159    simp only [sub_apply, zero_apply]160    abel161  · subst n162    simp only [min_self, min_eq_left (Nat.le_succ m), min_eq_right (Nat.le_succ m), ite_true]163    ext1 x164    simp only [sub_apply]165    abel166  · have h1 : min (m + 1) (n + 1) = n + 1 := min_eq_right (by omega)167    have h2 : min (m + 1) n = n := min_eq_right (by omega)168    have h3 : min m (n + 1) = n + 1 := min_eq_right (by omega)169    have h4 : min m n = n := min_eq_right (by omega)170    simp only [h.ne', ite_false, h1, h2, h3, h4]171    ext1 x172    simp only [sub_apply, zero_apply]173    abel174175theorem intrinsicBlock_isProjection (m : ℕ) : IsProjection (intrinsicBlock 𝕜 rates m) := by176  change (intrinsicBlock 𝕜 rates m).comp (intrinsicBlock 𝕜 rates m) = _177  simpa only [ite_true] using intrinsicBlock_comp 𝕜 rates m m178179theorem intrinsicExpectation_zero_comp_block (m : ℕ) :180    (intrinsicExpectation 𝕜 rates 0).comp (intrinsicBlock 𝕜 rates m) = 0 := by181  rw [intrinsicBlock_eq_sub, ContinuousLinearMap.comp_sub]182  simp only [intrinsicExpectation_comp_min, zero_min]183  ext1 x184  simp only [sub_apply, zero_apply]185  abel186187theorem intrinsicBlock_comp_expectation_zero (m : ℕ) :188    (intrinsicBlock 𝕜 rates m).comp (intrinsicExpectation 𝕜 rates 0) = 0 := by189  rw [intrinsicBlock_eq_sub, ContinuousLinearMap.sub_comp]190  simp only [intrinsicExpectation_comp_min, min_zero]191  ext1 x192  simp only [sub_apply, zero_apply]193  abel194195theorem norm_intrinsicBlock_le_two (m : ℕ) : ‖intrinsicBlock 𝕜 rates m‖ ≤ 2 := by196  rw [intrinsicBlock_eq_sub]197  calc198    _ ≤ ‖intrinsicExpectation 𝕜 rates (m + 1)‖ + ‖intrinsicExpectation 𝕜 rates m‖ :=199      norm_sub_le (intrinsicExpectation 𝕜 rates (m + 1)) (intrinsicExpectation 𝕜 rates m)200    _ ≤ 1 + 1 := add_le_add (norm_intrinsicExpectation_le 𝕜 rates (m + 1))201      (norm_intrinsicExpectation_le 𝕜 rates m)202    _ = 2 := by norm_num203204/-- The partial sums of the block expansion are exactly the contractive expectations. -/205theorem intrinsicBlock_partialSum (N : ℕ) :206    intrinsicExpectation 𝕜 rates 0 + ∑ m ∈ Finset.range N, intrinsicBlock 𝕜 rates m =207      intrinsicExpectation 𝕜 rates N := by208  ext1 x209  simp only [add_apply, sum_apply]210  induction N with211  | zero => simp212  | succ N ih =>213    rw [Finset.sum_range_succ, ← add_assoc, ih, intrinsicBlock_eq_sub, sub_apply]214    abel215216theorem intrinsicBlock_partialSum_apply (N : ℕ) (x : (dyadicSystem 𝕜 rates).IntrinsicSpace) :217    intrinsicExpectation 𝕜 rates 0 x + ∑ m ∈ Finset.range N, intrinsicBlock 𝕜 rates m x =218      intrinsicExpectation 𝕜 rates N x := by219  have h := DFunLike.congr_fun (intrinsicBlock_partialSum 𝕜 rates N) x220  simpa only [add_apply, sum_apply] using h221222/-- Every intrinsic vector has its Walsh block expansion converging in the actual intrinsic norm. -/223theorem tendsto_intrinsicBlock_partialSum (x : (dyadicSystem 𝕜 rates).IntrinsicSpace) :224    Tendsto (fun N => intrinsicExpectation 𝕜 rates 0 x +225      ∑ m ∈ Finset.range N, intrinsicBlock 𝕜 rates m x) atTop (𝓝 x) := by226  simpa only [intrinsicBlock_partialSum_apply] using tendsto_intrinsicExpectation 𝕜 rates x227228/-- Convergent expansions into the constant space and successive Walsh blocks are unique. -/229theorem intrinsicBlock_expansion_unique230    (x a₀ : (dyadicSystem 𝕜 rates).IntrinsicSpace)231    (a : ℕ → (dyadicSystem 𝕜 rates).IntrinsicSpace)232    (ha₀ : a₀ ∈ (intrinsicExpectation 𝕜 rates 0).range)233    (ha : ∀ m, a m ∈ (intrinsicBlock 𝕜 rates m).range)234    (hconv : Tendsto (fun N => a₀ + ∑ m ∈ Finset.range N, a m) atTop (𝓝 x)) :235    a₀ = intrinsicExpectation 𝕜 rates 0 x ∧ ∀ m, a m = intrinsicBlock 𝕜 rates m x := by236  have h₀₀ : intrinsicExpectation 𝕜 rates 0 a₀ = a₀ := by237    obtain ⟨y, rfl⟩ := ha₀238    exact DFunLike.congr_fun (intrinsicExpectation_isProjection 𝕜 rates 0) y239  have h₀a (m : ℕ) : intrinsicExpectation 𝕜 rates 0 (a m) = 0 := by240    obtain ⟨y, hy⟩ := ha m241    rw [← hy]242    exact DFunLike.congr_fun (intrinsicExpectation_zero_comp_block 𝕜 rates m) y243  have hm₀ (m : ℕ) : intrinsicBlock 𝕜 rates m a₀ = 0 := by244    obtain ⟨y, rfl⟩ := ha₀245    exact DFunLike.congr_fun (intrinsicBlock_comp_expectation_zero 𝕜 rates m) y246  have hma (m n : ℕ) : intrinsicBlock 𝕜 rates m (a n) = if m = n then a n else 0 := by247    obtain ⟨y, hy⟩ := ha n248    change intrinsicBlock 𝕜 rates n y = a n at hy249    have h := DFunLike.congr_fun (intrinsicBlock_comp 𝕜 rates m n) y250    change intrinsicBlock 𝕜 rates m (intrinsicBlock 𝕜 rates n y) = _ at h251    by_cases hmn : m = n252    · subst n253      simpa only [ite_true, hy] using h254    · simpa only [hmn, ite_false, zero_apply, hy] using h255  constructor256  · have h := ((intrinsicExpectation 𝕜 rates 0).continuous.tendsto x).comp hconv257    simp only [Function.comp_def, map_add, map_sum, h₀₀, h₀a, Finset.sum_const_zero, add_zero] at h258    exact tendsto_nhds_unique tendsto_const_nhds h259  · intro m260    have h := ((intrinsicBlock 𝕜 rates m).continuous.tendsto x).comp hconv261    have heq : (fun N => intrinsicBlock 𝕜 rates m (a₀ + ∑ n ∈ Finset.range N, a n))262        =ᶠ[atTop] (fun _ => a m) := by263      filter_upwards [eventually_ge_atTop (m + 1)] with N hN264      simp only [map_add, map_sum, hm₀, hma, zero_add]265      simp [show m < N by omega]266    exact tendsto_nhds_unique tendsto_const_nhds (h.congr' heq)267268end PL1.Noise269