OAI/Probability/LatticePassage/MetricCalibration.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompanionFPP.targetCocycle line 9
  2. theorem OAI.CompanionFPP.measurable_targetCocycle line 12
  3. theorem OAI.CompanionFPP.integrable_targetCocycle line 16
  4. theorem OAI.CompanionFPP.targetCocycle_add line 20
  5. theorem OAI.CompanionFPP.targetCocycle_dominated line 25
  6. theorem OAI.CompanionFPP.targetCocycle_translation line 36
  7. def OAI.CompanionFPP.averagedTargetCocycle line 41
  8. theorem OAI.CompanionFPP.averagedTargetCocycle_add line 45
  9. theorem OAI.CompanionFPP.integrable_averagedTargetCocycle line 51
  10. theorem OAI.CompanionFPP.averagedTargetCocycle_dominated line 55
  11. lemma OAI.CompanionFPP.integral_targetCocycle_step line 70
  12. theorem OAI.CompanionFPP.integral_averagedTargetCocycle line 85
  13. theorem OAI.CompanionFPP.mean_averagedTargetCocycle_tendsto line 101