OAI/Analysis/OInfinity/CocycleGluing.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Finite cocycle coefficients with an exact terminal seam

A path from V_N to 1 gives coefficients V_k α^[k](p(k/N)). The zeroth and terminal coefficients agree exactly, while consecutive coefficients satisfy the cocycle equation up to L/N. These are the coefficients for finite Rohlin gluing; commutation with the gluing projections is a separate requirement.

  1. lemma OAI.WeakPureInfiniteness.binarySplitHom_sub_norm_le line 21
  2. lemma OAI.WeakPureInfiniteness.unitaryHom_iterate_sub_norm_le line 31
  3. lemma OAI.WeakPureInfiniteness.unitaryHom_iterate_one line 41
  4. def OAI.WeakPureInfiniteness.finiteCocycleCoefficient line 47
  5. lemma OAI.WeakPureInfiniteness.finiteCocycleCoefficient_zero line 51
  6. lemma OAI.WeakPureInfiniteness.finiteCocycleCoefficient_terminal line 57
  7. lemma OAI.WeakPureInfiniteness.finiteCocycleCoefficient_step line 62
  8. lemma OAI.WeakPureInfiniteness.finiteCocycleCoefficient_step_norm line 69
  9. def OAI.WeakPureInfiniteness.cocycleGridTime line 85

    Source documentation

    The actual finite mesh. Its endpoint belongs to the same unit interval.

    def cocycleGridTime (N : ℕ) (hN : 0 < N) (k : Fin (N + 1)) : unitInterval :=
…
  10. lemma OAI.WeakPureInfiniteness.cocycleGridTime_zero line 92
  11. lemma OAI.WeakPureInfiniteness.cocycleGridTime_last line 98
  12. lemma OAI.WeakPureInfiniteness.cocycleGridTime_step line 104
  13. lemma OAI.WeakPureInfiniteness.finiteCocycleCoefficient_grid_seam line 111
  14. lemma OAI.WeakPureInfiniteness.finiteCocycleCoefficient_grid_step line 118