OAI/Combinatorics/SumProduct/Alignment/CentralFiber01.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CentralFiberAverage.average line 21
  2. lemma OAI.CentralFiberAverage.continuous_average line 27
  3. lemma OAI.CentralFiberAverage.average_smul line 37
  4. lemma OAI.CentralFiberAverage.integral_average line 44
  5. theorem OAI.CentralFiberAverage.exists_average_descend line 62
  6. theorem OAI.CentralFiberAverage.measure_eq_of_map_eq line 84
  7. theorem OAI.CentralFiberAverage.exists_right_probability line 106
  8. theorem OAI.CentralFiberAverage.ext_of_map_eq line 117
  9. lemma OAI.RationalNilmanifoldMeasure.normal_of_central line 139
  10. theorem OAI.RationalNilmanifoldMeasure.measure_eq_of_central_map_eq line 149
  11. lemma OAI.CompactGroupProducts.HasCompactReps.map line 190
  12. theorem OAI.RationalNilmanifoldMeasure.invariant_unique_of_series line 207