OAI/Analysis/ModularTheory/ProjectionExhaustion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A concrete exhaustion of the modular core by finite-weight corners.

  1. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_strong line 16
  2. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_right_strong line 48
  3. lemma OAI.WeakPureInfiniteness.modularFiniteProjection_corner_strong line 54
  4. lemma OAI.WeakPureInfiniteness.modularCore_finite_right_dense line 80
  5. lemma OAI.WeakPureInfiniteness.modularCore_finite_corner_weight line 90
  6. lemma OAI.WeakPureInfiniteness.modularCore_finite_corner_adjoint_norm line 104