English
Given a self-adjoint a with quasispectrum restriction, there exists a self-adjoint x such that x^2 = a and quasispectrum(x) restricted appropriately.
Русский
Существует самосопряжённый корень x such that x^2 = a и спектр x удовлетворяет требованию ограниченности.
LaTeX
$$$$ \\exists x \\; (IsSelfAdjoint x) \\land\\; QuasispectrumRestricts x RealToNNReal \\land x^2 = a $$$$
Lean4
theorem exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts {A : Type*} [NonUnitalRing A] [StarRing A]
[TopologicalSpace A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A]
[NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A} (ha₁ : IsSelfAdjoint a)
(ha₂ : QuasispectrumRestricts a ContinuousMap.realToNNReal) :
∃ x : A, IsSelfAdjoint x ∧ QuasispectrumRestricts x ContinuousMap.realToNNReal ∧ x * x = a :=
by
use cfcₙ (√·) a, cfcₙ_predicate (√·) a
constructor
·
simpa only [QuasispectrumRestricts.nnreal_iff, cfcₙ_map_quasispectrum (√·) a, Set.mem_image, forall_exists_index,
and_imp, forall_apply_eq_imp_iff₂] using fun x _ ↦ Real.sqrt_nonneg x
· rw [← cfcₙ_mul ..]
nth_rw 2 [← cfcₙ_id ℝ a]
apply cfcₙ_congr fun x hx ↦ ?_
rw [QuasispectrumRestricts.nnreal_iff] at ha₂
apply ha₂ x at hx
simp [← sq, Real.sq_sqrt hx]
