OAI/Probability/LatticePassage/PlanarCalibration.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompanionFPP.abs_range_average_le line 10
  2. def OAI.CompanionFPP.planarTargetCocycle line 18
  3. lemma OAI.CompanionFPP.measurable_planarTargetCocycle line 22
  4. lemma OAI.CompanionFPP.integrable_planarTargetCocycle line 27
  5. theorem OAI.CompanionFPP.planarTargetCocycle_add line 31
  6. theorem OAI.CompanionFPP.planarTargetCocycle_dominated line 39
  7. theorem OAI.CompanionFPP.planarTargetCocycle_memLp_two line 50
  8. theorem OAI.CompanionFPP.planarTargetCocycle_second_moment line 57
  9. theorem OAI.CompanionFPP.planarTargetCocycle_swap line 67
  10. theorem OAI.CompanionFPP.planarTargetCocycle_shift_bound line 72
  11. theorem OAI.CompanionFPP.planarTargetCocycle_shift_integral line 87
  12. theorem OAI.CompanionFPP.planarTargetCocycle_eq_offsets line 102
  13. theorem OAI.CompanionFPP.planarTargetCocycle_mean_error line 116
  14. lemma OAI.CompanionFPP.latticeDistance_planar_offset_le line 149
  15. def OAI.CompanionFPP.calibrationApprox line 164
  16. theorem OAI.CompanionFPP.calibrationApprox_mean_error line 168
  17. theorem OAI.CompanionFPP.calibrationApprox_mean_tendsto line 180
  18. theorem OAI.CompanionFPP.calibrationApprox_shift_tendsto line 197
  19. theorem OAI.CompanionFPP.calibrationApprox_second_shift_tendsto line 206