OAI/NumberTheory/PrimePackets/AmbientLeaves.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.RootBox.ae_coordinate_of_ambient line 118
  2. theorem OAI.PrimeDegreePackets.RootBox.ae_leafMeasure_of_ambient line 127
  3. lemma OAI.PrimeDegreePackets.RootBox.ae_basedLeaf_of_ambient line 168
  4. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_of_ambient line 191
  5. theorem OAI.PrimeDegreePackets.RootBox.ae_leafMeasure_intrinsic line 218
  6. lemma OAI.PrimeDegreePackets.RootBox.ae_basedLeaf_rebase line 276
  7. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_rebase line 302
  8. lemma OAI.PrimeDegreePackets.centerRealMeasure_singleton line 326
  9. lemma OAI.PrimeDegreePackets.basedRealMeasure_atom_ne_zero line 334
  10. lemma OAI.PrimeDegreePackets.ae_property_at_atom line 340
  11. theorem OAI.PrimeDegreePackets.realLeaf_nullSingleton_or_dirac line 347
  12. lemma OAI.PrimeDegreePackets.basedRealMeasure_ball_pos line 401
  13. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_ball_pos line 410
  14. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_nullSingleton_or_dirac line 432
  15. lemma OAI.PrimeDegreePackets.translation_invariant_of_based line 455
  16. theorem OAI.PrimeDegreePackets.RootBox.hasHaarConditionals_of_intrinsic line 481
  17. theorem OAI.PrimeDegreePackets.root_invariant_of_intrinsic line 511
  18. theorem OAI.PrimeDegreePackets.measure_eq_haar_of_intrinsic_roots line 550