OAI/NumberTheory/PrimePackets/OrbitProbability.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PrimeDegreePackets.haar_dvr_zero line 24
  2. def OAI.PrimeDegreePackets.orbitContainmentProbability line 58
  3. lemma OAI.PrimeDegreePackets.orbitContainmentProbability_eq_measure line 62
  4. lemma OAI.PrimeDegreePackets.orbitContainmentProbability_smul line 72
  5. theorem OAI.PrimeDegreePackets.orbitContainmentProbability_mul_shell_measure line 80
  6. theorem OAI.PrimeDegreePackets.lintegral_eq_tsum_shells line 126
  7. theorem OAI.PrimeDegreePackets.restricted_lintegral_eq_tsum_shells line 147
  8. lemma OAI.PrimeDegreePackets.units_smulInvariant_addHaar line 165
  9. lemma OAI.PrimeDegreePackets.measurableSMul_units line 178
  10. lemma OAI.PrimeDegreePackets.productDVRShell_full_measure line 197
  11. def OAI.PrimeDegreePackets.localShellProbability line 214
  12. lemma OAI.PrimeDegreePackets.localShellProbability_mul_mass line 238
  13. theorem OAI.PrimeDegreePackets.local_weight_integral_identity line 252
  14. theorem OAI.PrimeDegreePackets.local_weight_sum line 293
  15. theorem OAI.PrimeDegreePackets.local_weight_moment line 307
  16. def OAI.PrimeDegreePackets.localMajorant line 342
  17. lemma OAI.PrimeDegreePackets.localMajorant_nonneg line 345
  18. lemma OAI.PrimeDegreePackets.localMajorant_tendsto_one line 352
  19. theorem OAI.PrimeDegreePackets.finite_product_subpolynomial line 368
  20. theorem OAI.PrimeDegreePackets.localMajorant_product_le line 413
  21. lemma OAI.PrimeDegreePackets.localZinv_inv_le line 430
  22. lemma OAI.PrimeDegreePackets.localEulerFactor_le_majorant line 447