-
Notifications
You must be signed in to change notification settings - Fork 234
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: port Analysis.InnerProductSpace.Rayleigh (#4920)
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
- Loading branch information
Showing
2 changed files
with
296 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,295 @@ | ||
/- | ||
Copyright (c) 2021 Heather Macbeth. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Heather Macbeth, Frédéric Dupuis | ||
! This file was ported from Lean 3 source module analysis.inner_product_space.rayleigh | ||
! leanprover-community/mathlib commit 6b0169218d01f2837d79ea2784882009a0da1aa1 | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
import Mathlib.Analysis.InnerProductSpace.Calculus | ||
import Mathlib.Analysis.InnerProductSpace.Dual | ||
import Mathlib.Analysis.InnerProductSpace.Adjoint | ||
import Mathlib.Analysis.Calculus.LagrangeMultipliers | ||
import Mathlib.LinearAlgebra.Eigenspace.Basic | ||
|
||
/-! | ||
# The Rayleigh quotient | ||
The Rayleigh quotient of a self-adjoint operator `T` on an inner product space `E` is the function | ||
`λ x, ⟪T x, x⟫ / ‖x‖ ^ 2`. | ||
The main results of this file are `IsSelfAdjoint.hasEigenvector_of_isMaxOn` and | ||
`IsSelfAdjoint.hasEigenvector_of_isMinOn`, which state that if `E` is complete, and if the | ||
Rayleigh quotient attains its global maximum/minimum over some sphere at the point `x₀`, then `x₀` | ||
is an eigenvector of `T`, and the `iSup`/`iInf` of `λ x, ⟪T x, x⟫ / ‖x‖ ^ 2` is the corresponding | ||
eigenvalue. | ||
The corollaries `LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional` and | ||
`LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional` state that if `E` is | ||
finite-dimensional and nontrivial, then `T` has some (nonzero) eigenvectors with eigenvalue the | ||
`iSup`/`iInf` of `λ x, ⟪T x, x⟫ / ‖x‖ ^ 2`. | ||
## TODO | ||
A slightly more elaborate corollary is that if `E` is complete and `T` is a compact operator, then | ||
`T` has some (nonzero) eigenvector with eigenvalue either `⨆ x, ⟪T x, x⟫ / ‖x‖ ^ 2` or | ||
`⨅ x, ⟪T x, x⟫ / ‖x‖ ^ 2` (not necessarily both). | ||
-/ | ||
|
||
|
||
variable {𝕜 : Type _} [IsROrC 𝕜] | ||
|
||
variable {E : Type _} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] | ||
|
||
local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y | ||
|
||
open scoped NNReal | ||
|
||
open Module.End Metric | ||
|
||
namespace ContinuousLinearMap | ||
|
||
variable (T : E →L[𝕜] E) | ||
|
||
/-- The *Rayleigh quotient* of a continuous linear map `T` (over `ℝ` or `ℂ`) at a vector `x` is | ||
the quantity `re ⟪T x, x⟫ / ‖x‖ ^ 2`. -/ | ||
noncomputable abbrev rayleighQuotient (x : E) := T.reApplyInnerSelf x / ‖(x : E)‖ ^ 2 | ||
|
||
theorem rayleigh_smul (x : E) {c : 𝕜} (hc : c ≠ 0) : | ||
rayleighQuotient T (c • x) = rayleighQuotient T x := by | ||
by_cases hx : x = 0 | ||
· simp [hx] | ||
have : ‖c‖ ≠ 0 := by simp [hc] | ||
have : ‖x‖ ≠ 0 := by simp [hx] | ||
field_simp [norm_smul, T.reApplyInnerSelf_smul] | ||
ring | ||
#align continuous_linear_map.rayleigh_smul ContinuousLinearMap.rayleigh_smul | ||
|
||
theorem image_rayleigh_eq_image_rayleigh_sphere {r : ℝ} (hr : 0 < r) : | ||
rayleighQuotient T '' {0}ᶜ = rayleighQuotient T '' sphere 0 r := by | ||
ext a | ||
constructor | ||
· rintro ⟨x, hx : x ≠ 0, hxT⟩ | ||
have : ‖x‖ ≠ 0 := by simp [hx] | ||
let c : 𝕜 := ↑‖x‖⁻¹ * r | ||
have : c ≠ 0 := by simp [hx, hr.ne'] | ||
refine' ⟨c • x, _, _⟩ | ||
· field_simp [norm_smul, abs_of_pos hr] | ||
· rw [T.rayleigh_smul x this] | ||
exact hxT | ||
· rintro ⟨x, hx, hxT⟩ | ||
exact ⟨x, ne_zero_of_mem_sphere hr.ne' ⟨x, hx⟩, hxT⟩ | ||
#align continuous_linear_map.image_rayleigh_eq_image_rayleigh_sphere ContinuousLinearMap.image_rayleigh_eq_image_rayleigh_sphere | ||
|
||
theorem iSup_rayleigh_eq_iSup_rayleigh_sphere {r : ℝ} (hr : 0 < r) : | ||
(⨆ x : { x : E // x ≠ 0 }, rayleighQuotient T x) = | ||
⨆ x : sphere (0 : E) r, rayleighQuotient T x := | ||
show (⨆ x : ({0}ᶜ : Set E), rayleighQuotient T x) = _ by | ||
simp only [← @sSup_image' _ _ _ _ (rayleighQuotient T), | ||
T.image_rayleigh_eq_image_rayleigh_sphere hr] | ||
#align continuous_linear_map.supr_rayleigh_eq_supr_rayleigh_sphere ContinuousLinearMap.iSup_rayleigh_eq_iSup_rayleigh_sphere | ||
|
||
theorem iInf_rayleigh_eq_iInf_rayleigh_sphere {r : ℝ} (hr : 0 < r) : | ||
(⨅ x : { x : E // x ≠ 0 }, rayleighQuotient T x) = | ||
⨅ x : sphere (0 : E) r, rayleighQuotient T x := | ||
show (⨅ x : ({0}ᶜ : Set E), rayleighQuotient T x) = _ by | ||
simp only [← @sInf_image' _ _ _ _ (rayleighQuotient T), | ||
T.image_rayleigh_eq_image_rayleigh_sphere hr] | ||
#align continuous_linear_map.infi_rayleigh_eq_infi_rayleigh_sphere ContinuousLinearMap.iInf_rayleigh_eq_iInf_rayleigh_sphere | ||
|
||
end ContinuousLinearMap | ||
|
||
namespace IsSelfAdjoint | ||
|
||
section Real | ||
|
||
variable {F : Type _} [NormedAddCommGroup F] [InnerProductSpace ℝ F] | ||
|
||
theorem _root_.LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf {T : F →L[ℝ] F} | ||
(hT : (T : F →ₗ[ℝ] F).IsSymmetric) (x₀ : F) : | ||
HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ (T x₀))) x₀ := by | ||
convert T.hasStrictFDerivAt.inner ℝ (hasStrictFDerivAt_id x₀) using 1 | ||
ext y | ||
rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerClm_apply, | ||
ContinuousLinearMap.prod_apply, innerSL_apply, id.def, ContinuousLinearMap.id_apply, | ||
hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul] | ||
#align linear_map.is_symmetric.has_strict_fderiv_at_re_apply_inner_self LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf | ||
|
||
variable [CompleteSpace F] {T : F →L[ℝ] F} | ||
|
||
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) | ||
|
||
theorem linearly_dependent_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : F} | ||
(hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : F) ‖x₀‖) x₀) : | ||
∃ a b : ℝ, (a, b) ≠ 0 ∧ a • x₀ + b • T x₀ = 0 := by | ||
have H : IsLocalExtrOn T.reApplyInnerSelf {x : F | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀ := by | ||
convert hextr | ||
ext x | ||
simp [dist_eq_norm] | ||
-- find Lagrange multipliers for the function `T.re_apply_inner_self` and the | ||
-- hypersurface-defining function `λ x, ‖x‖ ^ 2` | ||
obtain ⟨a, b, h₁, h₂⟩ := | ||
IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d H (hasStrictFDerivAt_norm_sq x₀) | ||
(hT.isSymmetric.hasStrictFDerivAt_reApplyInnerSelf x₀) | ||
refine' ⟨a, b, h₁, _⟩ | ||
apply (InnerProductSpace.toDualMap ℝ F).injective | ||
simp only [LinearIsometry.map_add, LinearIsometry.map_smul, LinearIsometry.map_zero] | ||
simp only [map_smulₛₗ, IsROrC.conj_to_real] | ||
change a • innerSL ℝ x₀ + b • innerSL ℝ (T x₀) = 0 | ||
apply smul_right_injective (F →L[ℝ] ℝ) (two_ne_zero : (2 : ℝ) ≠ 0) | ||
simpa only [two_smul, smul_add, add_smul, add_zero] using h₂ | ||
#align is_self_adjoint.linearly_dependent_of_is_local_extr_on IsSelfAdjoint.linearly_dependent_of_isLocalExtrOn | ||
|
||
theorem eq_smul_self_of_isLocalExtrOn_real (hT : IsSelfAdjoint T) {x₀ : F} | ||
(hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : F) ‖x₀‖) x₀) : | ||
T x₀ = T.rayleighQuotient x₀ • x₀ := by | ||
obtain ⟨a, b, h₁, h₂⟩ := hT.linearly_dependent_of_isLocalExtrOn hextr | ||
by_cases hx₀ : x₀ = 0 | ||
· simp [hx₀] | ||
by_cases hb : b = 0 | ||
· have : a ≠ 0 := by simpa [hb] using h₁ | ||
refine' absurd _ hx₀ | ||
apply smul_right_injective F this | ||
simpa [hb] using h₂ | ||
let c : ℝ := -b⁻¹ * a | ||
have hc : T x₀ = c • x₀ := by | ||
have : b * (b⁻¹ * a) = a := by field_simp [mul_comm] | ||
apply smul_right_injective F hb | ||
simp [eq_neg_of_add_eq_zero_left h₂, ← mul_smul, this] | ||
convert hc | ||
have : ‖x₀‖ ≠ 0 := by simp [hx₀] | ||
have := congr_arg (fun x => ⟪x, x₀⟫_ℝ) hc | ||
field_simp [inner_smul_left, real_inner_self_eq_norm_mul_norm, sq] at this ⊢ | ||
exact this | ||
#align is_self_adjoint.eq_smul_self_of_is_local_extr_on_real IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn_real | ||
|
||
end Real | ||
|
||
section CompleteSpace | ||
|
||
variable [CompleteSpace E] {T : E →L[𝕜] E} | ||
|
||
theorem eq_smul_self_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : E} | ||
(hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) : | ||
T x₀ = (↑(T.rayleighQuotient x₀) : 𝕜) • x₀ := by | ||
letI := InnerProductSpace.isROrCToReal 𝕜 E | ||
let hSA := hT.isSymmetric.restrictScalars.toSelfAdjoint.prop | ||
exact hSA.eq_smul_self_of_isLocalExtrOn_real hextr | ||
#align is_self_adjoint.eq_smul_self_of_is_local_extr_on IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn | ||
|
||
/-- For a self-adjoint operator `T`, a local extremum of the Rayleigh quotient of `T` on a sphere | ||
centred at the origin is an eigenvector of `T`. -/ | ||
theorem hasEigenvector_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0) | ||
(hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) : | ||
HasEigenvector (T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀)) x₀ := by | ||
refine' ⟨_, hx₀⟩ | ||
rw [Module.End.mem_eigenspace_iff] | ||
exact hT.eq_smul_self_of_isLocalExtrOn hextr | ||
#align is_self_adjoint.has_eigenvector_of_is_local_extr_on IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn | ||
|
||
/-- For a self-adjoint operator `T`, a maximum of the Rayleigh quotient of `T` on a sphere centred | ||
at the origin is an eigenvector of `T`, with eigenvalue the global supremum of the Rayleigh | ||
quotient. -/ | ||
theorem hasEigenvector_of_isMaxOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0) | ||
(hextr : IsMaxOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) : | ||
HasEigenvector (T : E →ₗ[𝕜] E) (↑(⨆ x : { x : E // x ≠ 0 }, T.rayleighQuotient x)) x₀ := by | ||
convert hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inr hextr.localize) | ||
have hx₀' : 0 < ‖x₀‖ := by simp [hx₀] | ||
have hx₀'' : x₀ ∈ sphere (0 : E) ‖x₀‖ := by simp | ||
rw [T.iSup_rayleigh_eq_iSup_rayleigh_sphere hx₀'] | ||
refine' IsMaxOn.iSup_eq hx₀'' _ | ||
intro x hx | ||
dsimp | ||
have : ‖x‖ = ‖x₀‖ := by simpa using hx | ||
simp only [ContinuousLinearMap.rayleighQuotient] | ||
rw [this] | ||
gcongr | ||
exact hextr hx | ||
#align is_self_adjoint.has_eigenvector_of_is_max_on IsSelfAdjoint.hasEigenvector_of_isMaxOn | ||
|
||
/-- For a self-adjoint operator `T`, a minimum of the Rayleigh quotient of `T` on a sphere centred | ||
at the origin is an eigenvector of `T`, with eigenvalue the global infimum of the Rayleigh | ||
quotient. -/ | ||
theorem hasEigenvector_of_isMinOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0) | ||
(hextr : IsMinOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) : | ||
HasEigenvector (T : E →ₗ[𝕜] E) (↑(⨅ x : { x : E // x ≠ 0 }, T.rayleighQuotient x)) x₀ := by | ||
convert hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inl hextr.localize) | ||
have hx₀' : 0 < ‖x₀‖ := by simp [hx₀] | ||
have hx₀'' : x₀ ∈ sphere (0 : E) ‖x₀‖ := by simp | ||
rw [T.iInf_rayleigh_eq_iInf_rayleigh_sphere hx₀'] | ||
refine' IsMinOn.iInf_eq hx₀'' _ | ||
intro x hx | ||
dsimp | ||
have : ‖x‖ = ‖x₀‖ := by simpa using hx | ||
simp only [ContinuousLinearMap.rayleighQuotient] | ||
rw [this] | ||
gcongr | ||
exact hextr hx | ||
#align is_self_adjoint.has_eigenvector_of_is_min_on IsSelfAdjoint.hasEigenvector_of_isMinOn | ||
|
||
end CompleteSpace | ||
|
||
end IsSelfAdjoint | ||
|
||
section FiniteDimensional | ||
|
||
variable [FiniteDimensional 𝕜 E] [_i : Nontrivial E] {T : E →ₗ[𝕜] E} | ||
|
||
namespace LinearMap | ||
|
||
namespace IsSymmetric | ||
|
||
/-- The supremum of the Rayleigh quotient of a symmetric operator `T` on a nontrivial | ||
finite-dimensional vector space is an eigenvalue for that operator. -/ | ||
theorem hasEigenvalue_iSup_of_finiteDimensional (hT : T.IsSymmetric) : | ||
HasEigenvalue T ↑(⨆ x : { x : E // x ≠ 0 }, IsROrC.re ⟪T x, x⟫ / ‖(x : E)‖ ^ 2) := by | ||
haveI := FiniteDimensional.proper_isROrC 𝕜 E | ||
let T' := hT.toSelfAdjoint | ||
obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0 | ||
have H₁ : IsCompact (sphere (0 : E) ‖x‖) := isCompact_sphere _ _ | ||
have H₂ : (sphere (0 : E) ‖x‖).Nonempty := ⟨x, by simp⟩ | ||
-- key point: in finite dimension, a continuous function on the sphere has a max | ||
obtain ⟨x₀, hx₀', hTx₀⟩ := | ||
H₁.exists_forall_ge H₂ T'.val.reApplyInnerSelf_continuous.continuousOn | ||
have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀' | ||
have : IsMaxOn T'.val.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀ := by simpa only [← hx₀] using hTx₀ | ||
have hx₀_ne : x₀ ≠ 0 := by | ||
have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne.def, not_false_iff] | ||
simpa [← norm_eq_zero, Ne.def] | ||
exact hasEigenvalue_of_hasEigenvector (T'.prop.hasEigenvector_of_isMaxOn hx₀_ne this) | ||
#align linear_map.is_symmetric.has_eigenvalue_supr_of_finite_dimensional LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional | ||
|
||
/-- The infimum of the Rayleigh quotient of a symmetric operator `T` on a nontrivial | ||
finite-dimensional vector space is an eigenvalue for that operator. -/ | ||
theorem hasEigenvalue_iInf_of_finiteDimensional (hT : T.IsSymmetric) : | ||
HasEigenvalue T ↑(⨅ x : { x : E // x ≠ 0 }, IsROrC.re ⟪T x, x⟫ / ‖(x : E)‖ ^ 2) := by | ||
haveI := FiniteDimensional.proper_isROrC 𝕜 E | ||
let T' := hT.toSelfAdjoint | ||
obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0 | ||
have H₁ : IsCompact (sphere (0 : E) ‖x‖) := isCompact_sphere _ _ | ||
have H₂ : (sphere (0 : E) ‖x‖).Nonempty := ⟨x, by simp⟩ | ||
-- key point: in finite dimension, a continuous function on the sphere has a min | ||
obtain ⟨x₀, hx₀', hTx₀⟩ := | ||
H₁.exists_forall_le H₂ T'.val.reApplyInnerSelf_continuous.continuousOn | ||
have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀' | ||
have : IsMinOn T'.val.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀ := by simpa only [← hx₀] using hTx₀ | ||
have hx₀_ne : x₀ ≠ 0 := by | ||
have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne.def, not_false_iff] | ||
simpa [← norm_eq_zero, Ne.def] | ||
exact hasEigenvalue_of_hasEigenvector (T'.prop.hasEigenvector_of_isMinOn hx₀_ne this) | ||
#align linear_map.is_symmetric.has_eigenvalue_infi_of_finite_dimensional LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional | ||
|
||
theorem subsingleton_of_no_eigenvalue_finiteDimensional (hT : T.IsSymmetric) | ||
(hT' : ∀ μ : 𝕜, Module.End.eigenspace (T : E →ₗ[𝕜] E) μ = ⊥) : Subsingleton E := | ||
(subsingleton_or_nontrivial E).resolve_right fun _h => | ||
absurd (hT' _) hT.hasEigenvalue_iSup_of_finiteDimensional | ||
#align linear_map.is_symmetric.subsingleton_of_no_eigenvalue_finite_dimensional LinearMap.IsSymmetric.subsingleton_of_no_eigenvalue_finiteDimensional | ||
|
||
end IsSymmetric | ||
|
||
end LinearMap | ||
|
||
end FiniteDimensional |