Skip to content

Commit

Permalink
chore(Analysis/InnerProductSpace): weaken assumptions to `SeminormedA…
Browse files Browse the repository at this point in the history 
…ddCommGroup` (#17007)

replace the assumption `NormedAddCommGroup` to `SemiNormedAddCommGroup` in various places.

motivation: with the weakened assumption the results apply to `InnerProductSpace` without `definite` assumption.

This is suggested in #16707, and continues from #14024.



Co-authored-by: Eric Wieser <[email protected]>
  • Loading branch information
@yoh-tanimoto @eric-wieser
yoh-tanimoto and eric-wieser committed Sep 25, 2024
1 parent 15dec28 commit 691fdda
Show file tree
Hide file tree
Showing 3 changed files with 140 additions and 128 deletions.
196 changes: 94 additions & 102 deletions Mathlib/Analysis/InnerProductSpace/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1003,27 +1003,12 @@ theorem coe_basisOfOrthonormalOfCardEqFinrank [Fintype ι] [Nonempty ι] {v : ι
(basisOfOrthonormalOfCardEqFinrank hv card_eq : ι → E) = v :=
coe_basisOfLinearIndependentOfCardEqFinrank _ _

end OrthonormalSets_Seminormed

section OrthonormalSets

variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
variable {ι : Type*}

local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y

local notation "IK" => @RCLike.I 𝕜 _

local postfix:90 "†" => starRingEnd _

theorem Orthonormal.ne_zero {v : ι → E} (hv : Orthonormal 𝕜 v) (i : ι) : v i ≠ 0 := by
have : ‖v i‖ ≠ 0 := by
rw [hv.1 i]
norm_num
simpa using this
refine ne_of_apply_ne norm ?_
rw [hv.1 i, norm_zero]
norm_num

end OrthonormalSets
end OrthonormalSets_Seminormed

section Norm_Seminormed

Expand Down Expand Up @@ -1198,9 +1183,9 @@ instance (priority := 100) InnerProductSpace.toUniformConvexSpace : UniformConve
ring_nf
exact sub_le_sub_left (pow_le_pow_left hε.le hxy _) 4⟩

section Complex
section Complex_Seminormed

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V]
variable {V : Type*} [SeminormedAddCommGroup V] [InnerProductSpace ℂ V]

/-- A complex polarization identity, with a linear map
-/
Expand All @@ -1226,6 +1211,12 @@ theorem inner_map_polarization' (T : V →ₗ[ℂ] V) (x y : V) :
mul_add, ← mul_assoc, mul_neg, neg_neg, sub_neg_eq_add, one_mul, neg_one_mul, mul_sub, sub_sub]
ring

end Complex_Seminormed

section Complex

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V]

/-- A linear map `T` is zero, if and only if the identity `⟪T x, x⟫_ℂ = 0` holds for all `x`.
-/
theorem inner_map_self_eq_zero (T : V →ₗ[ℂ] V) : (∀ x : V, ⟪T x, x⟫_ℂ = 0) ↔ T = 0 := by
Expand Down Expand Up @@ -1551,7 +1542,7 @@ variable {𝕜}

namespace ContinuousLinearMap

variable {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E']
variable {E' : Type*} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E']

-- Note: odd and expensive build behavior is explicitly turned off using `noncomputable`
/-- Given `f : E →L[𝕜] E'`, construct the continuous sesquilinear form `fun x y ↦ ⟪x, A y⟫`, given
Expand All @@ -1576,6 +1567,83 @@ theorem toSesqForm_apply_norm_le {f : E →L[𝕜] E'} {v : E'} : ‖toSesqForm

end ContinuousLinearMap

section

variable {ι : Type*} {ι' : Type*} {ι'' : Type*}
variable {E' : Type*} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E']
variable {E'' : Type*} [SeminormedAddCommGroup E''] [InnerProductSpace 𝕜 E'']

@[simp]
theorem Orthonormal.equiv_refl {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) :
hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E :=
v.ext_linearIsometryEquiv fun i => by
simp only [Orthonormal.equiv_apply, Equiv.coe_refl, id, LinearIsometryEquiv.coe_refl]

@[simp]
theorem Orthonormal.equiv_symm {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'}
(hv' : Orthonormal 𝕜 v') (e : ι ≃ ι') : (hv.equiv hv' e).symm = hv'.equiv hv e.symm :=
v'.ext_linearIsometryEquiv fun i =>
(hv.equiv hv' e).injective <| by
simp only [LinearIsometryEquiv.apply_symm_apply, Orthonormal.equiv_apply, e.apply_symm_apply]

end

variable (𝕜)

/-- `innerSL` is an isometry. Note that the associated `LinearIsometry` is defined in
`InnerProductSpace.Dual` as `toDualMap`. -/
@[simp]
theorem innerSL_apply_norm (x : E) : ‖innerSL 𝕜 x‖ = ‖x‖ := by
refine
le_antisymm ((innerSL 𝕜 x).opNorm_le_bound (norm_nonneg _) fun y => norm_inner_le_norm _ _) ?_
rcases (norm_nonneg x).eq_or_gt with (h | h)
· simp [h]
· refine (mul_le_mul_right h).mp ?_
calc
‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ := by
rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
_ ≤ ‖innerSL 𝕜 x‖ * ‖x‖ := (innerSL 𝕜 x).le_opNorm _

lemma norm_innerSL_le : ‖innerSL 𝕜 (E := E)‖ ≤ 1 :=
ContinuousLinearMap.opNorm_le_bound _ zero_le_one (by simp)

variable {𝕜}

/-- When an inner product space `E` over `𝕜` is considered as a real normed space, its inner
product satisfies `IsBoundedBilinearMap`.
In order to state these results, we need a `NormedSpace ℝ E` instance. We will later establish
such an instance by restriction-of-scalars, `InnerProductSpace.rclikeToReal 𝕜 E`, but this
instance may be not definitionally equal to some other “natural” instance. So, we assume
`[NormedSpace ℝ E]`.
-/
theorem _root_.isBoundedBilinearMap_inner [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] :
IsBoundedBilinearMap ℝ fun p : E × E => ⟪p.1, p.2⟫ :=
{ add_left := inner_add_left
smul_left := fun r x y => by
simp only [← algebraMap_smul 𝕜 r x, algebraMap_eq_ofReal, inner_smul_real_left]
add_right := inner_add_right
smul_right := fun r x y => by
simp only [← algebraMap_smul 𝕜 r y, algebraMap_eq_ofReal, inner_smul_real_right]
bound :=
⟨1, zero_lt_one, fun x y => by
rw [one_mul]
exact norm_inner_le_norm x y⟩ }

/-- The inner product of two weighted sums, where the weights in each
sum add to 0, in terms of the norms of pairwise differences. -/
theorem inner_sum_smul_sum_smul_of_sum_eq_zero {ι₁ : Type*} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ}
(v₁ : ι₁ → F) (h₁ : ∑ i ∈ s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ}
(v₂ : ι₂ → F) (h₂ : ∑ i ∈ s₂, w₂ i = 0) :
⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
(-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2 := by
simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same,
← div_add_div_same, mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib,
Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul, h₁, h₂, zero_mul,
mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
Finset.sum_div, mul_div_assoc, mul_assoc]

end Norm_Seminormed

section Norm
Expand Down Expand Up @@ -1611,27 +1679,6 @@ theorem dist_div_norm_sq_smul {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) (R : ℝ)
_ = R ^ 2 / (‖x‖ * ‖y‖) * dist x y := by
rw [sqrt_mul, sqrt_sq, sqrt_sq, dist_eq_norm] <;> positivity

section

variable {ι : Type*} {ι' : Type*} {ι'' : Type*}
variable {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E']
variable {E'' : Type*} [NormedAddCommGroup E''] [InnerProductSpace 𝕜 E'']

@[simp]
theorem Orthonormal.equiv_refl {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) :
hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E :=
v.ext_linearIsometryEquiv fun i => by
simp only [Orthonormal.equiv_apply, Equiv.coe_refl, id, LinearIsometryEquiv.coe_refl]

@[simp]
theorem Orthonormal.equiv_symm {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'}
(hv' : Orthonormal 𝕜 v') (e : ι ≃ ι') : (hv.equiv hv' e).symm = hv'.equiv hv e.symm :=
v'.ext_linearIsometryEquiv fun i =>
(hv.equiv hv' e).injective <| by
simp only [LinearIsometryEquiv.apply_symm_apply, Orthonormal.equiv_apply, e.apply_symm_apply]

end

/-- The inner product of a nonzero vector with a nonzero multiple of
itself, divided by the product of their norms, has absolute value
1. -/
Expand Down Expand Up @@ -1804,62 +1851,6 @@ theorem eq_of_norm_le_re_inner_eq_norm_sq {x y : E} (hle : ‖x‖ ≤ ‖y‖)
have H₂ : re ⟪y, x⟫ = ‖y‖ ^ 2 := by rwa [← inner_conj_symm, conj_re]
simpa [inner_sub_left, inner_sub_right, ← norm_sq_eq_inner, h, H₂] using H₁

/-- The inner product of two weighted sums, where the weights in each
sum add to 0, in terms of the norms of pairwise differences. -/
theorem inner_sum_smul_sum_smul_of_sum_eq_zero {ι₁ : Type*} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ}
(v₁ : ι₁ → F) (h₁ : ∑ i ∈ s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ}
(v₂ : ι₂ → F) (h₂ : ∑ i ∈ s₂, w₂ i = 0) :
⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
(-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2 := by
simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same,
← div_add_div_same, mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib,
Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul, h₁, h₂, zero_mul,
mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
Finset.sum_div, mul_div_assoc, mul_assoc]

variable (𝕜)

/-- `innerSL` is an isometry. Note that the associated `LinearIsometry` is defined in
`InnerProductSpace.Dual` as `toDualMap`. -/
@[simp]
theorem innerSL_apply_norm (x : E) : ‖innerSL 𝕜 x‖ = ‖x‖ := by
refine
le_antisymm ((innerSL 𝕜 x).opNorm_le_bound (norm_nonneg _) fun y => norm_inner_le_norm _ _) ?_
rcases eq_or_ne x 0 with (rfl | h)
· simp
· refine (mul_le_mul_right (norm_pos_iff.2 h)).mp ?_
calc
‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ := by
rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
_ ≤ ‖innerSL 𝕜 x‖ * ‖x‖ := (innerSL 𝕜 x).le_opNorm _

lemma norm_innerSL_le : ‖innerSL 𝕜 (E := E)‖ ≤ 1 :=
ContinuousLinearMap.opNorm_le_bound _ zero_le_one (by simp)

variable {𝕜}

/-- When an inner product space `E` over `𝕜` is considered as a real normed space, its inner
product satisfies `IsBoundedBilinearMap`.
In order to state these results, we need a `NormedSpace ℝ E` instance. We will later establish
such an instance by restriction-of-scalars, `InnerProductSpace.rclikeToReal 𝕜 E`, but this
instance may be not definitionally equal to some other “natural” instance. So, we assume
`[NormedSpace ℝ E]`.
-/
theorem _root_.isBoundedBilinearMap_inner [NormedSpace ℝ E] :
IsBoundedBilinearMap ℝ fun p : E × E => ⟪p.1, p.2⟫ :=
{ add_left := inner_add_left
smul_left := fun r x y => by
simp only [← algebraMap_smul 𝕜 r x, algebraMap_eq_ofReal, inner_smul_real_left]
add_right := inner_add_right
smul_right := fun r x y => by
simp only [← algebraMap_smul 𝕜 r y, algebraMap_eq_ofReal, inner_smul_real_right]
bound :=
⟨1, zero_lt_one, fun x y => by
rw [one_mul]
exact norm_inner_le_norm x y⟩ }

end Norm

section BesselsInequality
Expand Down Expand Up @@ -2268,7 +2259,7 @@ end RCLikeToReal

section Continuous

variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
variable [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]

local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y

Expand All @@ -2283,6 +2274,7 @@ local postfix:90 "†" => starRingEnd _

theorem continuous_inner : Continuous fun p : E × E => ⟪p.1, p.2⟫ :=
letI : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
letI : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower _ _ _
isBoundedBilinearMap_inner.continuous

variable {α : Type*}
Expand Down Expand Up @@ -2333,7 +2325,7 @@ end ReApplyInnerSelf

section ReApplyInnerSelf_Seminormed

variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
variable [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]

local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y

Expand All @@ -2355,7 +2347,7 @@ end ReApplyInnerSelf_Seminormed

section UniformSpace.Completion

variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
variable [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]

local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y

Expand Down
70 changes: 45 additions & 25 deletions Mathlib/Analysis/InnerProductSpace/Symmetric.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,11 +36,13 @@ open RCLike

open ComplexConjugate

section Seminormed

variable {𝕜 E E' F G : Type*} [RCLike 𝕜]
variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
variable [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
variable [NormedAddCommGroup G] [InnerProductSpace 𝕜 G]
variable [NormedAddCommGroup E'] [InnerProductSpace ℝ E']
variable [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]
variable [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F]
variable [SeminormedAddCommGroup G] [InnerProductSpace 𝕜 G]
variable [SeminormedAddCommGroup E'] [InnerProductSpace ℝ E']

local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y

Expand Down Expand Up @@ -83,23 +85,6 @@ theorem IsSymmetric.add {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.Is
rw [LinearMap.add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right]
rfl

/-- The **Hellinger--Toeplitz theorem**: if a symmetric operator is defined on a complete space,
then it is automatically continuous. -/
theorem IsSymmetric.continuous [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : IsSymmetric T) :
Continuous T := by
-- We prove it by using the closed graph theorem
refine T.continuous_of_seq_closed_graph fun u x y hu hTu => ?_
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
have hlhs : ∀ k : ℕ, ⟪T (u k) - T x, y - T x⟫ = ⟪u k - x, T (y - T x)⟫ := by
intro k
rw [← T.map_sub, hT]
refine tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) ?_
simp_rw [Function.comp_apply, hlhs]
rw [← inner_zero_left (T (y - T x))]
refine Filter.Tendsto.inner ?_ tendsto_const_nhds
rw [← sub_self x]
exact hu.sub_const _

/-- For a symmetric operator `T`, the function `fun x ↦ ⟪T x, x⟫` is real-valued. -/
@[simp]
theorem IsSymmetric.coe_reApplyInnerSelf_apply {T : E →L[𝕜] E} (hT : IsSymmetric (T : E →ₗ[𝕜] E))
Expand All @@ -115,14 +100,14 @@ theorem IsSymmetric.restrict_invariant {T : E →ₗ[𝕜] E} (hT : IsSymmetric
(hV : ∀ v ∈ V, T v ∈ V) : IsSymmetric (T.restrict hV) := fun v w => hT v w

theorem IsSymmetric.restrictScalars {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
@LinearMap.IsSymmetric ℝ E _ _ (InnerProductSpace.rclikeToReal 𝕜 E)
(@LinearMap.restrictScalars ℝ 𝕜 _ _ _ _ _ _ (InnerProductSpace.rclikeToReal 𝕜 E).toModule
(InnerProductSpace.rclikeToReal 𝕜 E).toModule _ _ _ T) :=
letI := InnerProductSpace.rclikeToReal 𝕜 E
letI : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower _ _ _
(T.restrictScalars ℝ).IsSymmetric :=
fun x y => by simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]

section Complex

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V]
variable {V : Type*} [SeminormedAddCommGroup V] [InnerProductSpace ℂ V]

attribute [local simp] map_ofNat in -- use `ofNat` simp theorem with bad keys
open scoped InnerProductSpace in
Expand Down Expand Up @@ -167,6 +152,39 @@ theorem IsSymmetric.inner_map_polarization {T : E →ₗ[𝕜] E} (hT : T.IsSymm
sub_sub, ← mul_assoc, mul_neg, h, neg_neg, one_mul, neg_one_mul]
ring

end LinearMap

end Seminormed

section Normed

variable {𝕜 E E' F G : Type*} [RCLike 𝕜]
variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
variable [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
variable [NormedAddCommGroup G] [InnerProductSpace 𝕜 G]
variable [NormedAddCommGroup E'] [InnerProductSpace ℝ E']

local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y

namespace LinearMap

/-- The **Hellinger--Toeplitz theorem**: if a symmetric operator is defined on a complete space,
then it is automatically continuous. -/
theorem IsSymmetric.continuous [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : IsSymmetric T) :
Continuous T := by
-- We prove it by using the closed graph theorem
refine T.continuous_of_seq_closed_graph fun u x y hu hTu => ?_
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
have hlhs : ∀ k : ℕ, ⟪T (u k) - T x, y - T x⟫ = ⟪u k - x, T (y - T x)⟫ := by
intro k
rw [← T.map_sub, hT]
refine tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) ?_
simp_rw [Function.comp_apply, hlhs]
rw [← inner_zero_left (T (y - T x))]
refine Filter.Tendsto.inner ?_ tendsto_const_nhds
rw [← sub_self x]
exact hu.sub_const _

/-- A symmetric linear map `T` is zero if and only if `⟪T x, x⟫_ℝ = 0` for all `x`.
See `inner_map_self_eq_zero` for the complex version without the symmetric assumption. -/
theorem IsSymmetric.inner_map_self_eq_zero {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
Expand All @@ -178,3 +196,5 @@ theorem IsSymmetric.inner_map_self_eq_zero {T : E →ₗ[𝕜] E} (hT : T.IsSymm
ring

end LinearMap

end Normed
2 changes: 1 addition & 1 deletion Mathlib/Analysis/Normed/Module/Completion.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ namespace UniformSpace

namespace Completion

variable (𝕜 E : Type*) [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable (𝕜 E : Type*) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

instance (priority := 100) NormedSpace.to_uniformContinuousConstSMul :
UniformContinuousConstSMul 𝕜 E :=
Expand Down

0 comments on commit 691fdda

Please sign in to comment.