OAI/NumberTheory/PrimePackets/LeafAnchors.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PrimeDegreePackets.RootBox.ae_leafMeasure_change_anchor line 118
  2. theorem OAI.PrimeDegreePackets.RootBox.ae_change_anchor_mass line 165
  3. theorem OAI.PrimeDegreePackets.RootBox.ae_basedLeaf_change_anchor line 188
  4. theorem OAI.PrimeDegreePackets.RootBox.ae_basedLeaf_overlap line 212
  5. abbrev OAI.PrimeDegreePackets.RootSliceOverlap line 242
  6. def OAI.PrimeDegreePackets.rootTransitionPivot line 245
  7. def OAI.PrimeDegreePackets.rootTransitionTime line 248
  8. lemma OAI.PrimeDegreePackets.rootTransition_inverse_mul line 251
  9. def OAI.PrimeDegreePackets.rootTransitionSlice line 258
  10. lemma OAI.PrimeDegreePackets.rootTransitionTime_inverse line 264
  11. lemma OAI.PrimeDegreePackets.rootTransitionSlice_inverse line 273
  12. lemma OAI.PrimeDegreePackets.continuous_rootTransitionPivot line 282
  13. lemma OAI.PrimeDegreePackets.continuous_rootTransitionTime line 287
  14. lemma OAI.PrimeDegreePackets.continuous_rootTransitionSlice line 291
  15. def OAI.PrimeDegreePackets.rootSliceTransition line 298
  16. lemma OAI.PrimeDegreePackets.rootTransition_reconstruct line 317
  17. def OAI.PrimeDegreePackets.restrictFibers line 335
  18. instance OAI.PrimeDegreePackets.restrictFibers_finite line 346
  19. lemma OAI.PrimeDegreePackets.compProd_restrict_fibers line 352
  20. lemma OAI.PrimeDegreePackets.conditional_restrict_marginal line 361
  21. theorem OAI.PrimeDegreePackets.conditional_restrict_fibers line 374
  22. def OAI.PrimeDegreePackets.mapFibers line 394
  23. lemma OAI.PrimeDegreePackets.mapFibers_apply line 405
  24. instance OAI.PrimeDegreePackets.mapFibers_finite line 409
  25. lemma OAI.PrimeDegreePackets.fst_map_fibers line 416
  26. lemma OAI.PrimeDegreePackets.compProd_map_fibers line 425
  27. theorem OAI.PrimeDegreePackets.conditional_map_fibers line 442
  28. def OAI.PrimeDegreePackets.fiberShear line 462
  29. def OAI.PrimeDegreePackets.rootTransitionCoordinates line 473
  30. lemma OAI.PrimeDegreePackets.rootTransitionCoordinates_param line 477
  31. lemma OAI.PrimeDegreePackets.centerRealMeasure_translate line 495
  32. lemma OAI.PrimeDegreePackets.basedRealMeasure_translate line 504
  33. theorem OAI.PrimeDegreePackets.conditional_rootTransition line 510
  34. theorem OAI.PrimeDegreePackets.based_conditional_rootTransition line 521