OAI/Analysis/KadisonSimilarity/Similarity/KirchbergIntegral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The fundamental-theorem-of-calculus estimate in Kirchberg's Proposition 1, page 61.

  1. theorem OAI.KadisonSimilarity.integral_const_rpow_unit line 18
  2. theorem OAI.KadisonSimilarity.real_conjugation_hasDerivAt line 35
  3. theorem OAI.KadisonSimilarity.real_conjugation_integral line 45
  4. theorem OAI.KadisonSimilarity.norm_real_conjugation_le line 56

    Source documentation

    The matrix-independent path estimate. The precise condition-number scaling is supplied separately by functional calculus.

    theorem norm_real_conjugation_le (t a : B) {K : ℝ} (hK : 1 < K)
    (hscale : ∀ s ∈ Ioc (0 : ℝ) 1,
      ‖exp (s • (-t))‖ * ‖exp (s • t)‖ ≤ K ^ s) :
    ‖exp (-t) * a * exp t‖ ≤
      ‖a‖ + ‖a * t - t * a‖ * ((K - 1) / Real.log K) := by
…