[Nontrivial F] (T : F →L[ℂ] F) (hT : IsSelfAdjoint T) : sInf (spectrum ℝ T) = rayleighInf T

Initializing...

[Nontrivial F] (T : F →L[ℂ] F) (hT : IsSelfAdjoint T) : sInf (spectrum ℝ T) = rayleighInf T · Prove2Me