PL1/IntrinsicApproximations.lean
All source files · Download exact source
SHA-256: b025d46774fea64011c68336cdc768dfb2dc2c4134d25303a244acc300bf8f78
1import PL1.IntrinsicGraph2import PL1.L1Sum3import Mathlib.Analysis.Normed.Group.Tannery45/-! # Commuting finite-dimensional approximations of the actual intrinsic graph -/67noncomputable section8open Filter9open scoped Topology1011namespace PL1.IntrinsicGraph1213variable {𝕜 Y : Type*} [RCLike 𝕜] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]14variable (D : ℕ → Y →L[𝕜] Y) (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)15variable (T : Y →L[𝕜] Y) (hc : ∀ n y, T (D n y) = D n (T y))1617include hc in18theorem summable_commuting_image (x : Space D) :19 Summable (fun n => ‖D n (T (evalZero D x))‖) := by20 apply ((L1Sum.summable_norm (x : Ambient (Y := Y))).mul_left ‖T‖).of_nonneg_of_le21 · intro n22 exact norm_nonneg _23 · intro n24 rw [← hc, ← coord_eq]25 exact T.le_opNorm _2627def commutingLiftLinear : Space D →ₗ[𝕜] Space D where28 toFun x := ofSummable D h0 (T (evalZero D x)) (summable_commuting_image D T hc x)29 map_add' x y := by30 apply evalZero_injective D31 simp only [evalZero_ofSummable, map_add]32 map_smul' c x := by33 apply evalZero_injective D34 simp only [evalZero_ofSummable, map_smul, RingHom.id_apply]3536theorem norm_commutingLiftLinear_le (x : Space D) :37 ‖commutingLiftLinear D h0 T hc x‖ ≤ ‖T‖ * ‖x‖ := by38 change ‖ofSummable D h0 (T (evalZero D x)) (summable_commuting_image D T hc x)‖ ≤ _39 rw [norm_ofSummable, norm_eq_tsum, ← tsum_mul_left]40 apply (summable_commuting_image D T hc x).tsum_le_tsum _41 ((L1Sum.summable_norm (x : Ambient (Y := Y))).mul_left ‖T‖)42 intro n43 rw [← hc, ← coord_eq]44 exact T.le_opNorm _4546def commutingLift : Space D →L[𝕜] Space D :=47 (commutingLiftLinear D h0 T hc).mkContinuous ‖T‖ (norm_commutingLiftLinear_le D h0 T hc)4849@[simp] theorem evalZero_commutingLift (x : Space D) :50 evalZero D (commutingLift D h0 T hc x) = T (evalZero D x) :=51 evalZero_ofSummable D h0 _ (summable_commuting_image D T hc x)5253@[simp] theorem coord_commutingLift (n : ℕ) (x : Space D) :54 coord D n (commutingLift D h0 T hc x) = T (coord D n x) := by55 change D n (T (evalZero D x)) = T (coord D n x)56 rw [← hc, coord_eq]5758theorem norm_commutingLift_le : ‖commutingLift D h0 T hc‖ ≤ ‖T‖ :=59 ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg T)60 (norm_commutingLiftLinear_le D h0 T hc)6162theorem commutingLift_isProjection (hT : IsProjection T) :63 IsProjection (commutingLift D h0 T hc) := by64 apply ContinuousLinearMap.ext65 intro x66 apply evalZero_injective D67 simp only [ContinuousLinearMap.comp_apply, evalZero_commutingLift]68 exact DFunLike.congr_fun hT (evalZero D x)6970theorem commutingLift_comp_eq_left (U : Y →L[𝕜] Y)71 (hu : ∀ n y, U (D n y) = D n (U y)) (hTU : T.comp U = T) :72 (commutingLift D h0 T hc).comp (commutingLift D h0 U hu) =73 commutingLift D h0 T hc := by74 apply ContinuousLinearMap.ext75 intro x76 apply evalZero_injective D77 simp only [ContinuousLinearMap.comp_apply, evalZero_commutingLift]78 exact DFunLike.congr_fun hTU (evalZero D x)7980def commutingLiftRangeMap : (commutingLift D h0 T hc).range →ₗ[𝕜] T.range :=81 ((evalZero D).toLinearMap.comp (commutingLift D h0 T hc).range.subtype).codRestrict _ (by82 rintro ⟨x, y, hy⟩83 refine ⟨evalZero D y, ?_⟩84 change T (evalZero D y) = evalZero D x85 rw [← hy]86 exact (evalZero_commutingLift D h0 T hc y).symm)8788theorem commutingLiftRangeMap_injective :89 Function.Injective (commutingLiftRangeMap D h0 T hc) := by90 intro x y h91 apply Subtype.ext92 apply evalZero_injective D93 exact congrArg Subtype.val h9495theorem commutingLift_range_finiteDimensional [FiniteDimensional 𝕜 T.range] :96 FiniteDimensional 𝕜 (commutingLift D h0 T hc).range :=97 FiniteDimensional.of_injective (commutingLiftRangeMap D h0 T hc)98 (commutingLiftRangeMap_injective D h0 T hc)99100theorem finrank_commutingLift_range_le [FiniteDimensional 𝕜 T.range] :101 Module.finrank 𝕜 (commutingLift D h0 T hc).range ≤ Module.finrank 𝕜 T.range :=102 LinearMap.finrank_le_finrank_of_injective (commutingLiftRangeMap_injective D h0 T hc)103104theorem commutingLift_tendsto105 (S : ℕ → Y →L[𝕜] Y) (hS : ∀ m, ‖S m‖ ≤ 1)106 (hcomm : ∀ m n y, S m (D n y) = D n (S m y))107 (hstrong : ∀ y, Tendsto (fun m => S m y) atTop (𝓝 y)) (x : Space D) :108 Tendsto (fun m => commutingLift D h0 (S m) (hcomm m) x) atTop (𝓝 x) := by109 have hsum : Summable (fun n => 2 * ‖coord D n x‖) :=110 (L1Sum.summable_norm (x : Ambient (Y := Y))).mul_left 2111 have ht : Tendsto (fun m => ∑' n, ‖S m (coord D n x) - coord D n x‖) atTop (𝓝 0) := by112 have h := tendsto_tsum_of_dominated_convergence113 (f := fun m n => ‖S m (coord D n x) - coord D n x‖)114 (g := fun _ : ℕ => (0 : ℝ)) (𝓕 := atTop) hsum115 (fun n => by simpa only [sub_self, norm_zero] using116 ((hstrong (coord D n x)).sub (tendsto_const_nhds :117 Tendsto (fun _ : ℕ => coord D n x) atTop (𝓝 (coord D n x)))).norm)118 (Eventually.of_forall (fun m n => by119 rw [norm_norm]120 have hbound : ‖S m (coord D n x)‖ ≤ ‖coord D n x‖ :=121 ((S m).le_opNorm _).trans (by122 simpa only [one_mul] using mul_le_mul_of_nonneg_right (hS m) (norm_nonneg _))123 exact (norm_sub_le _ _).trans (by linarith)))124 simpa only [tsum_zero] using h125 apply tendsto_iff_norm_sub_tendsto_zero.mpr126 simpa only [norm_eq_tsum, map_sub, coord_commutingLift] using ht127128end PL1.IntrinsicGraph129