English
Under the same hypotheses, the calculus commutes with the involution (star): cfc_n (x ↦ star(f(x))) a = star (cfc_n f a).
Русский
С тем же допущением функциональный калькулятор сохраняет звёздоператор (инволюцию):
LaTeX
$$$$ cfc\\!_n(\\,x\\mapsto \\ star(f(x))\\,)\\,a \\\\ = \\\\ star\\ Bigl( cfc\\!_n f\\,a \\Bigr) $$$$
Lean4
theorem cfcₙ_star : cfcₙ (fun x ↦ star (f x)) a = star (cfcₙ f a) :=
by
by_cases h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
· obtain ⟨ha, hf, h0⟩ := h
rw [cfcₙ_apply f a, ← map_star, cfcₙ_apply _ a]
congr
· simp only [not_and_or] at h
obtain (ha | hf | h0) := h
· simp [cfcₙ_apply_of_not_predicate a ha]
· rw [cfcₙ_apply_of_not_continuousOn a hf, cfcₙ_apply_of_not_continuousOn, star_zero]
exact fun hf_star ↦ hf <| by simpa using hf_star.star
· rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, star_zero]
exact fun hf0 ↦ h0 <| by simpa using congr(star $(hf0))
