OAI/Analysis/KadisonSimilarity/FreeProduct/AngularIntegralBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Norm control for the normalized angular Fourier integrals used in the spectral-arc construction.

  1. def OAI.KadisonSimilarity.angularIntegral line 12
  2. theorem OAI.KadisonSimilarity.angularIntegral_const line 15
  3. theorem OAI.KadisonSimilarity.norm_angularCharacter line 21
  4. theorem OAI.KadisonSimilarity.angularIntegral_sub line 24
  5. theorem OAI.KadisonSimilarity.angularIntegral_norm_le line 34

    Source documentation

    Normalized angular integration is contractive for the uniform bound.

    theorem angularIntegral_norm_le (f : ℝ → ℂ) (l : ℤ) {C : ℝ}
    (_hC : 0 ≤ C) (hf : ∀ x ∈ Set.Ioc (-Real.pi) Real.pi, ‖f x‖ ≤ C) :
    ‖angularIntegral f l‖ ≤ C := by
…

    Mentions: OAI.KadisonSimilarity.angularIntegral

  6. theorem OAI.KadisonSimilarity.angularIntegral_continuous_sub_bound line 52