noncomputable def SpectralTheorem.rayleighInf {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) : ℝ

The infimum of the Rayleigh quotient of a continuous linear operator T over nonzero vectors. For self-adjoint T, this is the lower endpoint of spectrum ℝ T.

noncomputable def SpectralTheorem.rayleighSup {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) : ℝ

The supremum of the Rayleigh quotient of a continuous linear operator T over nonzero vectors. For self-adjoint T, this is the upper endpoint of spectrum ℝ T.

theorem SpectralTheorem.inner_shifted_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (t : ℝ) (x : H) : inner ℂ (((algebraMap ℝ (H →L[ℂ] H)) t - T) x) x = ↑(t * ‖x‖ ^ 2 - T.reApplyInnerSelf x)

For a self-adjoint operator T, ⟨(t·I − T)x, x⟩ equals the real number t‖x‖² − ⟨Tx,x⟩_ℝ cast into ℂ.

theorem SpectralTheorem.bddAbove_rayleigh {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) : BddAbove (Set.range fun (x : { x : H // x ≠ 0 }) => T.rayleighQuotient ↑x)

The Rayleigh quotient is bounded above by ‖T‖, so its range over nonzero vectors admits a supremum.

theorem SpectralTheorem.bddBelow_rayleigh {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) : BddBelow (Set.range fun (x : { x : H // x ≠ 0 }) => T.rayleighQuotient ↑x)

The Rayleigh quotient is bounded below by −‖T‖, so its range over nonzero vectors admits an infimum.

theorem SpectralTheorem.reApplyInnerSelf_le_rayleighSup_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) (x : H) : T.reApplyInnerSelf x ≤ rayleighSup T * ‖x‖ ^ 2

Pointwise bound: Re⟨Tx, x⟩ ≤ rayleighSup T · ‖x‖².

theorem SpectralTheorem.rayleighInf_mul_le_reApplyInnerSelf {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) (x : H) : rayleighInf T * ‖x‖ ^ 2 ≤ T.reApplyInnerSelf x

Pointwise bound: rayleighInf T · ‖x‖² ≤ Re⟨Tx, x⟩.

theorem SpectralTheorem.selfAdjoint_spectrum_subset_Icc {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) : spectrum ℝ T ⊆ Set.Icc (rayleighInf T) (rayleighSup T)

Spectral inclusion for self-adjoint operators: spectrum ℝ T ⊆ [rayleighInf T, rayleighSup T]. This is one direction of the Rayleigh quotient characterization of the spectrum (Melrose Prop 16.2).

theorem SpectralTheorem.discriminant_nonneg_aux {A B C : ℝ} (hC : 0 ≤ C) (hquad : ∀ (t : ℝ), 0 ≤ A + 2 * t * B + t ^ 2 * C) : B ^ 2 ≤ A * C

Discriminant bound for a quadratic in t: if A + 2tB + t²C ≥ 0 for all real t and C ≥ 0, then B² ≤ AC. Used in proving positivity-derived Cauchy-Schwarz inequalities.

theorem SpectralTheorem.quadratic_expansion_aux {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (P : H →L[ℂ] H) (hP : P.IsPositive) (x : H) (t : ℝ) : P.reApplyInnerSelf (x + ↑t • P x) = P.reApplyInnerSelf x + 2 * t * ‖P x‖ ^ 2 + t ^ 2 * P.reApplyInnerSelf (P x)

Quadratic expansion of ⟨P(x + tPx), x + tPx⟩ for positive P: expressed in t as a quadratic polynomial whose coefficients are Re⟨Px,x⟩, 2‖Px‖² and Re⟨P²x, Px⟩.

theorem SpectralTheorem.norm_sq_le_opNorm_mul_reApplyInnerSelf {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (P : H →L[ℂ] H) (hP : P.IsPositive) (x : H) : ‖P x‖ ^ 2 ≤ ‖P‖ * P.reApplyInnerSelf x

For a positive operator P, the Cauchy-Schwarz-type bound ‖Px‖² ≤ ‖P‖ · Re⟨Px, x⟩. This is the key inequality used to show that rayleighInf lies in the spectrum.

theorem SpectralTheorem.selfAdjoint_inf_mem_spectrum {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) : rayleighInf T ∈ spectrum ℝ T

The infimum of the Rayleigh quotient of a self-adjoint operator on a nontrivial complex Hilbert space belongs to its real spectrum (Melrose Prop 16.2 / 16.3).

theorem SpectralTheorem.rayleighInf_neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) : rayleighInf (-T) = -rayleighSup T

Negation symmetry: rayleighInf (-T) = -rayleighSup T.

theorem SpectralTheorem.selfAdjoint_sup_mem_spectrum {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) : rayleighSup T ∈ spectrum ℝ T

The supremum of the Rayleigh quotient of a self-adjoint operator on a nontrivial complex Hilbert space belongs to its real spectrum, obtained from the infimum statement via negation.

theorem SpectralTheorem.selfAdjoint_spectrum_Icc_characterization {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) : {rayleighInf T, rayleighSup T} ⊆ spectrum ℝ T ∧ spectrum ℝ T ⊆ Set.Icc (rayleighInf T) (rayleighSup T)

Full Rayleigh quotient characterization (Melrose Prop 16.1–16.3): for a self-adjoint operator T on a nontrivial complex Hilbert space, both rayleighInf T and rayleighSup T lie in spectrum ℝ T, and spectrum ℝ T is contained in [rayleighInf T, rayleighSup T].