OAI/Probability/GaussianInformation/Dyadic/Realization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.through_snoc_castSucc line 22
2. lemma OAI.RepeatedLocalization.through_last line 29
3. instance OAI.RepeatedLocalization.AnalysisState.indexMeasurableSpace line 33
4. instance OAI.RepeatedLocalization.AnalysisState.indexMeasurableSingleton line 35
5. structure OAI.RepeatedLocalization.Realization line 37
6. lemma OAI.RepeatedLocalization.Realization.valid line 54
7. def OAI.RepeatedLocalization.initialRealization line 64
8. lemma OAI.RepeatedLocalization.ExtensionWitness.choose_meas line 82