OAI/NumberTheory/PrimePackets/RootLeaves.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.RootBox.IsNormalizedRootLeaf line 115
2. def OAI.PrimeDegreePackets.RootBox.leafMeasure line 125
3. lemma OAI.PrimeDegreePackets.RootBox.leafMeasure_spec_of_exists line 129
4. theorem OAI.PrimeDegreePackets.RootBox.ae_leafMeasure_spec line 136
5. lemma OAI.PrimeDegreePackets.RootBox.IsNormalizedRootLeaf.unique line 146
6. lemma OAI.PrimeDegreePackets.RootBox.IsNormalizedRootLeaf.ne_zero line 153
7. theorem OAI.PrimeDegreePackets.RootBox.ae_leafMeasure_restrict line 168
8. theorem OAI.PrimeDegreePackets.RootBox.ae_leafMeasure_radius_independent line 220
9. theorem OAI.PrimeDegreePackets.RootBox.aemeasurable_leafMeasure_apply line 258
10. theorem OAI.PrimeDegreePackets.RootBox.aemeasurable_log_leafMeasure line 305
11. lemma OAI.PrimeDegreePackets.normalized_translation_invariant_measure line 322
12. theorem OAI.PrimeDegreePackets.RootBox.hasHaarConditionals_of_invariant_leafMeasure line 340
13. lemma OAI.PrimeDegreePackets.anchorNormalize_map_equiv line 374
14. lemma OAI.PrimeDegreePackets.RootBox.base_ae_of_ae line 386
15. lemma OAI.PrimeDegreePackets.RootBox.diagonal_marginal line 401
16. theorem OAI.PrimeDegreePackets.RootBox.ae_leafMeasure_diagonal line 413
17. lemma OAI.PrimeDegreePackets.measurable_measure_restrict line 494
18. lemma OAI.PrimeDegreePackets.measurable_measure_sum line 502
19. lemma OAI.PrimeDegreePackets.measure_eq_sum_disjointed line 509
20. lemma OAI.PrimeDegreePackets.RootBox.aemeasurable_leafMeasure_restrict_window line 520
21. theorem OAI.PrimeDegreePackets.RootBox.aemeasurable_leafMeasure line 556
22. def OAI.PrimeDegreePackets.RootBox.leafKernel line 583
23. lemma OAI.PrimeDegreePackets.RootBox.ae_leafKernel_eq line 592