PL1/GeneratorGraphBanach.lean
All source files · Download exact source
SHA-256: 71426c53f4e09d27a0b0a81e71c8895ccdda191208395016236e4d7e1d281753
1import PL1.NoiseGenerator2import PL1.KFunctional3import Mathlib.Analysis.Normed.Lp.ProdLp45/-!6# The genuine generator domain with its complete graph sum norm78The domain is a closed subspace of `WithLp 1 (Y × Y)`, so its inherited norm9is exactly `‖f‖ + ‖Af‖`. The original base norm, resolvent graph and K-functional10are unchanged. The coordinate maps supply the continuous inclusion and the11generator as an operator on this graph-norm domain.12-/1314noncomputable section15open MeasureTheory16open scoped ENNReal NNReal1718namespace PL1.GeneratorGraphBanach19open Noise Walsh2021variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)2223abbrev Ambient := WithLp 1 (Lp K 1 haar × Lp K 1 haar)2425def submodule : Submodule K (Ambient K) :=26 (ResolventGeneratorGraph.graph K rates).comap27 (WithLp.prodContinuousLinearEquiv 1 K (Lp K 1 haar) (Lp K 1 haar)).toLinearMap2829abbrev Domain := submodule K rates3031theorem isClosed_submodule : IsClosed (submodule K rates : Set (Ambient K)) := by32 change IsClosed {z : Ambient K |33 resolventL1 K rates (dyadicTime 0) (z.fst + z.snd) = z.fst}34 exact isClosed_eq ((resolventL1 K rates (dyadicTime 0)).continuous.comp35 ((WithLp.fstL 1 K (Lp K 1 haar) (Lp K 1 haar)).continuous.add36 (WithLp.sndL 1 K (Lp K 1 haar) (Lp K 1 haar)).continuous))37 (WithLp.fstL 1 K (Lp K 1 haar) (Lp K 1 haar)).continuous3839instance : CompleteSpace (Domain K rates) :=40 (isClosed_submodule K rates).isComplete.completeSpace_coe4142def inclusion : Domain K rates →L[K] Lp K 1 haar :=43 (WithLp.fstL 1 K (Lp K 1 haar) (Lp K 1 haar)).comp (submodule K rates).subtypeL4445def generator : Domain K rates →L[K] Lp K 1 haar :=46 (WithLp.sndL 1 K (Lp K 1 haar) (Lp K 1 haar)).comp (submodule K rates).subtypeL4748@[simp] theorem inclusion_apply (z : Domain K rates) :49 inclusion K rates z = (z : Ambient K).fst := rfl5051@[simp] theorem generator_apply (z : Domain K rates) :52 generator K rates z = (z : Ambient K).snd := rfl5354/-- The norm is exactly the manuscript's graph sum norm. -/55theorem norm_eq (z : Domain K rates) :56 ‖z‖ = ‖inclusion K rates z‖ + ‖generator K rates z‖ :=57 WithLp.prod_norm_eq_of_L1 (z : Ambient K)5859theorem norm_inclusion_le (z : Domain K rates) : ‖inclusion K rates z‖ ≤ ‖z‖ := by60 rw [norm_eq]61 exact le_add_of_nonneg_right (norm_nonneg _)6263theorem norm_generator_le (z : Domain K rates) : ‖generator K rates z‖ ≤ ‖z‖ := by64 rw [norm_eq]65 exact le_add_of_nonneg_left (norm_nonneg _)6667theorem norm_inclusion_le_one : ‖inclusion K rates‖ ≤ 1 :=68 ContinuousLinearMap.opNorm_le_bound _ zero_le_one69 (fun z => by simpa only [one_mul] using norm_inclusion_le K rates z)7071theorem norm_generator_le_one : ‖generator K rates‖ ≤ 1 :=72 ContinuousLinearMap.opNorm_le_bound _ zero_le_one73 (fun z => by simpa only [one_mul] using norm_generator_le K rates z)7475theorem isGeneratorPair (z : Domain K rates) :76 Noise.IsGeneratorPair K rates (inclusion K rates z) (generator K rates z) :=77 (Noise.isGeneratorPair_iff_mem_graph K rates _ _).mpr z.property7879theorem inclusion_injective : Function.Injective (inclusion K rates) := by80 intro z w hzw81 have hs : generator K rates z = generator K rates w :=82 Noise.IsGeneratorPair.unique K rates (isGeneratorPair K rates z)83 (by rw [hzw]; exact isGeneratorPair K rates w)84 apply Subtype.ext85 apply WithLp.ofLp_injective 186 exact Prod.ext hzw hs8788def ofPair (f g : Lp K 1 haar) (hfg : Noise.IsGeneratorPair K rates f g) : Domain K rates :=89 ⟨WithLp.toLp 1 (f, g), (Noise.isGeneratorPair_iff_mem_graph K rates f g).mp hfg⟩9091@[simp] theorem inclusion_ofPair (f g : Lp K 1 haar)92 (hfg : Noise.IsGeneratorPair K rates f g) :93 inclusion K rates (ofPair K rates f g hfg) = f := rfl9495@[simp] theorem generator_ofPair (f g : Lp K 1 haar)96 (hfg : Noise.IsGeneratorPair K rates f g) :97 generator K rates (ofPair K rates f g hfg) = g := rfl9899theorem norm_ofPair (f g : Lp K 1 haar) (hfg : Noise.IsGeneratorPair K rates f g) :100 ‖ofPair K rates f g hfg‖ = ‖f‖ + ‖g‖ := norm_eq K rates _101102theorem mem_range_inclusion_iff (f : Lp K 1 haar) :103 f ∈ (inclusion K rates).range ↔ ∃ g, Noise.IsGeneratorPair K rates f g := by104 constructor105 · rintro ⟨z, rfl⟩106 exact ⟨generator K rates z, isGeneratorPair K rates z⟩107 · rintro ⟨g, hfg⟩108 exact ⟨ofPair K rates f g hfg, rfl⟩109110theorem denseRange_inclusion : DenseRange (inclusion K rates) := by111 have he : Set.range (inclusion K rates) =112 {f : Lp K 1 haar | ∃ g, Noise.IsGeneratorPair K rates f g} := by113 ext f114 exact mem_range_inclusion_iff K rates f115 rw [DenseRange, he]116 exact Noise.dense_generator_domain K rates117118/-- The existing K-functional is the standard infimum for the continuous119inclusion of this genuine complete graph-norm domain. -/120theorem kFunctional_eq (t : ℝ) (f : Lp K 1 haar) :121 KFunctional.value K rates t f =122 sInf (Set.range (fun z : Domain K rates => ‖f - inclusion K rates z‖ + t * ‖z‖)) := by123 unfold KFunctional.value124 congr 1125 ext r126 constructor127 · rintro ⟨z, rfl⟩128 let w := ofPair K rates z.val.1 z.val.2129 ((Noise.isGeneratorPair_iff_mem_graph K rates _ _).mpr z.property)130 refine ⟨w, ?_⟩131 change ‖f - inclusion K rates w‖ + t * ‖w‖ = _132 rw [norm_eq]133 rfl134 · rintro ⟨z, rfl⟩135 refine ⟨⟨(inclusion K rates z, generator K rates z),136 (Noise.isGeneratorPair_iff_mem_graph K rates _ _).mp (isGeneratorPair K rates z)⟩, ?_⟩137 change ‖f - inclusion K rates z‖ + t *138 (‖inclusion K rates z‖ + ‖generator K rates z‖) = _139 rw [← norm_eq]140141end PL1.GeneratorGraphBanach142