English
A self-adjoint element a satisfies SpectrumRestricts a ContinuousMap.realToNNReal iff the NNReal-norm inequality holds.
Русский
Самосопряженный элемент a удовлетворяет SpectrumRestricts a RealToNNReal тогда и только тогда, когда выполняется неотрицательное неравенство по NNReal-норме.
LaTeX
$$SpectrumRestricts a ContinuousMap.realToNNReal \\leftrightarrow ‖algebraMap ℝ A t - a‖₊ ≤ t$$
Lean4
theorem nnreal_iff_nnnorm {a : A} {t : ℝ≥0} (ha : IsSelfAdjoint a) (ht : ‖a‖₊ ≤ t) :
SpectrumRestricts a ContinuousMap.realToNNReal ↔ ‖algebraMap ℝ A t - a‖₊ ≤ t :=
by
have : IsSelfAdjoint (algebraMap ℝ A t - a) := IsSelfAdjoint.algebraMap A (.all (t : ℝ)) |>.sub ha
rw [← ENNReal.coe_le_coe, ← IsSelfAdjoint.spectralRadius_eq_nnnorm, ←
SpectrumRestricts.spectralRadius_eq (f := Complex.reCLM)] at ht ⊢
· exact SpectrumRestricts.nnreal_iff_spectralRadius_le ht
all_goals
try apply IsSelfAdjoint.spectrumRestricts
assumption
