PL1/IntrinsicGraph.lean
All source files · Download exact source
SHA-256: be869713a967910adbe0d4745e3a6fa2b8334356abef42e7f905d0f4311cd0ae
1import PL1.Definitions23/-!4# An intrinsic norm as a closed graph in an `ℓ₁` sum56For continuous coordinate operators `D n`, the vectors of the intrinsic space7are exactly the summable tuples satisfying `x n = D n (x 0)`. The norm is the8actual inherited `ℓ₁` norm; completeness follows from closedness of these9coordinate equations. The coordinate operators themselves need not be10uniformly bounded.11-/1213noncomputable section1415namespace PL1.IntrinsicGraph1617variable {𝕜 Y : Type*} [RCLike 𝕜]18variable [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]1920/-- The ambient countable `ℓ₁` sum of copies of `Y`. -/21abbrev Ambient := lp (fun _ : ℕ => Y) 12223/-- The simultaneous graph of all coordinate operators, based at coordinate zero. -/24def graph (D : ℕ → Y →L[𝕜] Y) : Submodule 𝕜 (Ambient (Y := Y)) where25 carrier := {x | ∀ n, x n = D n (x 0)}26 zero_mem' := by simp27 add_mem' := by28 intro x y hx hy n29 simp only [lp.coeFn_add, Pi.add_apply, map_add, hx n, hy n]30 smul_mem' := by31 intro c x hx n32 simp only [lp.coeFn_smul, Pi.smul_apply, map_smul, hx n]3334/-- The intrinsic normed space, with the norm inherited from the actual `ℓ₁` sum. -/35abbrev Space (D : ℕ → Y →L[𝕜] Y) := graph D3637variable (D : ℕ → Y →L[𝕜] Y)3839@[simp]40theorem mem_graph (x : Ambient (Y := Y)) :41 x ∈ graph D ↔ ∀ n, x n = D n (x 0) := Iff.rfl4243/-- Each defining coordinate equation is closed. -/44theorem isClosed_graph : IsClosed (graph D : Set (Ambient (Y := Y))) := by45 change IsClosed {x : Ambient (Y := Y) | ∀ n, x n = D n (x 0)}46 simp only [Set.ofPred_forall]47 apply isClosed_iInter48 intro n49 exact isClosed_eq (lp.evalCLM 𝕜 (fun _ : ℕ => Y) 1 n).continuous50 ((D n).continuous.comp (lp.evalCLM 𝕜 (fun _ : ℕ => Y) 1 0).continuous)5152instance [CompleteSpace Y] : CompleteSpace (Space D) :=53 (isClosed_graph D).isComplete.completeSpace_coe5455/-- The canonical embedding into the ambient sum is isometric. -/56def inclusion : Space D →ₗᵢ[𝕜] Ambient (Y := Y) :=57 (graph D).subtypeₗᵢ5859/-- Evaluation at any coordinate of the intrinsic graph is continuous linear. -/60def coord (n : ℕ) : Space D →L[𝕜] Y :=61 (lp.evalCLM 𝕜 (fun _ : ℕ => Y) 1 n).comp (graph D).subtypeL6263@[simp]64theorem coord_apply (n : ℕ) (x : Space D) :65 coord D n x = (x : Ambient (Y := Y)) n := rfl6667/-- Coordinate zero recovers the original underlying vector. -/68def evalZero : Space D →L[𝕜] Y := coord D 06970@[simp]71theorem evalZero_apply (x : Space D) :72 evalZero D x = (x : Ambient (Y := Y)) 0 := rfl7374theorem coord_eq (n : ℕ) (x : Space D) :75 coord D n x = D n (evalZero D x) := x.property n7677/-- The zeroth coordinate determines the whole intrinsic graph vector. -/78theorem evalZero_injective : Function.Injective (evalZero D) := by79 intro x y h80 apply Subtype.ext81 apply lp.ext82 funext n83 change coord D n x = coord D n y84 rw [coord_eq, coord_eq, h]8586/-- The original ambient norm is bounded by the intrinsic graph norm. -/87theorem norm_evalZero_le (x : Space D) : ‖evalZero D x‖ ≤ ‖x‖ := by88 exact lp.norm_apply_le_norm (by simp) (x : Ambient (Y := Y)) 08990theorem opNorm_evalZero_le_one : ‖evalZero D‖ ≤ 1 := by91 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one92 intro x93 simpa only [one_mul] using norm_evalZero_le D x9495/-- The graph norm is precisely the sum of the coordinate norms. -/96theorem norm_eq_tsum (x : Space D) :97 ‖x‖ = ∑' n : ℕ, ‖coord D n x‖ := by98 change ‖(x : Ambient (Y := Y))‖ = ∑' n : ℕ, ‖(x : Ambient (Y := Y)) n‖99 simpa using lp.norm_eq_tsum_rpow (by norm_num : 0 < (1 : ENNReal).toReal)100 (x : Ambient (Y := Y))101102theorem norm_eq_tsum_operators (x : Space D) :103 ‖x‖ = ∑' n : ℕ, ‖D n (evalZero D x)‖ := by104 rw [norm_eq_tsum]105 congr 1106 funext n107 rw [coord_eq]108109/-- A vector belongs to the intrinsic space whenever its operator coordinates110are absolutely summable, provided coordinate zero is the identity. -/111def ofSummable (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)112 (f : Y) (hf : Summable (fun n : ℕ => ‖D n f‖)) : Space D :=113 ⟨⟨fun n => D n f, memℓp_gen (by simpa using hf)⟩, by114 intro n115 change D n f = D n (D 0 f)116 rw [h0]117 rfl⟩118119@[simp]120theorem coord_ofSummable (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)121 (f : Y) (hf : Summable (fun n : ℕ => ‖D n f‖)) (n : ℕ) :122 coord D n (ofSummable D h0 f hf) = D n f := rfl123124@[simp]125theorem evalZero_ofSummable (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)126 (f : Y) (hf : Summable (fun n : ℕ => ‖D n f‖)) :127 evalZero D (ofSummable D h0 f hf) = f := by128 change D 0 f = f129 rw [h0]130 rfl131132theorem norm_ofSummable (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)133 (f : Y) (hf : Summable (fun n : ℕ => ‖D n f‖)) :134 ‖ofSummable D h0 f hf‖ = ∑' n : ℕ, ‖D n f‖ := by135 rw [norm_eq_tsum]136 rfl137138/-- Scalar recovery identifies the graph exactly with the vectors having139finite intrinsic norm, rather than only embedding a subset of them. -/140theorem mem_range_evalZero_iff (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y) (f : Y) :141 f ∈ (evalZero D).range ↔ Summable (fun n : ℕ => ‖D n f‖) := by142 constructor143 · rintro ⟨x, rfl⟩144 change Summable (fun n : ℕ => ‖D n (evalZero D x)‖)145 have hx : Summable (fun n : ℕ => ‖coord D n x‖) := by146 simpa only [coord_apply, ENNReal.toReal_one, Real.rpow_one] using147 (lp.memℓp (x : Ambient (Y := Y))).summable (by norm_num)148 simpa only [coord_eq] using hx149 · intro hf150 exact ⟨ofSummable D h0 f hf, evalZero_ofSummable D h0 f hf⟩151152/-- A smoothing operator gives an algebraic column into the intrinsic graph. -/153def columnLinear (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)154 (B : Y →L[𝕜] Y)155 (hs : ∀ y : Y, Summable (fun n : ℕ => ‖D n (B y)‖)) :156 Y →ₗ[𝕜] Space D where157 toFun y := ofSummable D h0 (B y) (hs y)158 map_add' x y := by159 apply Subtype.ext160 apply lp.ext161 funext n162 change D n (B (x + y)) = D n (B x) + D n (B y)163 simp only [map_add]164 map_smul' c y := by165 apply Subtype.ext166 apply lp.ext167 funext n168 change D n (B (c • y)) = c • D n (B y)169 simp only [map_smul]170171/-- A uniform estimate on the sum of coordinate norms bundles the smoothing172column as a bounded operator into the intrinsic Banach space. -/173def column (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)174 (B : Y →L[𝕜] Y)175 (hs : ∀ y : Y, Summable (fun n : ℕ => ‖D n (B y)‖))176 (C : ℝ) (hC : ∀ y : Y, (∑' n : ℕ, ‖D n (B y)‖) ≤ C * ‖y‖) :177 Y →L[𝕜] Space D :=178 (columnLinear D h0 B hs).mkContinuous C (fun y => by179 change ‖ofSummable D h0 (B y) (hs y)‖ ≤ C * ‖y‖180 rw [norm_ofSummable]181 exact hC y)182183@[simp]184theorem column_apply (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)185 (B : Y →L[𝕜] Y)186 (hs : ∀ y : Y, Summable (fun n : ℕ => ‖D n (B y)‖))187 (C : ℝ) (hC : ∀ y : Y, (∑' n : ℕ, ‖D n (B y)‖) ≤ C * ‖y‖) (y : Y) :188 column D h0 B hs C hC y = ofSummable D h0 (B y) (hs y) := rfl189190theorem norm_column_le (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)191 (B : Y →L[𝕜] Y)192 (hs : ∀ y : Y, Summable (fun n : ℕ => ‖D n (B y)‖))193 (C : ℝ) (hC : ∀ y : Y, (∑' n : ℕ, ‖D n (B y)‖) ≤ C * ‖y‖)194 (hC0 : 0 ≤ C) : ‖column D h0 B hs C hC‖ ≤ C := by195 apply ContinuousLinearMap.opNorm_le_bound _ hC0196 intro y197 rw [column_apply, norm_ofSummable]198 exact hC y199200@[simp]201theorem evalZero_column (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)202 (B : Y →L[𝕜] Y)203 (hs : ∀ y : Y, Summable (fun n : ℕ => ‖D n (B y)‖))204 (C : ℝ) (hC : ∀ y : Y, (∑' n : ℕ, ‖D n (B y)‖) ≤ C * ‖y‖) (y : Y) :205 evalZero D (column D h0 B hs C hC y) = B y := by206 rw [column_apply, evalZero_ofSummable]207208end PL1.IntrinsicGraph209