OAI/NumberTheory/GaussianMoat/KernelComposition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GaussianMoat.FinLaw.pure line 10
2. lemma OAI.GaussianMoat.FinLaw.mix_pure line 15
3. lemma OAI.GaussianMoat.FinLaw.joint_pure_observation line 20
4. def OAI.GaussianMoat.TimeLaw.at line 26
5. lemma OAI.GaussianMoat.TimeLaw.at_advance line 30
6. lemma OAI.GaussianMoat.SplitSieve.pointEntropy_exact_start line 38
7. theorem OAI.GaussianMoat.TimeLaw.advance_entropy_succ line 48
8. theorem OAI.GaussianMoat.commonSchedule_subband_entropy line 76
9. lemma OAI.GaussianMoat.ForwardKernel.ext_observe line 108
10. lemma OAI.GaussianMoat.ForwardKernel.then_assoc line 126
11. lemma OAI.GaussianMoat.FinLaw.map_pure line 146
12. lemma OAI.GaussianMoat.FinLaw.mix_pure_right line 156
13. lemma OAI.GaussianMoat.smoothingKernel_zero_law line 164
14. lemma OAI.GaussianMoat.ForwardKernel.then_zero line 171
15. lemma OAI.GaussianMoat.ForwardKernel.zero_then line 182
16. lemma OAI.GaussianMoat.commonSchedule_append line 193