OAI/NumberTheory/PrimePackets/HaarBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PrimeDegreePackets.haar_kernel_eq_inv_card line 18
  2. theorem OAI.PrimeDegreePackets.haar_kernel_le_inv_addOrderOf line 31
  3. theorem OAI.PrimeDegreePackets.haar_zero_fiber_le_of_order line 44
  4. lemma OAI.PrimeDegreePackets.mem_maximalIdeal_pow_iff_addVal line 60
  5. lemma OAI.PrimeDegreePackets.addVal_scalar_unit_mul_pow line 69
  6. theorem OAI.PrimeDegreePackets.scalar_preimage_maximalIdeal_pow line 82
  7. lemma OAI.PrimeDegreePackets.natCast_mem_maximalIdeal_pow_iff line 102
  8. theorem OAI.PrimeDegreePackets.addOrderOf_quotient_unit line 116
  9. lemma OAI.PrimeDegreePackets.exists_unit_of_span_eq_top line 134
  10. theorem OAI.PrimeDegreePackets.haar_dvr_projection_tail line 154
  11. theorem OAI.PrimeDegreePackets.haar_natVal_projection_tail line 185
  12. lemma OAI.PrimeDegreePackets.measurableSet_dvr_tail line 211
  13. lemma OAI.PrimeDegreePackets.measurable_dvr_val line 219
  14. lemma OAI.PrimeDegreePackets.measurable_dvr_natVal line 233
  15. theorem OAI.PrimeDegreePackets.haar_dvr_zero_fiber line 241
  16. theorem OAI.PrimeDegreePackets.lintegral_pow_le_of_nat_tail line 275
  17. theorem OAI.PrimeDegreePackets.sqrt_geometric_factor_le line 302
  18. theorem OAI.PrimeDegreePackets.local_sqrt_moment line 325
  19. def OAI.PrimeDegreePackets.ramifiedMaximum line 352
  20. lemma OAI.PrimeDegreePackets.ramifiedMaximum_measurable line 355
  21. lemma OAI.PrimeDegreePackets.ceilDiv_ramification_succ line 361
  22. theorem OAI.PrimeDegreePackets.ramifiedMaximum_tail line 370
  23. theorem OAI.PrimeDegreePackets.normExponent_le_degree_mul_maximum line 403
  24. lemma OAI.PrimeDegreePackets.card_le_localDegree line 416
  25. theorem OAI.PrimeDegreePackets.local_norm_moment_of_valuation_tails line 428