OAI/Probability/Ballisticity/Estimates/PrefixVariationNonneg.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.prefixVariation_nonneg line 141
2. theorem OAI.DirectionalTransience.off_diagonal_comparison line 147
3. def OAI.DirectionalTransience.layerPairPrefix line 206
4. def OAI.DirectionalTransience.layerPairEvent line 214
5. def OAI.DirectionalTransience.layerPairTruthEvent line 218
6. lemma OAI.DirectionalTransience.measurableSet_layerPairPrefix line 223
7. lemma OAI.DirectionalTransience.layerPairPrefix_determined line 232
8. lemma OAI.DirectionalTransience.layerPairPrefix_disjoint line 248
9. lemma OAI.DirectionalTransience.layerPairTruthEvent_subset_noDrop line 261
10. theorem OAI.DirectionalTransience.shared_layer_truth_domination line 277