feat(Analysis): operator norm of a LinearIsometryEquiv (leanprover-community#39143)

Also generalise a bunch of lemmas from `NormedAddCommGroup` + `Nontrivial` to `SeminormedAddCommGroup` + `NontrivialTopology`.

From MeanFourier

Author: YaelDillies

Mathlib/Analysis/Normed/Operator/NormedSpace.lean

@@ -26,6 +26,64 @@ open scoped NNReal
 -- the `ₗ` subscript variables are for special cases about linear (as opposed to semilinear) maps
 variable {𝕜 𝕜₂ 𝕜₃ E F Fₗ G : Type*}
 
+section SeminormedAddCommGroup
+variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G]
+  [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃]
+  [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G]
+  {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₂] F)
+
+namespace LinearIsometry
+section
+variable [NontrivialTopology E] [RingHomIsometric σ₁₂]
+
+@[simp] lemma norm_toContinuousLinearMap (f : E →ₛₗᵢ[σ₁₂] F) : ‖f.toContinuousLinearMap‖ = 1 :=
+  f.toContinuousLinearMap.homothety_norm <| by simp
+
+@[simp] lemma nnnorm_toContinuousLinearMap (f : E →ₛₗᵢ[σ₁₂] F) : ‖f.toContinuousLinearMap‖₊ = 1 :=
+  Subtype.ext f.norm_toContinuousLinearMap
+
+@[simp] lemma enorm_toContinuousLinearMap (f : E →ₛₗᵢ[σ₁₂] F) : ‖f.toContinuousLinearMap‖ₑ = 1 :=
+  congrArg _ f.nnnorm_toContinuousLinearMap
+
+end
+
+variable {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
+
+/-- Postcomposition of a continuous linear map with a linear isometry preserves
+the operator norm. -/
+lemma norm_toContinuousLinearMap_comp [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G)
+    {g : E →SL[σ₁₂] F} : ‖f.toContinuousLinearMap.comp g‖ = ‖g‖ :=
+  (f.toContinuousLinearMap.comp g).opNorm_ext g fun x ↦ by simp
+
+/-- Composing on the left with a linear isometry gives a linear isometry between spaces of
+continuous linear maps. -/
+def postcomp [RingHomIsometric σ₁₂] [RingHomIsometric σ₁₃] (a : F →ₛₗᵢ[σ₂₃] G) :
+    (E →SL[σ₁₂] F) →ₛₗᵢ[σ₂₃] (E →SL[σ₁₃] G) where
+  toFun f := a.toContinuousLinearMap.comp f
+  map_add' f g := by simp
+  map_smul' c f := by simp
+  norm_map' f := by simp [a.norm_toContinuousLinearMap_comp]
+
+end LinearIsometry
+
+namespace LinearIsometryEquiv
+variable [NontrivialTopology E] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
+  [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₁₂]
+
+@[simp] lemma norm_toContinuousLinearMap (e : E ≃ₛₗᵢ[σ₁₂] F) :
+    ‖e.toContinuousLinearEquiv.toContinuousLinearMap‖ = 1 :=
+  e.toLinearIsometry.norm_toContinuousLinearMap
+
+@[simp] lemma nnnorm_toContinuousLinearMap (e : E ≃ₛₗᵢ[σ₁₂] F) :
+    ‖e.toContinuousLinearEquiv.toContinuousLinearMap‖₊ = 1 :=
+  e.toLinearIsometry.nnnorm_toContinuousLinearMap
+
+@[simp] lemma enorm_toContinuousLinearMap (e : E ≃ₛₗᵢ[σ₁₂] F) :
+    ‖e.toContinuousLinearEquiv.toContinuousLinearMap‖ₑ = 1 :=
+  e.toLinearIsometry.enorm_toContinuousLinearMap
+
+end LinearIsometryEquiv
+end SeminormedAddCommGroup
 
 section Normed
 
@@ -91,8 +149,6 @@ end LinearMap
 
 namespace ContinuousLinearMap
 
-section OpNorm
-
 open Set Real
 
 /-- An operator is zero iff its norm vanishes. -/
@@ -121,47 +177,8 @@ theorem antilipschitz_of_isEmbedding (f : E →L[𝕜] Fₗ) (hf : IsEmbedding f
     ∃ K, AntilipschitzWith K f :=
   f.toLinearMap.antilipschitz_of_comap_nhds_le <| map_zero f ▸ (hf.nhds_eq_comap 0).ge
 
-end OpNorm
-
 end ContinuousLinearMap
 
-namespace LinearIsometry
-
-@[simp]
-theorem norm_toContinuousLinearMap [Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :
-    ‖f.toContinuousLinearMap‖ = 1 :=
-  f.toContinuousLinearMap.homothety_norm <| by simp
-
-@[simp]
-theorem nnnorm_toContinuousLinearMap [Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :
-    ‖f.toContinuousLinearMap‖₊ = 1 :=
-  Subtype.ext f.norm_toContinuousLinearMap
-
-@[simp]
-theorem enorm_toContinuousLinearMap [Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :
-    ‖f.toContinuousLinearMap‖ₑ = 1 :=
-  congrArg _ f.nnnorm_toContinuousLinearMap
-
-variable {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
-
-/-- Postcomposition of a continuous linear map with a linear isometry preserves
-the operator norm. -/
-theorem norm_toContinuousLinearMap_comp [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G)
-    {g : E →SL[σ₁₂] F} : ‖f.toContinuousLinearMap.comp g‖ = ‖g‖ :=
-  opNorm_ext (f.toContinuousLinearMap.comp g) g fun x => by
-    simp only [norm_map, coe_toContinuousLinearMap, coe_comp', Function.comp_apply]
-
-/-- Composing on the left with a linear isometry gives a linear isometry between spaces of
-continuous linear maps. -/
-def postcomp [RingHomIsometric σ₁₂] [RingHomIsometric σ₁₃] (a : F →ₛₗᵢ[σ₂₃] G) :
-    (E →SL[σ₁₂] F) →ₛₗᵢ[σ₂₃] (E →SL[σ₁₃] G) where
-  toFun f := a.toContinuousLinearMap.comp f
-  map_add' f g := by simp
-  map_smul' c f := by simp
-  norm_map' f := by simp [a.norm_toContinuousLinearMap_comp]
-
-end LinearIsometry
-
 end
 
 namespace ContinuousLinearMap
@@ -272,7 +289,7 @@ end Normed
 /-- A bounded bilinear form `B` in a real normed space is *coercive*
 if there is some positive constant C such that `C * ‖u‖ * ‖u‖ ≤ B u u`.
 -/
-def IsCoercive [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) : Prop :=
+def IsCoercive [SeminormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) : Prop :=
   ∃ C, 0 < C ∧ ∀ u, C * ‖u‖ * ‖u‖ ≤ B u u
 
 section Equicontinuous
@@ -348,8 +365,8 @@ lemma ContinuousLinearMap.norm_single_le_one [∀ i, SeminormedAddCommGroup (E i
     ‖ContinuousLinearMap.single 𝕜 E i‖ ≤ 1 :=
   (LinearIsometry.single 𝕜 E i).norm_toContinuousLinearMap_le
 
-lemma ContinuousLinearMap.norm_single [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
-    (i : ι) [Nontrivial (E i)] :
+lemma ContinuousLinearMap.norm_single [∀ i, SeminormedAddCommGroup (E i)]
+    [∀ i, NormedSpace 𝕜 (E i)] (i : ι) [NontrivialTopology (E i)] :
     ‖ContinuousLinearMap.single 𝕜 E i‖ = 1 :=
   (LinearIsometry.single 𝕜 E i).norm_toContinuousLinearMap
 
@@ -389,13 +406,13 @@ lemma ContinuousLinearMap.norm_inr_le_one [SeminormedAddCommGroup E] [NormedSpac
     ‖ContinuousLinearMap.inr 𝕜 E F‖ ≤ 1 :=
   (LinearIsometry.inr 𝕜 E F).norm_toContinuousLinearMap_le
 
-lemma ContinuousLinearMap.norm_inl [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Nontrivial E] :
+lemma ContinuousLinearMap.norm_inl [SeminormedAddCommGroup E] [NontrivialTopology E]
+    [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :
     ‖ContinuousLinearMap.inl 𝕜 E F‖ = 1 :=
   (LinearIsometry.inl 𝕜 E F).norm_toContinuousLinearMap
 
-lemma ContinuousLinearMap.norm_inr [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Nontrivial F] :
+lemma ContinuousLinearMap.norm_inr [SeminormedAddCommGroup E] [NontrivialTopology E]
+    [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NontrivialTopology F] :
     ‖ContinuousLinearMap.inr 𝕜 E F‖ = 1 :=
   (LinearIsometry.inr 𝕜 E F).norm_toContinuousLinearMap
 

Mathlib/Topology/ContinuousMap/Compact.lean

@@ -180,6 +180,10 @@ instance {E : Type*} [NormedAddCommGroup E] : NormedAddCommGroup C(α, E) where
   __ : SeminormedAddCommGroup C(α, E) := inferInstance
   __ : MetricSpace C(α, E) := inferInstance
 
+instance [Nonempty α] {E : Type*} [NormedAddCommGroup E] [Nontrivial E] :
+    NontrivialTopology C(α, E) := by
+  simpa [nontrivialTopology_iff_exists_norm_ne_zero] using exists_ne (0 : C(α, E))
+
 instance [Nonempty α] [One E] [NormOneClass E] : NormOneClass C(α, E) where
   norm_one := by simp only [← norm_mkOfCompact, mkOfCompact_one, norm_one]
 

Mathlib/Topology/Order.lean

@@ -542,6 +542,9 @@ instance (priority := 100) Subsingleton.discreteTopology [t : TopologicalSpace 
 instance [TopologicalSpace α] [Subsingleton α] : IndiscreteTopology α where
   eq_top := Subsingleton.elim _ _
 
+variable (α) in
+lemma Nontrivial.of_nontrivialTopology [TopologicalSpace α] [h : NontrivialTopology α] :
+    Nontrivial α := by contrapose! h; infer_instance
 
 instance : TopologicalSpace Empty := ⊥
 instance : DiscreteTopology Empty := ⟨rfl⟩