nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts

English

The map cfcHom equals the real-restricted version of the spectrum-restrictive calculus on a self-adjoint element.

Русский

Отображение cfcHom равно ограниченной по реалу версии функционального калькулятора спектрального типа на самосопряженном элементе.

LaTeX

$$$$ cfcHom ha = \\text{SpectrumRestricts}_{\\mathbb{R}}(cfcHom ha) $$$$

Lean4

theorem nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts {a : A} :
    0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ContinuousMap.realToNNReal :=
  by
  refine ⟨fun ha ↦ ⟨.of_nonneg ha, .nnreal_of_nonneg ha⟩, ?_⟩
  rintro ⟨ha₁, ha₂⟩
  obtain ⟨x, hx, -, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts ha₁ ha₂
  simpa [sq, hx.star_eq] using star_mul_self_nonneg x

Похожие утверждения