OAI/Probability/LatticePassage/WeakCalibration.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.convex_calibrationL2_Icc line 8
2. lemma OAI.CompanionFPP.approxL2_mem_Icc line 32
3. lemma OAI.CompanionFPP.weakLimit_mem_Icc line 47
4. def OAI.CompanionFPP.meanL2 line 58
5. lemma OAI.CompanionFPP.meanL2_eq_integral line 61
6. lemma OAI.CompanionFPP.weak_eval_continuous line 68
7. lemma OAI.CompanionFPP.approxL2_swap line 72
8. theorem OAI.CompanionFPP.calibration_weak_limit_properties line 79
9. theorem OAI.CompanionFPP.exists_directional_calibrationL2 line 123