OAI/Analysis/IrrationalRotation/Sampling/SampleMapConditioning.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.SampleMapConditioning.condExp_observation_comp_measurePreserving line 12
2. theorem OAI.Invariant233.SampleMapConditioning.condExp_preimage_indicator line 37
3. theorem OAI.Invariant233.SampleMapConditioning.condExp_preimage_indicator_le line 53
4. theorem OAI.Invariant233.SampleMapConditioning.condExp_preimage_indicator_le_countable line 66
5. theorem OAI.Invariant233.SampleMapConditioning.condExp_preimage_indicator_le_countable_on line 80
6. theorem OAI.Invariant233.SampleMapConditioning.condExp_preimage_indicator_of_observation_ae line 96