OAI/Probability/BinarySweep/Mixing/DimensionSeries.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Young.dimensionInv line 11
2. def OAI.BinaryCoordinateSweeps.Young.dimensionFiber line 14
3. def OAI.BinaryCoordinateSweeps.Young.dimensionSeries line 17
4. lemma OAI.BinaryCoordinateSweeps.Young.dimensionInv_nonneg line 20
5. lemma OAI.BinaryCoordinateSweeps.Young.dimensionInv_exponential line 23
6. lemma OAI.BinaryCoordinateSweeps.Young.dimensionFiber_nonneg line 40
7. lemma OAI.BinaryCoordinateSweeps.Young.dimensionFiber_bound line 46
8. lemma OAI.BinaryCoordinateSweeps.Young.dimensionFiber_grows_bound line 62
9. lemma OAI.BinaryCoordinateSweeps.Young.dimensionFiber_tendsto line 81
10. lemma OAI.BinaryCoordinateSweeps.Young.dimensionFiber_eq_filter line 99
11. lemma OAI.BinaryCoordinateSweeps.Young.dimensionSeries_tsum line 117
12. theorem OAI.BinaryCoordinateSweeps.Young.dimensionSeries_tendsto line 137