OAI/NumberTheory/PrimePackets/PrimeFactors.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.prime_dvd_card_padic_module line 24
  2. lemma OAI.PrimeDegreePackets.prime_le_cardQuot line 36
  3. lemma OAI.PrimeDegreePackets.ennreal_tsum_fintype_prod line 50
  4. lemma OAI.PrimeDegreePackets.local_weight_product_factorization line 81
  5. lemma OAI.PrimeDegreePackets.unit_contains_probability line 95
  6. def OAI.PrimeDegreePackets.localProductConstant line 112
  7. lemma OAI.PrimeDegreePackets.localProductConstant_pos line 115
  8. lemma OAI.PrimeDegreePackets.localProductConstant_bound line 119
  9. def OAI.PrimeDegreePackets.localIndexProduct line 144
  10. def OAI.PrimeDegreePackets.packetLocalWeight line 146
  11. def OAI.PrimeDegreePackets.packetLocalNorm line 149
  12. theorem OAI.PrimeDegreePackets.global_local_weight_sum line 154
  13. theorem OAI.PrimeDegreePackets.global_local_weight_moment line 179
  14. lemma OAI.PrimeDegreePackets.reciprocal_norm_tail_le line 243
  15. lemma OAI.PrimeDegreePackets.reciprocal_norm_tail_of_moment line 267
  16. lemma OAI.PrimeDegreePackets.packetLocalNorm_ne_zero line 317
  17. lemma OAI.PrimeDegreePackets.packetLocalNorm_ne_top line 326
  18. theorem OAI.PrimeDegreePackets.global_local_weight_tail line 332
  19. def OAI.PrimeDegreePackets.modelUnitProbability line 377
  20. lemma OAI.PrimeDegreePackets.modelUnitProbability_isProbability line 383
  21. lemma OAI.PrimeDegreePackets.modelUnitProbability_isHaar line 392
  22. lemma OAI.PrimeDegreePackets.smul_normalized_mem_iff line 401
  23. lemma OAI.PrimeDegreePackets.actual_containment_eq_model_orbit line 414
  24. lemma OAI.PrimeDegreePackets.integral_idealLocalGenerator line 453
  25. lemma OAI.PrimeDegreePackets.nonZeroDivisor_component_ne_zero line 464
  26. lemma OAI.PrimeDegreePackets.model_generator_components_ne_zero line 477
  27. theorem OAI.PrimeDegreePackets.localIdealWeight_eq_model_shell line 493