OAI/Probability/LatticePassage/OffsetCalibration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.mean_passageTime_endpoint_lipschitz line 9
2. def OAI.CompanionFPP.offsetTargetCocycle line 28
3. lemma OAI.CompanionFPP.measurable_offsetTargetCocycle line 32
4. lemma OAI.CompanionFPP.integrable_offsetTargetCocycle line 37
5. lemma OAI.CompanionFPP.integral_offset_target_step line 41
6. theorem OAI.CompanionFPP.integral_offsetTargetCocycle line 54
7. theorem OAI.CompanionFPP.offsetTargetCocycle_mean_error line 65