OAI/Probability/LatticePassage/RectangleCalibration.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompanionFPP.rectangleTargetCocycle line 9
  2. lemma OAI.CompanionFPP.measurable_rectangleTargetCocycle line 14
  3. lemma OAI.CompanionFPP.integrable_rectangleTargetCocycle line 19
  4. theorem OAI.CompanionFPP.rectangleTargetCocycle_add line 24
  5. lemma OAI.CompanionFPP.rectangleTargetCocycle_swap line 32
  6. theorem OAI.CompanionFPP.rectangleTargetCocycle_dominated line 44
  7. theorem OAI.CompanionFPP.rectangleTargetCocycle_shift_identity line 65
  8. theorem OAI.CompanionFPP.rectangleTargetCocycle_shift_bound line 90
  9. theorem OAI.CompanionFPP.rectangleTargetCocycle_shift_integral line 117
  10. theorem OAI.CompanionFPP.rectangleTargetCocycle_second_shift_integral line 132
  11. theorem OAI.CompanionFPP.rectangleTargetCocycle_memLp_two line 140
  12. theorem OAI.CompanionFPP.rectangleTargetCocycle_second_moment line 147
  13. theorem OAI.CompanionFPP.rectangleTargetCocycle_shift_tendsto line 157
  14. theorem OAI.CompanionFPP.rectangleTargetCocycle_second_shift_tendsto line 169