OAI/Probability/LatticePassage/StationaryCalibration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.environmentTranslation_zero line 9
2. lemma OAI.CompanionFPP.translationL2_zero line 17
3. lemma OAI.CompanionFPP.translationL2_add line 22
4. lemma OAI.CompanionFPP.translationL2_injective line 30
5. def OAI.CompanionFPP.calibrationCovarianceSubgroup line 34
6. lemma OAI.CompanionFPP.covariance_of_generators line 48
7. structure OAI.CompanionFPP.DirectionalCalibration line 61
8. theorem OAI.CompanionFPP.exists_directionalCalibration line 71