OAI/NumberTheory/PrimePackets/InverseEntropy.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.reverseNameEquiv line 45
  2. lemma OAI.PrimeDegreePackets.orbitName_inverse line 51
  3. theorem OAI.PrimeDegreePackets.orbitEntropy_inverse line 70
  4. theorem OAI.PrimeDegreePackets.measureEntropy_inverse line 81
  5. def OAI.PrimeDegreePackets.RelationDiameter line 99
  6. def OAI.PrimeDegreePackets.StepCover line 104
  7. lemma OAI.PrimeDegreePackets.stepCover_of_image line 108
  8. theorem OAI.PrimeDegreePackets.orbit_name_cover line 126
  9. theorem OAI.PrimeDegreePackets.orbit_name_mass line 212
  10. def OAI.PrimeDegreePackets.visitCount line 248
  11. lemma OAI.PrimeDegreePackets.visitCount_cast line 251
  12. lemma OAI.PrimeDegreePackets.integrable_visitCount line 259
  13. lemma OAI.PrimeDegreePackets.integral_visitCount line 268
  14. lemma OAI.PrimeDegreePackets.measurable_visitCount line 285
  15. theorem OAI.PrimeDegreePackets.measure_many_visits line 293
  16. lemma OAI.PrimeDegreePackets.matrixBall_mono line 312
  17. lemma OAI.PrimeDegreePackets.inverse_entries_uniform line 319
  18. lemma OAI.PrimeDegreePackets.left_div_entry_bound line 351
  19. theorem OAI.PrimeDegreePackets.small_matrix_ball_cover line 371
  20. lemma OAI.PrimeDegreePackets.one_mem_matrixBall line 442
  21. lemma OAI.PrimeDegreePackets.matrixBall_nhds_basis line 447
  22. lemma OAI.PrimeDegreePackets.local_uniform_chart_injective line 461
  23. theorem OAI.PrimeDegreePackets.compact_uniform_chart_injective line 486