OAI/Analysis/KadisonKastler/QuantitativePolarPath.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_continuous_polar_path line 16

   Source documentation

   The smoothing estimates produce a continuous unitary family with explicit errors in both factors. Only the first family needs continuity.

   theorem exists_continuous_polar_path (a c : X → A) (ha : Continuous a)
       {r : ℝ} (hr : 0 ≤ r) (hrsmall : r < 1 / 8)
       (hanorm : ∀ x, ‖a x‖ ≤ 1 + r) (hcnorm : ∀ x, ‖c x‖ ≤ 1 + r)
       (hac : ∀ x, ‖a x * c x - 1‖ ≤ r) (hca : ∀ x, ‖c x * a x - 1‖ ≤ r) :
       ∃ v : X → unitary A, Continuous v ∧
         (∀ x, ‖(v x : A) - a x‖ ≤ 4 * r) ∧
         (∀ x, ‖star (v x : A) - c x‖ ≤ 10 * r) := by
   …