OAI/NumberTheory/PrimePackets/IntrinsicLeaves.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.selectedRootBox line 119
  2. lemma OAI.PrimeDegreePackets.selectedRootBox_mem line 121
  3. def OAI.PrimeDegreePackets.intrinsicRootLeaf line 126
  4. theorem OAI.PrimeDegreePackets.RootBox.ae_intrinsicRootLeaf_coordinates line 135
  5. lemma OAI.PrimeDegreePackets.RootBox.aemeasurable_intrinsicRootLeaf_restrict line 151
  6. lemma OAI.PrimeDegreePackets.RootBox.ae_intrinsicRootLeaf_spec_restrict line 161
  7. lemma OAI.PrimeDegreePackets.boundedRootAtlas_iUnion line 175
  8. theorem OAI.PrimeDegreePackets.aemeasurable_intrinsicRootLeaf line 181
  9. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_spec line 192
  10. def OAI.PrimeDegreePackets.intrinsicRootKernel line 206
  11. instance OAI.PrimeDegreePackets.intrinsicRootKernel_locallyFinite line 213
  12. instance OAI.PrimeDegreePackets.intrinsicRootKernel_sFinite line 219
  13. lemma OAI.PrimeDegreePackets.ae_intrinsicRootKernel_eq line 224
  14. lemma OAI.PrimeDegreePackets.RootBox.diagonal_time_bound line 244
  15. lemma OAI.PrimeDegreePackets.RootBox.ae_basedLeaf_diagonal line 257
  16. lemma OAI.PrimeDegreePackets.RootBox.ae_intrinsicRootLeaf_diagonal_restrict line 281
  17. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_diagonal line 305
  18. lemma OAI.PrimeDegreePackets.ae_eq_of_measurePreserving_ennreal_le line 325
  19. lemma OAI.PrimeDegreePackets.ae_eq_of_measurePreserving_ennreal_ge line 338
  20. lemma OAI.PrimeDegreePackets.realScaling_preimage_singleton line 352
  21. lemma OAI.PrimeDegreePackets.realScaling_preimage_unitBall_subset line 358
  22. lemma OAI.PrimeDegreePackets.realScaling_unitBall_subset_preimage line 366
  23. lemma OAI.PrimeDegreePackets.normalized_realScaling_atom line 373
  24. theorem OAI.PrimeDegreePackets.ae_atom_eq_of_scaling_covariance line 384
  25. lemma OAI.PrimeDegreePackets.scaling_ball_mass_of_atom_eq line 418
  26. lemma OAI.PrimeDegreePackets.realScaling_preimage_ball line 432
  27. lemma OAI.PrimeDegreePackets.real_iInter_ball_inv_nat line 439
  28. lemma OAI.PrimeDegreePackets.realMeasure_eq_dirac_of_ball_masses line 459
  29. theorem OAI.PrimeDegreePackets.ae_dirac_of_scaling_covariance line 492
  30. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_atom_dirac line 524
  31. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_zero_atom_or_trivial line 561