OAI/NumberTheory/PrimePackets/LeafNormalization.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.RootBox.shrink_marginal_absolutelyContinuous line 113
  2. lemma OAI.PrimeDegreePackets.RootBox.shrink_marginal_ae_anchor_pos line 122
  3. theorem OAI.PrimeDegreePackets.RootBox.overlap_anchorNormalize line 134
  4. theorem OAI.PrimeDegreePackets.RootBox.overlap_anchorNormalize_restrict line 164
  5. instance OAI.PrimeDegreePackets.rootSliceSecondCountable line 182
  6. theorem OAI.PrimeDegreePackets.exists_countable_rootBoxes_exact_time line 188
  7. theorem OAI.PrimeDegreePackets.RootBox.ae_injective_root_slice_of_ae_free line 213
  8. theorem OAI.PrimeDegreePackets.RootBox.ae_injective_root_slice line 237
  9. lemma OAI.PrimeDegreePackets.RootBox.shrink_full_time_marginal line 249
  10. theorem OAI.PrimeDegreePackets.RootBox.base_overlap_anchorNormalize line 270
  11. theorem OAI.PrimeDegreePackets.RootBox.base_anchor_restrict line 294
  12. theorem OAI.PrimeDegreePackets.RootBox.base_overlap_restrict line 314
  13. def OAI.PrimeDegreePackets.rootLeafWindow line 333
  14. lemma OAI.PrimeDegreePackets.rootLeafWindow_open line 335
  15. lemma OAI.PrimeDegreePackets.rootLeafWindow_mono line 337
  16. lemma OAI.PrimeDegreePackets.rootLeafWindow_cover line 342
  17. def OAI.PrimeDegreePackets.rootLongBoxFamily line 358
  18. lemma OAI.PrimeDegreePackets.rootLongBoxFamily_countable line 361
  19. lemma OAI.PrimeDegreePackets.rootLongBoxFamily_time line 365
  20. lemma OAI.PrimeDegreePackets.rootLongBoxFamily_covers line 370
  21. def OAI.PrimeDegreePackets.increasingMeasureLimit line 384
  22. lemma OAI.PrimeDegreePackets.increasingMeasureLimit_apply line 393
  23. lemma OAI.PrimeDegreePackets.le_increasingMeasureLimit line 398
  24. lemma OAI.PrimeDegreePackets.increasingMeasureLimit_le line 405
  25. lemma OAI.PrimeDegreePackets.restrictionChain_monotone line 414
  26. theorem OAI.PrimeDegreePackets.increasingMeasureLimit_restrict line 421
  27. theorem OAI.PrimeDegreePackets.measure_eq_of_restrictionChain line 441
  28. theorem OAI.PrimeDegreePackets.increasingMeasureLimit_locallyFinite line 453
  29. theorem OAI.PrimeDegreePackets.RootBox.ae_exists_rootLeafMeasure line 478
  30. theorem OAI.PrimeDegreePackets.RootBox.rootLeafMeasure_unique line 564