OAI/Analysis/KadisonSimilarity/Similarity/KirchbergExponentialNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact exponential condition-number scaling used on page 61 of Kirchberg's proof.

  1. theorem OAI.KadisonSimilarity.exp_real_smul_eq_rpow line 18
  2. theorem OAI.KadisonSimilarity.norm_exp_real_smul line 28
  3. theorem OAI.KadisonSimilarity.exp_condition_real_smul line 33

    Source documentation

    The product of the forward and inverse norms scales by the same power.

    theorem exp_condition_real_smul (t : B) (ht : IsSelfAdjoint t) {s : ℝ} (hs : 0 < s) :
    ‖exp (s • (-t))‖ * ‖exp (s • t)‖ = (‖exp (-t)‖ * ‖exp t‖) ^ s := by
…