OAI/Analysis/Kaplansky/Regular/PowersAverages.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyConsequences.Regular.conjugateMap line 14
  2. lemma OAI.KaplanskyConsequences.Regular.conjugateMap_val line 19
  3. lemma OAI.KaplanskyConsequences.Regular.conjugateMap_norm_le line 21
  4. lemma OAI.KaplanskyConsequences.Regular.conjugateMap_one line 23
  5. lemma OAI.KaplanskyConsequences.Regular.conjugateMap_mul line 27
  6. lemma OAI.KaplanskyConsequences.Regular.conjugateMap_generator line 32
  7. def OAI.KaplanskyConsequences.Regular.averageConjugate line 39
  8. lemma OAI.KaplanskyConsequences.Regular.averageConjugate_apply line 42
  9. lemma OAI.KaplanskyConsequences.Regular.averageConjugate_norm_le line 47
  10. lemma OAI.KaplanskyConsequences.Regular.averageConjugate_one line 56
  11. lemma OAI.KaplanskyConsequences.Regular.averageConjugate_val line 62
  12. lemma OAI.KaplanskyConsequences.Regular.mask_left_mask_zero line 69