English
For a ≥ 0, the range of cfc with R = ℝ≥0 equals the set of x in the elemental part with x ≥ 0.
Русский
Для a ≥ 0 диапазон cfc с R = ℝ≥0 совпадает с множеством тех x, которые лежат в элементарной части и удовлетворяют x ≥ 0.
LaTeX
$$$\\mathrm{range}(\\mathrm{cfc}\\; a) = \\{x \\mid x \\in \\mathrm{elemental}\\; a \\wedge 0 \\le x\\}$$$
Lean4
theorem range_cfc_nnreal (a : A) (ha : 0 ≤ a) :
Set.range (cfc (R := ℝ≥0) · a) = {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x} :=
by
rw [range_cfc_nnreal_eq_image_cfc_real a ha, Set.setOf_and, SetLike.setOf_mem_eq, ← range_cfc _ ha.isSelfAdjoint,
Set.inter_comm, ← Set.image_preimage_eq_inter_range]
refine Set.Subset.antisymm (Set.image_mono (fun _ ↦ cfc_nonneg)) ?_
rintro _ ⟨f, hf, rfl⟩
simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq, Set.mem_image] at hf ⊢
obtain (⟨h₁, h₂⟩ | h | h) := by simpa only [not_and_or] using em (ContinuousOn f (spectrum ℝ a) ∧ IsSelfAdjoint a)
· refine ⟨f, ?_, rfl⟩
rwa [cfc_nonneg_iff f a] at hf
· exact ⟨0, by simp, by simp [cfc_apply_of_not_continuousOn a h]⟩
· exact ⟨0, by simp, by simp [cfc_apply_of_not_predicate a h]⟩
