OAI/Analysis/OInfinity/RohlinGluing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Weighted finite Rohlin sums

Orthogonal projection domains give a square-sum norm bound. Hence N coefficient errors of size L/N contribute at most L/√N, even before commutation with the projections is imposed. The shift and unitarity errors are tracked separately.

  1. lemma OAI.WeakPureInfiniteness.weightedProjection_norm_le_one line 20
  2. lemma OAI.WeakPureInfiniteness.orthogonalWeighted_square line 26
  3. lemma OAI.WeakPureInfiniteness.orthogonalWeighted_norm_sq_le line 44
  4. lemma OAI.WeakPureInfiniteness.orthogonalWeighted_norm_le line 66
  5. def OAI.WeakPureInfiniteness.finiteRohlinSum line 82
  6. lemma OAI.WeakPureInfiniteness.finiteRohlinSum_defect_identity line 85
  7. lemma OAI.WeakPureInfiniteness.finiteRohlinSum_defect_le line 106
  8. lemma OAI.WeakPureInfiniteness.finiteRohlinSum_coisometry_defect_le line 139

    Source documentation

    One of the two unitary defects only needs the diagonal commutators.

    lemma finiteRohlinSum_coisometry_defect_le (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)‖ ≤ δ) :
    ‖finiteRohlinSum v e * star (finiteRohlinSum v e) - 1‖ ≤ (Fintype.card I : ℝ) * δ := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteRohlinSum