RohlinUnitarity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Both unitary defects of a weighted Rohlin sum

The diagonal coefficient/projection commutators control both defects. The second estimate compares the adjoint weighted sum with the weighted adjoints; it does not require pairwise commutation of all coefficients and projections. The hypotheses still have to be supplied by the actual tower construction.

lemma OAI.WeakPureInfiniteness.adjoint_unitary_commutator_norm line 20
lemma OAI.WeakPureInfiniteness.star_mul_self_sub_norm_le line 31
lemma OAI.WeakPureInfiniteness.finiteRohlinSum_norm_le line 45
lemma OAI.WeakPureInfiniteness.finiteRohlinSum_star_commutator_le line 54

lemma OAI.WeakPureInfiniteness.finiteRohlinSum_isometry_defect_le line 73

Source documentation

The second defect has a dimension-dependent bound, sufficient when the commutator accuracy is chosen after the finite tower size.

lemma finiteRohlinSum_isometry_defect_le [Nontrivial E] (v : I → unitary E) (e : I → E)
    (he : ∀ i, star (e i) = e i) (hee : ∀ i, e i * e i = e i)
    (horth : ∀ i j, i ≠ j → e i * e j = 0)
    (hsum : (∑ i, e i) = 1) (δ : ℝ)
    (hc : ∀ i, ‖(v i : E) * e i - e i * (v i : E)‖ ≤ δ) :
    ‖star (finiteRohlinSum v e) * finiteRohlinSum v e - 1‖ ≤
      (Fintype.card I : ℝ) * (2 * Real.sqrt (Fintype.card I) + 1) * δ := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRohlinSum