OAI/NumberTheory/PrimePackets/LocalMoments.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PrimeDegreePackets.saturated_local_norm_moment line 23
  2. theorem OAI.PrimeDegreePackets.saturated_local_zero_components line 56
  3. theorem OAI.PrimeDegreePackets.haar_submodule_eq_inv_cardQuot line 82
  4. def OAI.PrimeDegreePackets.normalizedSubmoduleHaar line 104
  5. lemma OAI.PrimeDegreePackets.normalizedSubmoduleHaar_probability line 107
  6. lemma OAI.PrimeDegreePackets.normalizedSubmoduleHaar_leftInvariant line 125
  7. lemma OAI.PrimeDegreePackets.lintegral_normalizedSubmoduleHaar line 135
  8. lemma OAI.PrimeDegreePackets.ambient_lintegral_eq_normalized line 144
  9. lemma OAI.PrimeDegreePackets.projection_saturation line 162
  10. theorem OAI.PrimeDegreePackets.finite_index_saturated_module_norm_moment line 189
  11. theorem OAI.PrimeDegreePackets.haar_dvr_ideal_pow line 234
  12. lemma OAI.PrimeDegreePackets.dvr_shell_eq_sdiff line 248
  13. theorem OAI.PrimeDegreePackets.haar_dvr_shell line 259
  14. def OAI.PrimeDegreePackets.productDVRShell line 289
  15. lemma OAI.PrimeDegreePackets.productDVRShell_eq_pi line 292
  16. lemma OAI.PrimeDegreePackets.productDVRShell_nonempty line 297
  17. lemma OAI.PrimeDegreePackets.productDVRShell_smul_iff line 301
  18. lemma OAI.PrimeDegreePackets.productDVRShell_transitive line 309
  19. lemma OAI.PrimeDegreePackets.productDVRShell_pairwiseDisjoint line 320
  20. lemma OAI.PrimeDegreePackets.mem_iUnion_productDVRShell_iff line 328
  21. lemma OAI.PrimeDegreePackets.measurableSet_dvr_shell line 351
  22. lemma OAI.PrimeDegreePackets.measurableSet_productDVRShell line 365
  23. def OAI.PrimeDegreePackets.shellNorm line 383
  24. def OAI.PrimeDegreePackets.localZinv line 386
  25. lemma OAI.PrimeDegreePackets.product_shell_mass line 389
  26. lemma OAI.PrimeDegreePackets.localZinv_ne_zero line 401
  27. lemma OAI.PrimeDegreePackets.localZinv_ne_top line 414
  28. lemma OAI.PrimeDegreePackets.shellNorm_ne_zero line 420
  29. lemma OAI.PrimeDegreePackets.shellNorm_ne_top line 429
  30. lemma OAI.PrimeDegreePackets.shellNorm_eq_prime_pow line 437