OAI/Probability/Ballisticity/Estimates/AllLayerOccupation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.physical_small_gap_prefix line 16
2. lemma OAI.DirectionalTransience.layer_truth_small_subset line 57
3. lemma OAI.DirectionalTransience.physical_small_gap_truth_domination line 65
4. lemma OAI.DirectionalTransience.smallCommonCount_lintegral line 81
5. theorem OAI.DirectionalTransience.all_layers_occupation_le line 105
6. def OAI.DirectionalTransience.occupationMacroConstant line 144
7. lemma OAI.DirectionalTransience.occupationMacroConstant_pos line 147
8. lemma OAI.DirectionalTransience.occupation_coefficient_normalization line 152
9. lemma OAI.DirectionalTransience.real_sum_le_of_ennreal_count line 164
10. lemma OAI.DirectionalTransience.real_all_layer_bound line 174