OAI/NumberTheory/PrimePackets/AtomMass.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.small_matrixBall_pairwise line 48
  2. theorem OAI.PrimeDegreePackets.homogeneous_name_atom_mass line 63
  3. def OAI.PrimeDegreePackets.entropyGoodSet line 124
  4. lemma OAI.PrimeDegreePackets.entropyGoodSet_measurable line 127
  5. theorem OAI.PrimeDegreePackets.entropyGoodSet_mass line 135
  6. lemma OAI.PrimeDegreePackets.tendsto_entropyMidpoint line 179
  7. lemma OAI.PrimeDegreePackets.branching_exp_bound line 187
  8. theorem OAI.PrimeDegreePackets.good_name_atom_mass line 230
  9. theorem OAI.PrimeDegreePackets.entropy_lower_of_ordinary_balls line 295
  10. lemma OAI.PrimeDegreePackets.diagonalOneParameter_eq_diagonalFlow line 392
  11. theorem OAI.PrimeDegreePackets.entropy_from_ordinary_balls_dominated line 412
  12. def OAI.PrimeDegreePackets.regularDiagonalWeights line 438
  13. lemma OAI.PrimeDegreePackets.regularDiagonalWeights_sum line 441
  14. lemma OAI.PrimeDegreePackets.regularDiagonalWeights_separated line 446
  15. theorem OAI.PrimeDegreePackets.positive_entropy_every_dominated_invariant line 463