PL1/ResolventGeneratorGraph.lean
All source files · Download exact source
SHA-256: fc59fad27f7fe22764f57e3791299217a84aded967de9838df2efedac0877e9c
1import PL1.NoiseSemigroup23/-!4# The actual resolvent graph associated to the generator56The submodule is defined by `R₁(f + g) = f`, using the genuine Haar L¹7resolvent. Its graph norm is explicitly the sum of the two L¹ norms, rather8than the maximum norm on the ambient product. Identification with the9infinitesimal semigroup generator is a separate theorem in NoiseGenerator.10-/1112noncomputable section13open MeasureTheory Filter14open scoped ENNReal NNReal Topology1516namespace PL1.ResolventGeneratorGraph17open Noise Walsh1819variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)2021def graph : Submodule K (Lp K 1 haar × Lp K 1 haar) where22 carrier := {z | resolventL1 K rates (dyadicTime 0) (z.1 + z.2) = z.1}23 zero_mem' := by simp24 add_mem' := by25 intro x y hx hy26 change resolventL1 K rates (dyadicTime 0) ((x.1 + y.1) + (x.2 + y.2)) = x.1 + y.127 rw [show (x.1 + y.1) + (x.2 + y.2) = (x.1 + x.2) + (y.1 + y.2) by abel,28 map_add, hx, hy]29 smul_mem' := by30 intro c x hx31 change resolventL1 K rates (dyadicTime 0) (c • x.1 + c • x.2) = c • x.132 rw [← smul_add, map_smul, hx]3334@[simp] theorem mem_graph (f g : Lp K 1 haar) :35 (f, g) ∈ graph K rates ↔ resolventL1 K rates (dyadicTime 0) (f + g) = f := Iff.rfl3637/-- This is the graph sum norm, not the ambient product norm. -/38def graphNorm (z : Lp K 1 haar × Lp K 1 haar) : ℝ := ‖z.1‖ + ‖z.2‖3940theorem graphNorm_nonneg (z : Lp K 1 haar × Lp K 1 haar) : 0 ≤ graphNorm K z :=41 add_nonneg (norm_nonneg _) (norm_nonneg _)4243theorem norm_resolvent_apply_le (t : PositiveTime) (f : Lp K 1 haar) :44 ‖resolventL1 K rates t f‖ ≤ ‖f‖ :=45 ((resolventL1 K rates t).le_opNorm f).trans46 (by47 simpa only [one_mul] using48 mul_le_mul_of_nonneg_right (norm_resolventL1_le_one K rates t) (norm_nonneg f))4950theorem resolvent_one_eq_zero {f : Lp K 1 haar}51 (hf : resolventL1 K rates (dyadicTime 0) f = 0) : f = 0 := by52 have hz (t : PositiveTime) : resolventL1 K rates t f = 0 := by53 have h := DFunLike.congr_fun (resolventL1_identity K rates t (dyadicTime 0)) f54 have ht : ((t : ℝ) : K) ≠ 0 := by exact_mod_cast t.property.ne'55 have h1 : (dyadicTime 0 : ℝ) = 1 := rfl56 simp only [ContinuousLinearMap.comp_apply, sub_apply, ContinuousLinearMap.id_apply,57 smul_apply, hf, map_zero, sub_zero, h1, div_one] at h58 exact (smul_eq_zero.mp h.symm).resolve_left ht59 have hzero : Tendsto (fun n => resolventL1 K rates (dyadicTime n) f) atTop (𝓝 0) := by60 simpa only [hz] using (tendsto_const_nhds : Tendsto (fun _ : ℕ => (0 : Lp K 1 haar)) atTop (𝓝 0))61 exact tendsto_nhds_unique (dyadic_resolvent_strong K rates f) hzero6263theorem resolvent_one_injective : Function.Injective (resolventL1 K rates (dyadicTime 0)) := by64 intro f g hfg65 apply sub_eq_zero.mp66 apply resolvent_one_eq_zero K rates67 rw [map_sub, hfg, sub_self]6869theorem snd_unique {f g h : Lp K 1 haar}70 (hfg : (f, g) ∈ graph K rates) (hfh : (f, h) ∈ graph K rates) : g = h := by71 have he : f + g = f + h := resolvent_one_injective K rates (hfg.trans hfh.symm)72 exact add_left_cancel he7374/-- The actual resolvent supplies a graph pair at every positive time. -/75theorem resolvent_pair_mem (t : PositiveTime) (f : Lp K 1 haar) :76 (resolventL1 K rates t f,77 (((t : ℝ)⁻¹ : ℝ) : K) • (f - resolventL1 K rates t f)) ∈ graph K rates := by78 have h := DFunLike.congr_fun (resolventL1_identity K rates (dyadicTime 0) t) f79 have h1 : (dyadicTime 0 : ℝ) = 1 := rfl80 simp only [ContinuousLinearMap.comp_apply, sub_apply, ContinuousLinearMap.id_apply,81 smul_apply, h1, one_div] at h82 change resolventL1 K rates (dyadicTime 0)83 (resolventL1 K rates t f + (((t : ℝ)⁻¹ : ℝ) : K) • (f - resolventL1 K rates t f)) =84 resolventL1 K rates t f85 rw [map_add, map_smul, ← h]86 abel8788theorem defect_eq (t : PositiveTime) {f g : Lp K 1 haar}89 (hfg : (f, g) ∈ graph K rates) :90 f - resolventL1 K rates t f = ((t : ℝ) : K) • resolventL1 K rates t g := by91 have h := DFunLike.congr_fun (resolventL1_identity K rates t (dyadicTime 0)) (f + g)92 have h1 : (dyadicTime 0 : ℝ) = 1 := rfl93 change resolventL1 K rates (dyadicTime 0) (f + g) = f at hfg94 simp only [ContinuousLinearMap.comp_apply, sub_apply, ContinuousLinearMap.id_apply,95 smul_apply, hfg, add_sub_cancel_left, h1, div_one] at h96 exact h9798theorem norm_defect_le (t : PositiveTime) {f g : Lp K 1 haar}99 (hfg : (f, g) ∈ graph K rates) :100 ‖f - resolventL1 K rates t f‖ ≤ (t : ℝ) * ‖g‖ := by101 rw [defect_eq K rates t hfg, norm_smul, RCLike.norm_ofReal, abs_of_pos t.property]102 exact mul_le_mul_of_nonneg_left (norm_resolvent_apply_le K rates t g) t.property.le103104end PL1.ResolventGeneratorGraph105