OAI/Probability/Ballisticity/Estimates/ProfileMeasureUpdate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.measure_le_of_atoms line 12
2. def OAI.DirectionalTransience.arrayProfileMeasure line 23
3. lemma OAI.DirectionalTransience.arrayProfileMeasure_atom line 27
4. lemma OAI.DirectionalTransience.arrayProfileImage line 32
5. lemma OAI.DirectionalTransience.arrayProfile_measure_update line 40
6. lemma OAI.DirectionalTransience.properProfileKernel_eq_map line 49
7. lemma OAI.DirectionalTransience.properData_kernel_eq line 56
8. lemma OAI.DirectionalTransience.horizontalKernel_fill line 63
9. lemma OAI.DirectionalTransience.horizontalProfileImage_fill line 93