OAI/Analysis/OInfinity/RohlinPolar.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polar correction of the finite Rohlin sum

Both Gram defects are used. An element with small initial and final Gram defects is invertible; continuous functional calculus then corrects it to a nearby unitary. This step does not supply the tower commutator estimates.

  1. lemma OAI.WeakPureInfiniteness.isUnit_of_two_gram_units line 19
  2. lemma OAI.WeakPureInfiniteness.isUnit_of_norm_sub_one_lt line 36
  3. lemma OAI.WeakPureInfiniteness.exists_polar_unitary_of_two_gram_units line 44
  4. lemma OAI.WeakPureInfiniteness.exists_near_unitary_of_two_gram_errors line 69

    Source documentation

    An arbitrarily small polar correction follows from a sufficiently small initial Gram defect and a final Gram defect less than one.

    lemma exists_near_unitary_of_two_gram_errors [Nontrivial E] (ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ x : E,
      ‖star x * x - 1‖ < δ → ‖x * star x - 1‖ < 1 →
      ∃ u : unitary E, ‖(u : E) - x‖ < ε := by
…