OAI/NumberTheory/PrimePackets/LocalModels.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PrimeDegreePackets.ActualLocalModel line 26
  2. lemma OAI.PrimeDegreePackets.actualLocalModel_nonempty line 57
  3. def OAI.PrimeDegreePackets.actualLocalModel line 63
  4. instance OAI.PrimeDegreePackets.model_measurableSpace line 66
  5. instance OAI.PrimeDegreePackets.model_borelSpace line 69
  6. instance OAI.PrimeDegreePackets.model_units_measurableSpace line 72
  7. instance OAI.PrimeDegreePackets.model_units_borelSpace line 76
  8. def OAI.PrimeDegreePackets.modelAddHaarProbability line 81
  9. instance OAI.PrimeDegreePackets.modelAddHaarProbability_isProbability line 86
  10. instance OAI.PrimeDegreePackets.modelAddHaarProbability_isHaar line 92
  11. instance OAI.PrimeDegreePackets.model_actual_unit_probability line 97
  12. instance OAI.PrimeDegreePackets.model_actual_unit_haar line 102
  13. abbrev OAI.PrimeDegreePackets.actualValuationTuples line 108
  14. def OAI.PrimeDegreePackets.actualTupleWeight line 111
  15. def OAI.PrimeDegreePackets.actualTupleNorm line 117
  16. def OAI.PrimeDegreePackets.actualLocalZ line 121
  17. lemma OAI.PrimeDegreePackets.actualTupleNorm_ne_zero line 125
  18. lemma OAI.PrimeDegreePackets.actualTupleNorm_ne_top line 129
  19. theorem OAI.PrimeDegreePackets.actual_tuple_weight_sum line 134
  20. theorem OAI.PrimeDegreePackets.global_local_weight_moment_of_support_prod_le line 177
  21. theorem OAI.PrimeDegreePackets.actual_tuple_weight_moment line 233
  22. lemma OAI.PrimeDegreePackets.dvr_principal_eq_maximal_pow line 274
  23. lemma OAI.PrimeDegreePackets.product_dvr_principal_eq line 283
  24. lemma OAI.PrimeDegreePackets.cardQuot_pi_restrictScalars line 293
  25. lemma OAI.PrimeDegreePackets.cardQuot_product_dvr_powers line 309
  26. def OAI.PrimeDegreePackets.integralCompletedIdeal line 323
  27. lemma OAI.PrimeDegreePackets.integralCompletedIdeal_eq_span line 328
  28. lemma OAI.PrimeDegreePackets.map_principal_restrictScalars line 350
  29. def OAI.PrimeDegreePackets.integralIdealValuations line 361
  30. lemma OAI.PrimeDegreePackets.integralCompletedIdeal_model line 367
  31. lemma OAI.PrimeDegreePackets.integralCompletedIdeal_cardQuot line 378
  32. def OAI.PrimeDegreePackets.nonzeroIntegralIdealUnit line 397
  33. lemma OAI.PrimeDegreePackets.nonzeroIntegralIdealUnit_le_one line 401
  34. lemma OAI.PrimeDegreePackets.integralIdeal_subgroup_map line 406
  35. lemma OAI.PrimeDegreePackets.fullLattice_ideal_relIndex line 413
  36. lemma OAI.PrimeDegreePackets.absNorm_smul_integral line 426
  37. lemma OAI.PrimeDegreePackets.completed_ideal_primePower_mem line 434
  38. lemma OAI.PrimeDegreePackets.completed_ideal_eq_off line 447
  39. lemma OAI.PrimeDegreePackets.integralCompletedIdeal_relIndex line 456
  40. theorem OAI.PrimeDegreePackets.integralIdeal_norm_eq_valuation_product line 463
  41. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_eq_of_integralCompletedIdeal_eq line 491
  42. lemma OAI.PrimeDegreePackets.integralIdeal_completions_eq_of_valuations_eq line 512
  43. def OAI.PrimeDegreePackets.primaryIntegralIdeals line 525
  44. def OAI.PrimeDegreePackets.primaryIdealValuations line 528
  45. theorem OAI.PrimeDegreePackets.primaryIdealValuations_injective line 536
  46. lemma OAI.PrimeDegreePackets.localIdealWeight_eq_of_completion_eq line 553
  47. lemma OAI.PrimeDegreePackets.primaryIdeal_actual_weight line 563
  48. lemma OAI.PrimeDegreePackets.primaryIdeal_actual_norm line 575
  49. theorem OAI.PrimeDegreePackets.primaryIdeal_reciprocal_sum_le line 591
  50. theorem OAI.PrimeDegreePackets.primaryIdeal_moment_le line 605