PL1/TruncatedResolventFactorization.lean
All source files · Download exact source
SHA-256: 4734539670ddc72b73ecf7f505b86e96c5cb4b104ff14fc6b63002ed52e44767
1import PL1.BochnerResolvents2import PL1.ExponentialTail3import PL1.CompactWalshMultiplier45/-!6# Exact smoothing factorization of the truncated resolvents78The equality is proved for the actual Bochner averages on Haar L1. Its9conditional Lp-to-L2 corollary needs only a genuine extension of one noise10operator on the common L1/Lp domain. Hypercontractivity itself is not assumed11to have been proved by this file.12-/1314noncomputable section15open MeasureTheory Filter16open scoped Topology ENNReal NNReal1718namespace PL1.Noise19open Walsh ExponentialTime2021variable (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0)2223theorem truncatedResolventL1_character (t : PositiveTime) (ε : ℝ≥0) (F : Finset ℕ) :24 truncatedResolventL1 𝕜 rates t ε (scalarCharacterLp 𝕜 1 F) =25 ((Real.exp (-(ε : ℝ) * ((t : ℝ)⁻¹ + rateSum rates F)) *26 (1 + (t : ℝ) * rateSum rates F)⁻¹ : ℝ) : 𝕜) • scalarCharacterLp 𝕜 1 F := by27 rw [truncatedResolventL1_apply]28 simp only [noiseL1_character, integral_smul_const]29 rw [integral_laplace_Ici_ofReal t.property _ (rateSum_nonneg rates F)]3031/-- Removing the initial time interval is exactly exponential damping followed32by a resolvent and the noise operator at the cutoff time. -/33theorem truncatedResolventL1_eq_resolvent_comp_noise (t : PositiveTime) (ε : ℝ≥0) :34 truncatedResolventL1 𝕜 rates t ε =35 ((Real.exp (-(ε : ℝ) / (t : ℝ)) : ℝ) : 𝕜) •36 (resolventL1 𝕜 rates t).comp (noiseL1 𝕜 rates ε) := by37 apply continuousLinearMap_ext_on_scalarCharacterL138 intro F39 simp only [truncatedResolventL1_character, smul_apply,40 ContinuousLinearMap.comp_apply, noiseL1_character, map_smul,41 resolventL1_scalarCharacter, smul_smul]42 congr 143 rw [show -(ε : ℝ) * ((t : ℝ)⁻¹ + rateSum rates F) =44 -(ε : ℝ) / (t : ℝ) + -(ε : ℝ) * rateSum rates F by ring,45 Real.exp_add]46 simp only [RCLike.ofReal_mul]47 ring4849theorem truncatedResolventL1_eq_noise_comp_resolvent (t : PositiveTime) (ε : ℝ≥0) :50 truncatedResolventL1 𝕜 rates t ε =51 ((Real.exp (-(ε : ℝ) / (t : ℝ)) : ℝ) : 𝕜) •52 (noiseL1 𝕜 rates ε).comp (resolventL1 𝕜 rates t) := by53 rw [truncatedResolventL1_eq_resolvent_comp_noise, noiseL1_resolvent_commute]5455variable {𝕜 rates}5657/-- A compatible smoothing extension at the cutoff time gives a bounded58Hilbert-valued extension of the actual truncated L1 resolvent. -/59def truncatedResolventLpToL2 (t : PositiveTime) (ε : ℝ≥0)60 {p : ℝ≥0∞} [Fact (1 ≤ p)]61 (H : Lp 𝕜 p haar →L[𝕜] Lp 𝕜 2 haar) :62 Lp 𝕜 p haar →L[𝕜] Lp 𝕜 2 haar :=63 ((Real.exp (-(ε : ℝ) / (t : ℝ)) : ℝ) : 𝕜) •64 (WalshMultiplier.actualResolventL2 𝕜 rates t).comp H6566theorem truncatedResolventLpToL2_overlap (t : PositiveTime) (ε : ℝ≥0)67 {p : ℝ≥0∞} [Fact (1 ≤ p)]68 (H : Lp 𝕜 p haar →L[𝕜] Lp 𝕜 2 haar)69 (hH : ∀ (g : Lp 𝕜 1 haar) (f : Lp 𝕜 p haar),70 g =ᵐ[haar] f → noiseL1 𝕜 rates ε g = l2ToL1 (H f))71 (g : Lp 𝕜 1 haar) (f : Lp 𝕜 p haar) (hgf : g =ᵐ[haar] f) :72 truncatedResolventL1 𝕜 rates t ε g =73 l2ToL1 (truncatedResolventLpToL2 (rates := rates) t ε H f) := by74 rw [truncatedResolventL1_eq_resolvent_comp_noise]75 simp only [smul_apply, ContinuousLinearMap.comp_apply,76 truncatedResolventLpToL2, map_smul]77 rw [hH g f hgf]78 congr 179 exact (DFunLike.congr_fun (WalshMultiplier.actualResolventL2_l2ToL1 𝕜 rates t) (H f)).symm8081theorem norm_truncatedResolventLpToL2_le (t : PositiveTime) (ε : ℝ≥0)82 {p : ℝ≥0∞} [Fact (1 ≤ p)]83 (H : Lp 𝕜 p haar →L[𝕜] Lp 𝕜 2 haar) :84 ‖truncatedResolventLpToL2 (rates := rates) t ε H‖ ≤85 Real.exp (-(ε : ℝ) / (t : ℝ)) * ‖H‖ := by86 rw [truncatedResolventLpToL2, norm_smul, RCLike.norm_ofReal,87 abs_of_pos (Real.exp_pos _)]88 apply mul_le_mul_of_nonneg_left _ (Real.exp_pos _).le89 exact (ContinuousLinearMap.opNorm_comp_le _ _).trans (by90 simpa only [one_mul] using mul_le_mul_of_nonneg_right91 (WalshMultiplier.norm_actualResolventL2_le_one 𝕜 rates t) (norm_nonneg H))9293end PL1.Noise94