DihedralContinuousMoments.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform polynomial approximation transfers the dihedral polynomial moments to the continuous functional calculus of the real rotation.

theorem OAI.KadisonSimilarity.exists_polynomial_near_cfc line 18

Source documentation

Polynomial approximation on the exact interval used for a selfadjoint contraction, in the source algebra norm.

theorem exists_polynomial_near_cfc (a : A) (ha : IsSelfAdjoint a) (han : ‖a‖ ≤ 1)
    (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc (-1) 1))
    {ε : ℝ} (hε : 0 < ε) :
    ∃ p : Polynomial ℝ, ‖cfc f a - Polynomial.aeval a p‖ ≤ ε ∧
      ∀ x ∈ Set.Icc (-1) 1, |p.eval x - f x| < ε := by
…

theorem OAI.KadisonSimilarity.trace_cfc_realPart_rotation_reflection line 41

Source documentation

The zero reflection-coset functional extends from polynomials to every continuous function of the real part.

theorem trace_cfc_realPart_rotation_reflection (τ : A →L[ℂ] ℂ) (w : Aˣ) (d : A)
    (hw : star (w : A) = (↑w⁻¹ : A)) (hwn : ‖(w : A)‖ ≤ 1)
    (hcoset : ∀ l : ℤ, τ ((↑(w ^ l) : A) * d) = 0)
    (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc (-1) 1)) (l : ℤ) :
    τ ((cfc f (realPart (w : A) : A) * (↑(w ^ l) : A)) * d) = 0 := by
…