OAI/Analysis/WeakInfiniteness/FreeTwistedNorm.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WeakPureInfiniteness.FreeTwo line 18
  2. abbrev OAI.WeakPureInfiniteness.FreeLetter line 20
  3. def OAI.WeakPureInfiniteness.freeLetter line 22
  4. def OAI.WeakPureInfiniteness.inverseLetter line 25
  5. lemma OAI.WeakPureInfiniteness.freeLetter_inverseLetter line 28
  6. lemma OAI.WeakPureInfiniteness.inverseLetter_inverseLetter line 34
  7. lemma OAI.WeakPureInfiniteness.toWord_freeLetter line 40
  8. lemma OAI.WeakPureInfiniteness.toWord_freeLetter_mul line 44
  9. def OAI.WeakPureInfiniteness.freeTreeWeight line 56
  10. lemma OAI.WeakPureInfiniteness.freeTreeWeight_pos line 58
  11. lemma OAI.WeakPureInfiniteness.freeTreeWeight_one line 61
  12. lemma OAI.WeakPureInfiniteness.freeTreeWeight_step_nil line 64
  13. lemma OAI.WeakPureInfiniteness.freeTreeWeight_step_cons line 68
  14. theorem OAI.WeakPureInfiniteness.freeTreeWeight_sum_le line 88
  15. lemma OAI.WeakPureInfiniteness.freeTree_norm_gap line 109
  16. theorem OAI.WeakPureInfiniteness.norm_freeTwisted_sum_le line 114