OAI/Analysis/WeakInfiniteness/FreeTreeNormExtension.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakPureInfiniteness.l2_summable_norm_sq line 22
  2. lemma OAI.WeakPureInfiniteness.l2_norm_sq line 27
  3. lemma OAI.WeakPureInfiniteness.weighted_two_mul_le line 32
  4. def OAI.WeakPureInfiniteness.permutationSum line 39
  5. lemma OAI.WeakPureInfiniteness.weighted_squares_summable line 42
  6. lemma OAI.WeakPureInfiniteness.weighted_squares_sum_le line 54
  7. theorem OAI.WeakPureInfiniteness.norm_permutationSum_le line 68
  8. def OAI.WeakPureInfiniteness.inverseLetterEquiv line 127
  9. lemma OAI.WeakPureInfiniteness.freeTreeWeight_inverse_sum_le line 133
  10. def OAI.WeakPureInfiniteness.freeTreeAdjacency line 142
  11. theorem OAI.WeakPureInfiniteness.norm_freeTreeAdjacency_le line 145
  12. theorem OAI.WeakPureInfiniteness.norm_freeTreeAdjacency_lt_four line 153