OAI/MeasureTheory/Falconer/Measures/DyadicMeasure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.DyadicSquare.descendant line 12
2. theorem OAI.PlanarFalconer.DyadicSquare.descendant_side_pos line 17
3. theorem OAI.PlanarFalconer.DyadicSquare.descendant_subset line 23
4. theorem OAI.PlanarFalconer.measure_zero_of_disjoint_carrier line 30
5. theorem OAI.PlanarFalconer.four_measures_on_branch line 35
6. def OAI.PlanarFalconer.DyadicMassBounds line 46
7. theorem OAI.PlanarFalconer.routes_mass_bounds line 50
8. theorem OAI.PlanarFalconer.measure_from_geometric_routes line 56
9. theorem OAI.PlanarFalconer.exists_dyadic_probability_sequence line 129