From ac537a4a8fe7098691db632b0e1f493b8c993b61 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 23 Sep 2024 11:56:11 +0000 Subject: [PATCH] chore: generalize `IsBoundedBilinearMap` to seminormed spaces (#17011) The claim in `Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean` that > This file contains statements about operator norm for which it really matters that the > underlying space has a norm (rather than just a seminorm). was not entirely true. The main trick is to case on whether the norm of an element is zero, rather than on that element itself being zero. Unfortunately this causes some minor elaboration issues downstream, but they are easy to work around. --- Mathlib/Analysis/Calculus/ContDiff/Basic.lean | 2 +- Mathlib/Analysis/Calculus/FDeriv/Mul.lean | 15 +++--- .../Analysis/InnerProductSpace/Calculus.lean | 9 ++-- .../Normed/Operator/BoundedLinearMaps.lean | 25 +++++---- .../NormedSpace/OperatorNorm/Bilinear.lean | 48 +++++++++++++++++ .../NormedSpace/OperatorNorm/NormedSpace.lean | 52 ------------------- 6 files changed, 79 insertions(+), 72 deletions(-) diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index eecfb2a1688da..f9cc1aee3a4f1 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -802,7 +802,7 @@ theorem ContDiff.clm_comp {g : X β†’ F β†’L[π•œ] G} {f : X β†’ E β†’L[π•œ] F} theorem ContDiffOn.clm_comp {g : X β†’ F β†’L[π•œ] G} {f : X β†’ E β†’L[π•œ] F} {s : Set X} (hg : ContDiffOn π•œ n g s) (hf : ContDiffOn π•œ n f s) : ContDiffOn π•œ n (fun x => (g x).comp (f x)) s := - isBoundedBilinearMap_comp.contDiff.comp_contDiff_onβ‚‚ hg hf + (isBoundedBilinearMap_comp (π•œ := π•œ) (E := E) (F := F) (G := G)).contDiff.comp_contDiff_onβ‚‚ hg hf theorem ContDiff.clm_apply {f : E β†’ F β†’L[π•œ] G} {g : E β†’ F} {n : β„•βˆž} (hf : ContDiff π•œ n f) (hg : ContDiff π•œ n g) : ContDiff π•œ n fun x => (f x) (g x) := diff --git a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean index 9c79b4bf2279c..47dd475da18fc 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean @@ -50,20 +50,20 @@ variable {H : Type*} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G theorem HasStrictFDerivAt.clm_comp (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) : HasStrictFDerivAt (fun y => (c y).comp (d y)) ((compL π•œ F G H (c x)).comp d' + ((compL π•œ F G H).flip (d x)).comp c') x := - (isBoundedBilinearMap_comp.hasStrictFDerivAt (c x, d x)).comp x <| hc.prod hd + (isBoundedBilinearMap_comp.hasStrictFDerivAt (c x, d x) :).comp x <| hc.prod hd @[fun_prop] theorem HasFDerivWithinAt.clm_comp (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) : HasFDerivWithinAt (fun y => (c y).comp (d y)) ((compL π•œ F G H (c x)).comp d' + ((compL π•œ F G H).flip (d x)).comp c') s x := - (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp_hasFDerivWithinAt x <| hc.prod hd + (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x) :).comp_hasFDerivWithinAt x <| hc.prod hd @[fun_prop] theorem HasFDerivAt.clm_comp (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) : HasFDerivAt (fun y => (c y).comp (d y)) ((compL π•œ F G H (c x)).comp d' + ((compL π•œ F G H).flip (d x)).comp c') x := - (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp x <| hc.prod hd + (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x) :).comp x <| hc.prod hd @[fun_prop] theorem DifferentiableWithinAt.clm_comp (hc : DifferentiableWithinAt π•œ c s x) @@ -107,12 +107,12 @@ theorem HasStrictFDerivAt.clm_apply (hc : HasStrictFDerivAt c c' x) theorem HasFDerivWithinAt.clm_apply (hc : HasFDerivWithinAt c c' s x) (hu : HasFDerivWithinAt u u' s x) : HasFDerivWithinAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x := - (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp_hasFDerivWithinAt x (hc.prod hu) + (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x) :).comp_hasFDerivWithinAt x (hc.prod hu) @[fun_prop] theorem HasFDerivAt.clm_apply (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) : HasFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x := - (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp x (hc.prod hu) + (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x) :).comp x (hc.prod hu) @[fun_prop] theorem DifferentiableWithinAt.clm_apply (hc : DifferentiableWithinAt π•œ c s x) @@ -239,12 +239,13 @@ theorem HasStrictFDerivAt.smul (hc : HasStrictFDerivAt c c' x) (hf : HasStrictFD @[fun_prop] theorem HasFDerivWithinAt.smul (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun y => c y β€’ f y) (c x β€’ f' + c'.smulRight (f x)) s x := - (isBoundedBilinearMap_smul.hasFDerivAt (c x, f x)).comp_hasFDerivWithinAt x <| hc.prod hf + (isBoundedBilinearMap_smul.hasFDerivAt (π•œ := π•œ) (c x, f x) :).comp_hasFDerivWithinAt x <| + hc.prod hf @[fun_prop] theorem HasFDerivAt.smul (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) : HasFDerivAt (fun y => c y β€’ f y) (c x β€’ f' + c'.smulRight (f x)) x := - (isBoundedBilinearMap_smul.hasFDerivAt (c x, f x)).comp x <| hc.prod hf + (isBoundedBilinearMap_smul.hasFDerivAt (π•œ := π•œ) (c x, f x) :).comp x <| hc.prod hf @[fun_prop] theorem DifferentiableWithinAt.smul (hc : DifferentiableWithinAt π•œ c s x) diff --git a/Mathlib/Analysis/InnerProductSpace/Calculus.lean b/Mathlib/Analysis/InnerProductSpace/Calculus.lean index 031592910f445..44808e4d72423 100644 --- a/Mathlib/Analysis/InnerProductSpace/Calculus.lean +++ b/Mathlib/Analysis/InnerProductSpace/Calculus.lean @@ -80,15 +80,18 @@ theorem HasFDerivWithinAt.inner (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) : HasFDerivWithinAt (fun t => βŸͺf t, g t⟫) ((fderivInnerCLM π•œ (f x, g x)).comp <| f'.prod g') s x := - (isBoundedBilinearMap_inner.hasFDerivAt (f x, g x)).comp_hasFDerivWithinAt x (hf.prod hg) + isBoundedBilinearMap_inner (π•œ := π•œ) (E := E) + |>.hasFDerivAt (f x, g x) |>.comp_hasFDerivWithinAt x (hf.prod hg) theorem HasStrictFDerivAt.inner (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) : HasStrictFDerivAt (fun t => βŸͺf t, g t⟫) ((fderivInnerCLM π•œ (f x, g x)).comp <| f'.prod g') x := - (isBoundedBilinearMap_inner.hasStrictFDerivAt (f x, g x)).comp x (hf.prod hg) + isBoundedBilinearMap_inner (π•œ := π•œ) (E := E) + |>.hasStrictFDerivAt (f x, g x) |>.comp x (hf.prod hg) theorem HasFDerivAt.inner (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) : HasFDerivAt (fun t => βŸͺf t, g t⟫) ((fderivInnerCLM π•œ (f x, g x)).comp <| f'.prod g') x := - (isBoundedBilinearMap_inner.hasFDerivAt (f x, g x)).comp x (hf.prod hg) + isBoundedBilinearMap_inner (π•œ := π•œ) (E := E) + |>.hasFDerivAt (f x, g x) |>.comp x (hf.prod hg) theorem HasDerivWithinAt.inner {f g : ℝ β†’ E} {f' g' : E} {s : Set ℝ} {x : ℝ} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) : diff --git a/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean b/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean index 114bd3205cea4..4d0fea4e147c4 100644 --- a/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean +++ b/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean @@ -59,14 +59,14 @@ open Filter (Tendsto) open Metric ContinuousLinearMap -variable {π•œ : Type*} [NontriviallyNormedField π•œ] {E : Type*} [NormedAddCommGroup E] - [NormedSpace π•œ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type*} - [NormedAddCommGroup G] [NormedSpace π•œ G] +variable {π•œ : Type*} [NontriviallyNormedField π•œ] {E : Type*} [SeminormedAddCommGroup E] + [NormedSpace π•œ E] {F : Type*} [SeminormedAddCommGroup F] [NormedSpace π•œ F] {G : Type*} + [SeminormedAddCommGroup G] [NormedSpace π•œ G] /-- A function `f` satisfies `IsBoundedLinearMap π•œ f` if it is linear and satisfies the inequality `β€–f xβ€– ≀ M * β€–xβ€–` for some positive constant `M`. -/ -structure IsBoundedLinearMap (π•œ : Type*) [NormedField π•œ] {E : Type*} [NormedAddCommGroup E] - [NormedSpace π•œ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) extends +structure IsBoundedLinearMap (π•œ : Type*) [NormedField π•œ] {E : Type*} [SeminormedAddCommGroup E] + [NormedSpace π•œ E] {F : Type*} [SeminormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) extends IsLinearMap π•œ f : Prop where bound : βˆƒ M, 0 < M ∧ βˆ€ x : E, β€–f xβ€– ≀ M * β€–xβ€– @@ -186,7 +186,7 @@ variable {ΞΉ : Type*} [Fintype ΞΉ] /-- Taking the cartesian product of two continuous multilinear maps is a bounded linear operation. -/ -theorem isBoundedLinearMap_prod_multilinear {E : ΞΉ β†’ Type*} [βˆ€ i, NormedAddCommGroup (E i)] +theorem isBoundedLinearMap_prod_multilinear {E : ΞΉ β†’ Type*} [βˆ€ i, SeminormedAddCommGroup (E i)] [βˆ€ i, NormedSpace π•œ (E i)] : IsBoundedLinearMap π•œ fun p : ContinuousMultilinearMap π•œ E F Γ— ContinuousMultilinearMap π•œ E G => p.1.prod p.2 where @@ -244,7 +244,7 @@ variable {R : Type*} variable {π•œβ‚‚ π•œ' : Type*} [NontriviallyNormedField π•œ'] [NontriviallyNormedField π•œβ‚‚] variable {M : Type*} [TopologicalSpace M] variable {σ₁₂ : π•œ β†’+* π•œβ‚‚} -variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace π•œβ‚‚ G'] [NormedSpace π•œ' G'] +variable {G' : Type*} [SeminormedAddCommGroup G'] [NormedSpace π•œβ‚‚ G'] [NormedSpace π•œ' G'] variable [SMulCommClass π•œβ‚‚ π•œ' G'] section Semiring @@ -374,7 +374,7 @@ theorem IsBoundedBilinearMap.isBoundedLinearMap_right (h : IsBoundedBilinearMap (h.toContinuousLinearMap x).isBoundedLinearMap theorem isBoundedBilinearMap_smul {π•œ' : Type*} [NormedField π•œ'] [NormedAlgebra π•œ π•œ'] {E : Type*} - [NormedAddCommGroup E] [NormedSpace π•œ E] [NormedSpace π•œ' E] [IsScalarTower π•œ π•œ' E] : + [SeminormedAddCommGroup E] [NormedSpace π•œ E] [NormedSpace π•œ' E] [IsScalarTower π•œ π•œ' E] : IsBoundedBilinearMap π•œ fun p : π•œ' Γ— E => p.1 β€’ p.2 := (lsmul π•œ π•œ' : π•œ' β†’L[π•œ] E β†’L[π•œ] E).isBoundedBilinearMap @@ -436,7 +436,7 @@ variable (π•œ) /-- The function `ContinuousLinearMap.mulLeftRight : π•œ' Γ— π•œ' β†’ (π•œ' β†’L[π•œ] π•œ')` is a bounded bilinear map. -/ -theorem ContinuousLinearMap.mulLeftRight_isBoundedBilinear (π•œ' : Type*) [NormedRing π•œ'] +theorem ContinuousLinearMap.mulLeftRight_isBoundedBilinear (π•œ' : Type*) [SeminormedRing π•œ'] [NormedAlgebra π•œ π•œ'] : IsBoundedBilinearMap π•œ fun p : π•œ' Γ— π•œ' => ContinuousLinearMap.mulLeftRight π•œ π•œ' p.1 p.2 := (ContinuousLinearMap.mulLeftRight π•œ π•œ').isBoundedBilinearMap @@ -471,9 +471,16 @@ theorem ContinuousOn.clm_apply {X} [TopologicalSpace X] {f : X β†’ (E β†’L[π•œ] ContinuousOn (fun x ↦ f x (g x)) s := isBoundedBilinearMap_apply.continuous.comp_continuousOn (hf.prod hg) +end + namespace ContinuousLinearEquiv +variable {π•œ : Type*} [NontriviallyNormedField π•œ] +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace π•œ E] +variable {F : Type*} [SeminormedAddCommGroup F] [NormedSpace π•œ F] + open Set +open scoped Topology /-! ### The set of continuous linear equivalences between two Banach spaces is open diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean index 1d70cb3750159..61f5199b50531 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean @@ -409,6 +409,54 @@ theorem map_add_add (f : E β†’L[π•œ] Fβ‚— β†’L[π•œ] Gβ‚—) (x x' : E) (y y' : F simp only [map_add, add_apply, coe_derivβ‚‚, add_assoc] abel +/-- The norm of the tensor product of a scalar linear map and of an element of a normed space +is the product of the norms. -/ +@[simp] +theorem norm_smulRight_apply (c : E β†’L[π•œ] π•œ) (f : Fβ‚—) : β€–smulRight c fβ€– = β€–cβ€– * β€–fβ€– := by + refine le_antisymm ?_ ?_ + Β· refine opNorm_le_bound _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) fun x => ?_ + calc + β€–c x β€’ fβ€– = β€–c xβ€– * β€–fβ€– := norm_smul _ _ + _ ≀ β€–cβ€– * β€–xβ€– * β€–fβ€– := mul_le_mul_of_nonneg_right (le_opNorm _ _) (norm_nonneg _) + _ = β€–cβ€– * β€–fβ€– * β€–xβ€– := by ring + Β· obtain hf | hf := (norm_nonneg f).eq_or_gt + Β· simp [hf] + Β· rw [← le_div_iffβ‚€ hf] + refine opNorm_le_bound _ (div_nonneg (norm_nonneg _) (norm_nonneg f)) fun x => ?_ + rw [div_mul_eq_mul_div, le_div_iffβ‚€ hf] + calc + β€–c xβ€– * β€–fβ€– = β€–c x β€’ fβ€– := (norm_smul _ _).symm + _ = β€–smulRight c f xβ€– := rfl + _ ≀ β€–smulRight c fβ€– * β€–xβ€– := le_opNorm _ _ + +/-- The non-negative norm of the tensor product of a scalar linear map and of an element of a normed +space is the product of the non-negative norms. -/ +@[simp] +theorem nnnorm_smulRight_apply (c : E β†’L[π•œ] π•œ) (f : Fβ‚—) : β€–smulRight c fβ€–β‚Š = β€–cβ€–β‚Š * β€–fβ€–β‚Š := + NNReal.eq <| c.norm_smulRight_apply f + +variable (π•œ E Fβ‚—) in +/-- `ContinuousLinearMap.smulRight` as a continuous trilinear map: +`smulRightL (c : E β†’L[π•œ] π•œ) (f : F) (x : E) = c x β€’ f`. -/ +def smulRightL : (E β†’L[π•œ] π•œ) β†’L[π•œ] Fβ‚— β†’L[π•œ] E β†’L[π•œ] Fβ‚— := + LinearMap.mkContinuousβ‚‚ + { toFun := smulRightβ‚— + map_add' := fun c₁ cβ‚‚ => by + ext x + simp only [add_smul, coe_smulRightβ‚—, add_apply, smulRight_apply, LinearMap.add_apply] + map_smul' := fun m c => by + ext x + dsimp + rw [smul_smul] } + 1 fun c x => by + simp only [coe_smulRightβ‚—, one_mul, norm_smulRight_apply, LinearMap.coe_mk, AddHom.coe_mk, + le_refl] + + +@[simp] +theorem norm_smulRightL_apply (c : E β†’L[π•œ] π•œ) (f : Fβ‚—) : β€–smulRightL π•œ E Fβ‚— c fβ€– = β€–cβ€– * β€–fβ€– := + norm_smulRight_apply c f + end ContinuousLinearMap end SemiNormed diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean index d07b5ac33cae4..8530ba797f7ed 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean @@ -200,58 +200,6 @@ theorem opNorm_comp_linearIsometryEquiv (f : F β†’SL[σ₂₃] G) (g : F' ≃ₛ @[deprecated (since := "2024-02-02")] alias op_norm_comp_linearIsometryEquiv := opNorm_comp_linearIsometryEquiv -/-- The norm of the tensor product of a scalar linear map and of an element of a normed space -is the product of the norms. -/ -@[simp] -theorem norm_smulRight_apply (c : E β†’L[π•œ] π•œ) (f : Fβ‚—) : β€–smulRight c fβ€– = β€–cβ€– * β€–fβ€– := by - refine le_antisymm ?_ ?_ - Β· refine opNorm_le_bound _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) fun x => ?_ - calc - β€–c x β€’ fβ€– = β€–c xβ€– * β€–fβ€– := norm_smul _ _ - _ ≀ β€–cβ€– * β€–xβ€– * β€–fβ€– := mul_le_mul_of_nonneg_right (le_opNorm _ _) (norm_nonneg _) - _ = β€–cβ€– * β€–fβ€– * β€–xβ€– := by ring - Β· by_cases h : f = 0 - Β· simp [h] - Β· have : 0 < β€–fβ€– := norm_pos_iff.2 h - rw [← le_div_iffβ‚€ this] - refine opNorm_le_bound _ (div_nonneg (norm_nonneg _) (norm_nonneg f)) fun x => ?_ - rw [div_mul_eq_mul_div, le_div_iffβ‚€ this] - calc - β€–c xβ€– * β€–fβ€– = β€–c x β€’ fβ€– := (norm_smul _ _).symm - _ = β€–smulRight c f xβ€– := rfl - _ ≀ β€–smulRight c fβ€– * β€–xβ€– := le_opNorm _ _ - -/-- The non-negative norm of the tensor product of a scalar linear map and of an element of a normed -space is the product of the non-negative norms. -/ -@[simp] -theorem nnnorm_smulRight_apply (c : E β†’L[π•œ] π•œ) (f : Fβ‚—) : β€–smulRight c fβ€–β‚Š = β€–cβ€–β‚Š * β€–fβ€–β‚Š := - NNReal.eq <| c.norm_smulRight_apply f - -variable (π•œ E Fβ‚—) - - -/-- `ContinuousLinearMap.smulRight` as a continuous trilinear map: -`smulRightL (c : E β†’L[π•œ] π•œ) (f : F) (x : E) = c x β€’ f`. -/ -def smulRightL : (E β†’L[π•œ] π•œ) β†’L[π•œ] Fβ‚— β†’L[π•œ] E β†’L[π•œ] Fβ‚— := - LinearMap.mkContinuousβ‚‚ - { toFun := smulRightβ‚— - map_add' := fun c₁ cβ‚‚ => by - ext x - simp only [add_smul, coe_smulRightβ‚—, add_apply, smulRight_apply, LinearMap.add_apply] - map_smul' := fun m c => by - ext x - dsimp - rw [smul_smul] } - 1 fun c x => by - simp only [coe_smulRightβ‚—, one_mul, norm_smulRight_apply, LinearMap.coe_mk, AddHom.coe_mk, - le_refl] - -variable {π•œ E Fβ‚—} - -@[simp] -theorem norm_smulRightL_apply (c : E β†’L[π•œ] π•œ) (f : Fβ‚—) : β€–smulRightL π•œ E Fβ‚— c fβ€– = β€–cβ€– * β€–fβ€– := - norm_smulRight_apply c f - @[simp] theorem norm_smulRightL (c : E β†’L[π•œ] π•œ) [Nontrivial Fβ‚—] : β€–smulRightL π•œ E Fβ‚— cβ€– = β€–cβ€– := ContinuousLinearMap.homothety_norm _ c.norm_smulRight_apply