OAI/Probability/Ballisticity/Estimates/ReferenceFeller.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.ReferenceClasses.referenceProb line 19
2. lemma OAI.DirectionalTransience.ReferenceClasses.integral_uniform_error line 22
3. lemma OAI.DirectionalTransience.ReferenceClasses.reference_integral_continuous line 34
4. theorem OAI.DirectionalTransience.ReferenceClasses.referenceProb_continuous line 65
5. lemma OAI.DirectionalTransience.Entropy.continuous_joint_integral line 83
6. def OAI.DirectionalTransience.Entropy.compProdProb line 117
7. def OAI.DirectionalTransience.Entropy.kernelProb line 120
8. lemma OAI.DirectionalTransience.Entropy.compProdProb_tendsto line 123