Exact source: MathlibAnnex/Analysis/Normed/Module/EquivalentSeminorm/Transport.lean
Pinned GitHub source · Raw UTF-8 source
Back to The unit-sphere chord metric determines the ambient normed space
1import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Topology2import Mathlib.Analysis.Normed.Operator.LinearIsometry3import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap4import Mathlib.Topology.MetricSpace.Isometry56/-!7# Transport to the norm of an equivalent seminorm89`Space M` is a separate carrier whose norm is `M.p`. The original carrier retains10its reference norm. Public transport equations use explicit carrier identities,11so their statements expose no private helper names.12-/1314noncomputable section1516namespace MathlibAnnex.EquivalentSeminorm1718variable {E F X Y : Type*}19 [NormedAddCommGroup E] [NormedSpace ℝ E]20 [NormedAddCommGroup F] [NormedSpace ℝ F]21 [NormedAddCommGroup X] [NormedSpace ℝ X]22 [NormedAddCommGroup Y] [NormedSpace ℝ Y]2324/-- A separate copy of the carrier, equipped below with the model norm. -/25def Space (_M : EquivalentSeminorm E) := E2627variable (M : EquivalentSeminorm E)2829instance : AddCommGroup (Space M) := inferInstanceAs (AddCommGroup E)30instance : Module ℝ (Space M) := inferInstanceAs (Module ℝ E)31instance : Norm (Space M) := ⟨fun x => M.p (show E from x)⟩3233private theorem normedSpaceCore_space : NormedSpace.Core ℝ (Space M) where34 norm_nonneg x := apply_nonneg M.p (show E from x)35 norm_smul c x := by36 change M.p (c • (show E from x)) = ‖c‖ * M.p (show E from x)37 exact map_smul_eq_mul M.p c (show E from x)38 norm_triangle x y := map_add_le_add M.p (show E from x) (show E from y)39 norm_eq_zero_iff x := by40 change M.p (show E from x) = 0 ↔ (show E from x) = 041 exact ⟨M.eq_zero_of_apply_eq_zero, fun h => by simp [h]⟩4243instance : NormedAddCommGroup (Space M) := NormedAddCommGroup.ofCore (normedSpaceCore_space M)44instance : NormedSpace ℝ (Space M) := NormedSpace.ofCore (normedSpaceCore_space M)4546private def ofReference (x : E) : Space M := x47private def toReference (x : Space M) : E := x4849include M in50theorem toReference_ofReference (x : E) :51 (show E from (show Space M from x)) = x := rfl5253theorem ofReference_toReference (x : Space M) :54 (show Space M from (show E from x)) = x := rfl5556@[simp] theorem toReference_zero : (show E from (0 : Space M)) = 0 := rfl5758@[simp] theorem toReference_sub (x y : Space M) :59 (show E from (x - y)) = (show E from x) - (show E from y) := rfl6061@[simp] theorem toReference_sub_ofReference (x y : E) :62 (show E from ((show Space M from x) - (show Space M from y))) = x - y := rfl6364@[simp] theorem norm_space_eq (x : Space M) : ‖x‖ = M.p (show E from x) := rfl6566/-- Model distance is exactly the seminorm of the reference difference. -/67theorem dist_space_eq (x y : Space M) :68 dist x y = M.p ((show E from x) - (show E from y)) := by69 rw [dist_eq_norm]70 rfl7172@[simp] theorem sphere_apply (u : Metric.sphere (0 : Space M) 1) :73 M.p (show E from u.val) = 1 :=74 mem_sphere_zero_iff_norm.mp u.property7576/-- A linear equivalence preserving the two stored seminorms. -/77structure LinearIsometryEquiv (MX : EquivalentSeminorm E) (MY : EquivalentSeminorm F) where78 toLinearEquiv : E ≃ₗ[ℝ] F79 map_p_eq : ∀ x, MY.p (toLinearEquiv x) = MX.p x8081/-- Pull the target norm back along a continuous linear equivalence.82The maxima with `1` keep both comparison constants positive in dimension zero. -/83def ofContinuousLinearEquiv (e : E ≃L[ℝ] X) : EquivalentSeminorm E where84 p := (normSeminorm ℝ X).comp e.toLinearMap85 lower := (max ‖(e.symm : X →L[ℝ] E)‖ 1)⁻¹86 upper := max ‖(e : E →L[ℝ] X)‖ 187 lower_pos := inv_pos.mpr (lt_of_lt_of_le zero_lt_one (le_max_right _ _))88 upper_pos := lt_of_lt_of_le zero_lt_one (le_max_right _ _)89 lower_le := by90 intro x91 have hD : 0 < max ‖(e.symm : X →L[ℝ] E)‖ 1 :=92 lt_of_lt_of_le zero_lt_one (le_max_right _ _)93 have hbase : ‖x‖ ≤ ‖(e.symm : X →L[ℝ] E)‖ * ‖e x‖ := by94 simpa using ((e.symm : X →L[ℝ] E).le_opNorm (e x))95 have hmax : ‖x‖ ≤ max ‖(e.symm : X →L[ℝ] E)‖ 1 * ‖e x‖ :=96 hbase.trans (mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _))97 calc98 (max ‖(e.symm : X →L[ℝ] E)‖ 1)⁻¹ * ‖x‖ ≤99 (max ‖(e.symm : X →L[ℝ] E)‖ 1)⁻¹ *100 (max ‖(e.symm : X →L[ℝ] E)‖ 1 * ‖e x‖) :=101 mul_le_mul_of_nonneg_left hmax (inv_nonneg.mpr hD.le)102 _ = ‖e x‖ := by rw [← mul_assoc, inv_mul_cancel₀ hD.ne', one_mul]103 le_upper := by104 intro x105 calc106 ‖e x‖ ≤ ‖(e : E →L[ℝ] X)‖ * ‖x‖ := (e : E →L[ℝ] X).le_opNorm x107 _ ≤ max ‖(e : E →L[ℝ] X)‖ 1 * ‖x‖ :=108 mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _)109 continuous_p := by110 change Continuous (fun x : E => ‖e x‖)111 exact continuous_norm.comp e.continuous112113namespace Internal114115private def coordinateSeminorm (e : E ≃L[ℝ] X) : Seminorm ℝ E :=116 (normSeminorm ℝ X).comp e.toLinearMap117118@[simp] private theorem coordinateSeminorm_apply (e : E ≃L[ℝ] X) (x : E) :119 coordinateSeminorm e x = ‖e x‖ := rfl120121end Internal122123@[simp] theorem ofContinuousLinearEquiv_p_apply (e : E ≃L[ℝ] X) (x : E) :124 (ofContinuousLinearEquiv e).p x = ‖e x‖ := Internal.coordinateSeminorm_apply e x125126/-- Coordinate equivalence of the model sphere and the original target sphere. -/127def unitSphereEquiv (e : E ≃L[ℝ] X) :128 Metric.sphere (0 : Space (ofContinuousLinearEquiv e)) 1 ≃129 Metric.sphere (0 : X) 1 where130 toFun u := ⟨e (show E from u.val), by131 apply mem_sphere_zero_iff_norm.mpr132 exact sphere_apply (ofContinuousLinearEquiv e) u⟩133 invFun u := ⟨(show Space (ofContinuousLinearEquiv e) from e.symm u.val), by134 apply mem_sphere_zero_iff_norm.mpr135 change ‖e (e.symm u.val)‖ = 1136 rw [e.apply_symm_apply]137 exact mem_sphere_zero_iff_norm.mp u.property⟩138 left_inv u := by apply Subtype.ext; exact e.symm_apply_apply (show E from u.val)139 right_inv u := by apply Subtype.ext; exact e.apply_symm_apply u.val140141/-- Transport a sphere isometry to the two model normed spaces. -/142def sphereIsometryEquiv (eX : E ≃L[ℝ] X) (eY : F ≃L[ℝ] Y)143 (Δ : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :144 Metric.sphere (0 : Space (ofContinuousLinearEquiv eX)) 1 ≃ᵢ145 Metric.sphere (0 : Space (ofContinuousLinearEquiv eY)) 1 := by146 let cX := unitSphereEquiv eX147 let cY := unitSphereEquiv eY148 refine { toEquiv := cX.trans (Δ.toEquiv.trans cY.symm), isometry_toFun := ?_ }149 apply isometry_iff_dist_eq.mpr150 intro u v151 change dist (cY.symm (Δ (cX u))) (cY.symm (Δ (cX v))) = dist u v152 have hx : ∀ a b, dist (cX a) (cX b) = dist a b := by153 intro a b154 rw [Subtype.dist_eq, Subtype.dist_eq, dist_eq_norm, dist_space_eq]155 change ‖eX (show E from a.val) - eX (show E from b.val)‖ =156 ‖eX ((show E from a.val) - (show E from b.val))‖157 rw [map_sub]158 have hy : ∀ a b, dist (cY.symm a) (cY.symm b) = dist a b := by159 intro a b160 rw [Subtype.dist_eq, Subtype.dist_eq, dist_space_eq, dist_eq_norm]161 change ‖eY (eY.symm a.val - eY.symm b.val)‖ = ‖a.val - b.val‖162 rw [map_sub, eY.apply_symm_apply, eY.apply_symm_apply]163 rw [hy, Δ.isometry.dist_eq, hx]164165/-- Transport a model norm preserving linear equivalence to the original spaces. -/166def transportLinearIsometryEquiv (eX : E ≃L[ℝ] X) (eY : F ≃L[ℝ] Y)167 (A : LinearIsometryEquiv (ofContinuousLinearEquiv eX) (ofContinuousLinearEquiv eY)) :168 X ≃ₗᵢ[ℝ] Y := by169 let L : X ≃ₗ[ℝ] Y := eX.toLinearEquiv.symm.trans (A.toLinearEquiv.trans eY.toLinearEquiv)170 exact {171 toLinearEquiv := L172 norm_map' := by173 intro x174 have h := A.map_p_eq (eX.symm x)175 simpa [L] using h }176177end MathlibAnnex.EquivalentSeminorm