PL1/CompactWalshMultiplier.lean
All source files · Download exact source
SHA-256: 4c6d871e2e8de6ed8ab52c49637b04b0e157e82ca8f8023e822bd47538360b36
1import PL1.WalshModel2import Mathlib.Analysis.Normed.Lp.lpHolder3import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension4import Mathlib.Analysis.SpecialFunctions.Log.Basic5import PL1.ConcreteResolvents6import PL1.LpInclusions78/-!9# Compact diagonal Walsh multipliers1011This file proves compactness by finite-rank approximation in operator norm.12The coefficient condition is convergence to zero along the cofinite filter.13The final rate lemmas establish this condition for resolvent coefficients.14-/1516noncomputable section1718open Filter MeasureTheory19open scoped Topology ENNReal NNReal BigOperators2021namespace PL122namespace WalshMultiplier2324variable {ι : Type*} (𝕜 : Type*) [RCLike 𝕜]2526abbrev Coefficients (ι : Type*) (𝕜 : Type*) [RCLike 𝕜] := lp (fun _ : ι => 𝕜) ∞27abbrev SquareSummable (ι : Type*) (𝕜 : Type*) [RCLike 𝕜] := lp (fun _ : ι => 𝕜) 22829/-- Bounded coordinatewise multiplication on square-summable scalar families. -/30def diagonalL : Coefficients ι 𝕜 →L[𝕜] SquareSummable ι 𝕜 →L[𝕜] SquareSummable ι 𝕜 :=31 lp.holderL (p := ∞) (q := 2) 2 (fun _ : ι => ContinuousLinearMap.mul 𝕜 𝕜)32 (K := 1) (fun _ => ContinuousLinearMap.opNorm_mul_le 𝕜 𝕜)3334@[simp] theorem diagonalL_apply (a : Coefficients ι 𝕜) (x : SquareSummable ι 𝕜) (i : ι) :35 diagonalL 𝕜 a x i = a i * x i := rfl3637theorem norm_diagonalL_le : ‖(diagonalL 𝕜 : Coefficients ι 𝕜 →L[𝕜] _)‖ ≤ 1 :=38 lp.norm_holderL_le (p := ∞) (q := 2) 2 (fun _ : ι => ContinuousLinearMap.mul 𝕜 𝕜)39 (K := 1) (fun _ => ContinuousLinearMap.opNorm_mul_le 𝕜 𝕜)4041theorem diagonalL_single [DecidableEq ι] (j : ι) (c : 𝕜) :42 diagonalL 𝕜 (lp.single ∞ j c) =43 (lp.singleContinuousLinearMap 𝕜 (fun _ : ι => 𝕜) 2 j).comp44 ((ContinuousLinearMap.mul 𝕜 𝕜 c).comp (lp.evalCLM 𝕜 (fun _ : ι => 𝕜) 2 j)) := by45 ext x i46 change lp.single (E := fun _ : ι => 𝕜) ∞ j c i * x i =47 lp.single (E := fun _ : ι => 𝕜) 2 j (c * x j) i48 by_cases hi : i = j <;> simp [lp.single_apply, hi]4950theorem compact_diagonalL_single [DecidableEq ι] (j : ι) (c : 𝕜) :51 IsCompactOperator (diagonalL 𝕜 (lp.single ∞ j c)) := by52 rw [diagonalL_single]53 exact (isCompactOperator_of_locallyCompactSpace_dom54 ((ContinuousLinearMap.mul 𝕜 𝕜 c).comp (lp.evalCLM 𝕜 (fun _ : ι => 𝕜) 2 j))).clm_comp55 (lp.singleContinuousLinearMap 𝕜 (fun _ : ι => 𝕜) 2 j)5657theorem compact_diagonalL_sum [DecidableEq ι] (s : Finset ι) (a : ι → 𝕜) :58 IsCompactOperator (diagonalL 𝕜 (∑ i ∈ s, lp.single ∞ i (a i))) := by59 induction s using Finset.induction_on with60 | empty => simpa using (isCompactOperator_zero (M₁ := SquareSummable ι 𝕜)61 (M₂ := SquareSummable ι 𝕜))62 | @insert j s hj ih =>63 rw [Finset.sum_insert hj, map_add]64 exact (compact_diagonalL_single 𝕜 j (a j)).add ih6566/-- A null family has finite truncations converging in the supremum norm. -/67theorem tendsto_truncations [DecidableEq ι] (a : Coefficients ι 𝕜)68 (ha : Tendsto (fun i => a i) cofinite (𝓝 0)) :69 Tendsto (fun s : Finset ι => ∑ i ∈ s, lp.single ∞ i (a i)) atTop (𝓝 a) := by70 apply Metric.tendsto_atTop.mpr71 intro ε hε72 have he : ∀ᶠ i in cofinite, ‖a i‖ < ε / 2 := by73 have hn : Tendsto (fun i => ‖a i‖) cofinite (𝓝 (0 : ℝ)) := by74 simpa only [norm_zero] using ha.norm75 exact hn.eventually (gt_mem_nhds (half_pos hε))76 have hfinite := eventually_cofinite.mp he77 refine ⟨hfinite.toFinset, fun s hs => ?_⟩78 rw [dist_eq_norm]79 apply lt_of_le_of_lt (b := ε / 2) _ (half_lt_self hε)80 apply lp.norm_le_of_forall_le (half_pos hε).le81 intro i82 have hval : (∑ j ∈ s, lp.single ∞ j (a j)) i = if i ∈ s then a i else 0 := by83 simp only [lp.coeFn_sum, Finset.sum_apply, lp.coeFn_single, Finset.sum_pi_single]84 change ‖(∑ j ∈ s, lp.single ∞ j (a j)) i - a i‖ ≤ ε / 285 rw [hval]86 by_cases hi : i ∈ s87 · simp [hi, (half_pos hε).le]88 · have hai : ‖a i‖ < ε / 2 := by89 by_contra h90 exact hi (hs (hfinite.mem_toFinset.mpr h))91 simpa [hi] using hai.le9293/-- A bounded diagonal operator with coefficients vanishing at infinity is compact. -/94theorem compact_diagonalL [DecidableEq ι] (a : Coefficients ι 𝕜)95 (ha : Tendsto (fun i => a i) cofinite (𝓝 0)) :96 IsCompactOperator (diagonalL 𝕜 a) := by97 apply isCompactOperator_of_tendsto ((diagonalL 𝕜).continuous.tendsto a |>.comp98 (tendsto_truncations 𝕜 a ha))99 exact Eventually.of_forall (fun s => compact_diagonalL_sum 𝕜 s (fun i => a i))100101/-- Turn an arbitrary null scalar family into its bounded coefficient vector. -/102def nullCoefficients (a : ι → 𝕜) (ha : Tendsto a cofinite (𝓝 0)) : Coefficients ι 𝕜 :=103 ⟨a, memℓp_infty ha.norm.bddAbove_range_of_cofinite⟩104105section HilbertSpace106107variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]108109/-- Transfer a coordinate multiplier to any Hilbert space with a specified basis. -/110def hilbertDiagonal (b : HilbertBasis ι 𝕜 E) (a : Coefficients ι 𝕜) : E →L[𝕜] E :=111 b.repr.symm.toContinuousLinearEquiv.toContinuousLinearMap.comp112 ((diagonalL 𝕜 a).comp b.repr.toContinuousLinearEquiv.toContinuousLinearMap)113114theorem norm_hilbertDiagonal_le (b : HilbertBasis ι 𝕜 E) (a : Coefficients ι 𝕜) :115 ‖hilbertDiagonal 𝕜 b a‖ ≤ ‖a‖ := by116 apply ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg a)117 intro x118 change ‖b.repr.symm (diagonalL 𝕜 a (b.repr x))‖ ≤ ‖a‖ * ‖x‖119 rw [b.repr.symm.norm_map]120 have hD : ‖diagonalL 𝕜 a‖ ≤ ‖a‖ := by121 simpa only [one_mul] using (diagonalL 𝕜).le_of_opNorm_le (norm_diagonalL_le 𝕜) a122 simpa only [b.repr.norm_map] using (diagonalL 𝕜 a).le_of_opNorm_le hD (b.repr x)123124theorem compact_hilbertDiagonal [DecidableEq ι] (b : HilbertBasis ι 𝕜 E)125 (a : Coefficients ι 𝕜) (ha : Tendsto (fun i => a i) cofinite (𝓝 0)) :126 IsCompactOperator (hilbertDiagonal 𝕜 b a) :=127 ((compact_diagonalL 𝕜 a ha).comp_clm b.repr.toContinuousLinearEquiv.toContinuousLinearMap).clm_comp128 b.repr.symm.toContinuousLinearEquiv.toContinuousLinearMap129130theorem hilbertDiagonal_apply_basis [DecidableEq ι] (b : HilbertBasis ι 𝕜 E)131 (a : Coefficients ι 𝕜) (i : ι) : hilbertDiagonal 𝕜 b a (b i) = a i • b i := by132 apply b.repr.injective133 change b.repr (b.repr.symm (diagonalL 𝕜 a (b.repr (b i)))) = b.repr (a i • b i)134 rw [b.repr.apply_symm_apply, map_smul, b.repr_self]135 apply lp.ext136 funext j137 by_cases hj : j = i <;> simp [diagonalL_apply, lp.coeFn_smul, lp.single_apply, hj]138139/-- Any bounded operator diagonal on a Hilbert basis, with null eigenvalues, is compact. -/140theorem compact_of_diagonal [DecidableEq ι] (b : HilbertBasis ι 𝕜 E) (T : E →L[𝕜] E)141 (a : ι → 𝕜) (ha : Tendsto a cofinite (𝓝 0))142 (hT : ∀ i, T (b i) = a i • b i) : IsCompactOperator T := by143 have hEq : T = hilbertDiagonal 𝕜 b (nullCoefficients 𝕜 a ha) := by144 apply ContinuousLinearMap.ext_on (Submodule.dense_iff_topologicalClosure_eq_top.mpr b.dense_span)145 rintro x ⟨i, rfl⟩146 rw [hT, hilbertDiagonal_apply_basis]147 rfl148 rw [hEq]149 exact compact_hilbertDiagonal 𝕜 b (nullCoefficients 𝕜 a ha) ha150151end HilbertSpace152153section Rates154155variable (rates : ι → ℝ)156157/-- Only finitely many finite supports can have a bounded total rate. -/158theorem finite_rate_sublevels (hRate : ∀ i, 0 ≤ rates i)159 (hRateTop : Tendsto rates cofinite atTop) (L : ℝ) :160 Set.Finite {F : Finset ι | ∑ i ∈ F, rates i ≤ L} := by161 classical162 have he : ∀ᶠ i in cofinite, L < rates i := hRateTop.eventually (eventually_gt_atTop L)163 have hfinite : Set.Finite {i | rates i ≤ L} := by164 simpa only [not_lt] using eventually_cofinite.mp he165 apply hfinite.toFinset.powerset.finite_toSet.subset166 intro F hF167 apply Finset.mem_powerset.mpr168 intro i hi169 apply hfinite.mem_toFinset.mpr170 exact (Finset.single_le_sum (fun j _ => hRate j) hi).trans hF171172theorem tendsto_rateSum (hRate : ∀ i, 0 ≤ rates i) (hRateTop : Tendsto rates cofinite atTop) :173 Tendsto (fun F : Finset ι => ∑ i ∈ F, rates i) cofinite atTop := by174 apply tendsto_atTop.mpr175 intro L176 apply eventually_cofinite.mpr177 exact (finite_rate_sublevels rates hRate hRateTop L).subset (fun F hF => (not_le.mp hF).le)178179theorem tendsto_resolvent_coefficients (hRate : ∀ i, 0 ≤ rates i)180 (hRateTop : Tendsto rates cofinite atTop) {t : ℝ} (ht : 0 < t) :181 Tendsto (fun F : Finset ι => (1 + t * ∑ i ∈ F, rates i)⁻¹) cofinite (𝓝 0) := by182 apply tendsto_inv_atTop_zero.comp183 exact tendsto_const_nhds.add_atTop ((tendsto_rateSum rates hRate hRateTop).const_mul_atTop ht)184185end Rates186187/-- Growth of the actual rate sequence used for the Schur example. -/188theorem tendsto_schurRates :189 Tendsto (fun j : ℕ => Real.sqrt (Real.log (j + 2))) cofinite atTop := by190 rw [Nat.cofinite_eq_atTop]191 apply Real.tendsto_sqrt_atTop.comp192 apply Real.tendsto_log_atTop.comp193 exact (tendsto_natCast_atTop_atTop : Tendsto (fun j : ℕ => (j : ℝ)) atTop atTop).atTop_add194 (tendsto_const_nhds (x := (2 : ℝ)))195196/-- A direct compactness criterion for a resolvent acting on the actual Haar L2. -/197theorem compact_walsh_resolvent_of_diagonal (rates : ℕ → ℝ)198 (hRate : ∀ j, 0 ≤ rates j) (hRateTop : Tendsto rates cofinite atTop)199 {t : ℝ} (ht : 0 < t) (T : Lp 𝕜 2 Walsh.haar →L[𝕜] Lp 𝕜 2 Walsh.haar)200 (hT : ∀ F : Finset ℕ, T (Walsh.scalarCharacterLp 𝕜 2 F) =201 (((1 + t * ∑ j ∈ F, rates j)⁻¹ : ℝ) : 𝕜) • Walsh.scalarCharacterLp 𝕜 2 F) :202 IsCompactOperator T := by203 apply compact_of_diagonal 𝕜 (Walsh.scalarHilbertBasis 𝕜) T204 (fun F => (((1 + t * ∑ j ∈ F, rates j)⁻¹ : ℝ) : 𝕜))205 · simpa only [RCLike.ofReal_zero, Function.comp_def, RCLike.ofReal_inv] using206 RCLike.continuous_ofReal.tendsto 0 |>.comp (tendsto_resolvent_coefficients rates hRate hRateTop ht)207 · intro F208 simpa only [Walsh.scalarHilbertBasis_apply] using hT F209210theorem compact_schur_resolvent_of_diagonal {t : ℝ} (ht : 0 < t)211 (T : Lp 𝕜 2 Walsh.haar →L[𝕜] Lp 𝕜 2 Walsh.haar)212 (hT : ∀ F : Finset ℕ, T (Walsh.scalarCharacterLp 𝕜 2 F) =213 (((1 + t * ∑ j ∈ F, Real.sqrt (Real.log (j + 2)))⁻¹ : ℝ) : 𝕜) •214 Walsh.scalarCharacterLp 𝕜 2 F) : IsCompactOperator T :=215 compact_walsh_resolvent_of_diagonal 𝕜 _ (fun _ => Real.sqrt_nonneg _) tendsto_schurRates ht T hT216217section ConstructedResolvent218219variable (rates : ℕ → ℝ) (hRate : ∀ j, 0 ≤ rates j) (t : ℝ) (ht : 0 ≤ t)220include hRate ht221222theorem norm_resolvent_coefficient_le_one (F : Finset ℕ) :223 ‖(((1 + t * ∑ j ∈ F, rates j)⁻¹ : ℝ) : 𝕜)‖ ≤ 1 := by224 have hs : 0 ≤ ∑ j ∈ F, rates j := Finset.sum_nonneg (fun j _ => hRate j)225 have hd : 0 < 1 + t * ∑ j ∈ F, rates j := by positivity226 rw [RCLike.norm_ofReal, abs_of_nonneg (inv_nonneg.mpr hd.le)]227 exact (inv_le_one₀ hd).mpr (by nlinarith)228229/-- The bounded family of all resolvent eigenvalues; growth of the rates is not required. -/230def resolventCoefficients : Coefficients (Finset ℕ) 𝕜 :=231 ⟨fun F => (((1 + t * ∑ j ∈ F, rates j)⁻¹ : ℝ) : 𝕜), memℓp_infty232 ⟨1, by rintro r ⟨F, rfl⟩; exact norm_resolvent_coefficient_le_one 𝕜 rates hRate t ht F⟩⟩233234theorem norm_resolventCoefficients_le_one : ‖resolventCoefficients 𝕜 rates hRate t ht‖ ≤ 1 := by235 apply lp.norm_le_of_forall_le zero_le_one236 exact norm_resolvent_coefficient_le_one 𝕜 rates hRate t ht237238/-- A genuine bounded resolvent multiplier on Haar L2, for any nonnegative rates and time. -/239def resolventL2 : Lp 𝕜 2 Walsh.haar →L[𝕜] Lp 𝕜 2 Walsh.haar :=240 hilbertDiagonal 𝕜 (Walsh.scalarHilbertBasis 𝕜) (resolventCoefficients 𝕜 rates hRate t ht)241242theorem norm_resolventL2_le_one : ‖resolventL2 𝕜 rates hRate t ht‖ ≤ 1 :=243 (norm_hilbertDiagonal_le 𝕜 _ _).trans (norm_resolventCoefficients_le_one 𝕜 rates hRate t ht)244245theorem resolventL2_apply_character (F : Finset ℕ) :246 resolventL2 𝕜 rates hRate t ht (Walsh.scalarCharacterLp 𝕜 2 F) =247 (((1 + t * ∑ j ∈ F, rates j)⁻¹ : ℝ) : 𝕜) • Walsh.scalarCharacterLp 𝕜 2 F := by248 simpa only [Walsh.scalarHilbertBasis_apply, resolventL2, resolventCoefficients] using249 hilbertDiagonal_apply_basis 𝕜 (Walsh.scalarHilbertBasis 𝕜)250 (resolventCoefficients 𝕜 rates hRate t ht) F251252theorem compact_resolventL2 (hRateTop : Tendsto rates cofinite atTop) (htpos : 0 < t) :253 IsCompactOperator (resolventL2 𝕜 rates hRate t ht) :=254 compact_walsh_resolvent_of_diagonal 𝕜 rates hRate hRateTop htpos _255 (resolventL2_apply_character 𝕜 rates hRate t ht)256257end ConstructedResolvent258259section ActualResolvent260261variable (rates : ℕ → ℝ≥0) (t : Noise.PositiveTime)262263/-- The L2 extension of the manuscript's concrete convolution resolvent. -/264def actualResolventL2 : Lp 𝕜 2 Walsh.haar →L[𝕜] Lp 𝕜 2 Walsh.haar :=265 resolventL2 𝕜 (fun j => (rates j : ℝ)) (fun j => (rates j).coe_nonneg) t t.property.le266267theorem norm_actualResolventL2_le_one : ‖actualResolventL2 𝕜 rates t‖ ≤ 1 :=268 norm_resolventL2_le_one 𝕜 _ _ _ _269270theorem actualResolventL2_apply_character (F : Finset ℕ) :271 actualResolventL2 𝕜 rates t (Walsh.scalarCharacterLp 𝕜 2 F) =272 (((1 + (t : ℝ) * Noise.rateSum rates F)⁻¹ : ℝ) : 𝕜) •273 Walsh.scalarCharacterLp 𝕜 2 F :=274 resolventL2_apply_character 𝕜 _ _ _ _ F275276/-- The constructed L2 multiplier agrees with the actual convolution on their common domain. -/277theorem actualResolventL2_l2ToL1 :278 (Walsh.l2ToL1 (𝕜 := 𝕜)).comp (actualResolventL2 𝕜 rates t) =279 (Noise.resolventL1 𝕜 rates t).comp Walsh.l2ToL1 := by280 apply ContinuousLinearMap.ext_on (Walsh.dense_span_scalarCharacterLp 𝕜 2 (by norm_num))281 rintro f ⟨F, rfl⟩282 simp only [ContinuousLinearMap.comp_apply, actualResolventL2_apply_character,283 map_smul, Walsh.l2ToL1_scalarCharacter, Noise.resolventL1_scalarCharacter]284285theorem compact_actualResolventL2286 (hRateTop : Tendsto (fun j => (rates j : ℝ)) cofinite atTop) :287 IsCompactOperator (actualResolventL2 𝕜 rates t) :=288 compact_resolventL2 𝕜 _ _ _ _ hRateTop t.property289290theorem compact_schur_actualResolventL2 :291 IsCompactOperator (actualResolventL2 𝕜 Noise.schurRates t) :=292 compact_actualResolventL2 𝕜 Noise.schurRates t tendsto_schurRates293294theorem compact_resolventL1_on_L2295 (hRateTop : Tendsto (fun j => (rates j : ℝ)) cofinite atTop) :296 IsCompactOperator ((Noise.resolventL1 𝕜 rates t).comp Walsh.l2ToL1) := by297 rw [← actualResolventL2_l2ToL1]298 exact (compact_actualResolventL2 𝕜 rates t hRateTop).clm_comp Walsh.l2ToL1299300/-- The concrete resolvent has compact restriction from bounded functions to Haar L1. -/301theorem compact_resolventL1_on_Linfty302 (hRateTop : Tendsto (fun j => (rates j : ℝ)) cofinite atTop) :303 IsCompactOperator ((Noise.resolventL1 𝕜 rates t).comp304 ((Walsh.l2ToL1 (𝕜 := 𝕜)).comp Walsh.linftyToL2)) := by305 rw [← ContinuousLinearMap.comp_assoc]306 exact (compact_resolventL1_on_L2 𝕜 rates t hRateTop).comp_clm Walsh.linftyToL2307308theorem compact_schur_resolventL1_on_Linfty :309 IsCompactOperator ((Noise.resolventL1 𝕜 Noise.schurRates t).comp310 ((Walsh.l2ToL1 (𝕜 := 𝕜)).comp Walsh.linftyToL2)) :=311 compact_resolventL1_on_Linfty 𝕜 Noise.schurRates t tendsto_schurRates312313/-- Compactness stated using the direct canonical inclusion from L-infinity to L1. -/314theorem compact_resolventL1_restriction315 (hRateTop : Tendsto (fun j => (rates j : ℝ)) cofinite atTop) :316 IsCompactOperator ((Noise.resolventL1 𝕜 rates t).comp317 (ProbabilityLp.inclusion Walsh.haar 1 ∞ le_top)) := by318 simpa only [Walsh.l2ToL1, Walsh.linftyToL2, ProbabilityLp.inclusion_comp] using319 compact_resolventL1_on_Linfty 𝕜 rates t hRateTop320321theorem compact_schur_resolventL1_restriction :322 IsCompactOperator ((Noise.resolventL1 𝕜 Noise.schurRates t).comp323 (ProbabilityLp.inclusion Walsh.haar 1 ∞ le_top)) :=324 compact_resolventL1_restriction 𝕜 Noise.schurRates t tendsto_schurRates325326end ActualResolvent327328end WalshMultiplier329end PL1330