OAI/Analysis/BackwardIntertwiners/HaarBase.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.BackwardIntertwiners.padicBorel line 13
  2. instance OAI.BackwardIntertwiners.padicBorelSpace line 14
  3. def OAI.BackwardIntertwiners.baseHaar line 16
  4. instance OAI.BackwardIntertwiners.baseHaar_probability line 17
  5. instance OAI.BackwardIntertwiners.baseHaar_regular line 20
  6. instance OAI.BackwardIntertwiners.baseHaar_addHaar line 21
  7. def OAI.BackwardIntertwiners.odometerBorel line 24
  8. lemma OAI.BackwardIntertwiners.odometerBorel_ergodic line 25
  9. lemma OAI.BackwardIntertwiners.continuous_twoResidue line 32
  10. def OAI.BackwardIntertwiners.twoResidue line 43
  11. lemma OAI.BackwardIntertwiners.twoResidue_lt line 44
  12. lemma OAI.BackwardIntertwiners.measurable_twoResidue line 45
  13. lemma OAI.BackwardIntertwiners.baseHaar_singleton_eq line 48
  14. instance OAI.BackwardIntertwiners.baseHaar_nullSingleton line 62
  15. lemma OAI.BackwardIntertwiners.measurePreserving_completion line 79
  16. lemma OAI.BackwardIntertwiners.ergodic_completion line 93
  17. abbrev OAI.BackwardIntertwiners.Base line 102
  18. abbrev OAI.BackwardIntertwiners.baseMeasure line 103
  19. instance OAI.BackwardIntertwiners.base_probability line 104
  20. instance OAI.BackwardIntertwiners.base_nullSingleton line 105
  21. instance OAI.BackwardIntertwiners.base_measurableSingleton line 110
  22. def OAI.BackwardIntertwiners.odometer line 115
  23. lemma OAI.BackwardIntertwiners.odometer_ergodic line 116
  24. def OAI.BackwardIntertwiners.residue line 120
  25. lemma OAI.BackwardIntertwiners.residue_lt line 121
  26. lemma OAI.BackwardIntertwiners.measurable_residue line 122
  27. def OAI.BackwardIntertwiners.goodBase line 127
  28. lemma OAI.BackwardIntertwiners.measurableSet_goodBase line 128
  29. lemma OAI.BackwardIntertwiners.ae_goodBase line 131
  30. lemma OAI.BackwardIntertwiners.goodBase_odometer line 133
  31. lemma OAI.BackwardIntertwiners.zmod_val_neg_one line 147
  32. lemma OAI.BackwardIntertwiners.residue_exceptional_iff line 151
  33. lemma OAI.BackwardIntertwiners.goodBase_eventually_nonexceptional line 157
  34. lemma OAI.BackwardIntertwiners.residue_step line 176