OAI/NumberTheory/PowerFree/PairHilbert.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.normPair_finrank_of_exact line 7
  2. theorem OAI.QuarticPowerFree.normPair_filtered_principal_finrank line 16
  3. def OAI.QuarticPowerFree.homogeneousSpace line 54
  4. theorem OAI.QuarticPowerFree.mem_homogeneousSpace line 70
  5. theorem OAI.QuarticPowerFree.homogeneous_principal_finrank line 74
  6. theorem OAI.QuarticPowerFree.homogeneous_coord line 91
  7. theorem OAI.QuarticPowerFree.homogeneousSpace_eq_basis_span line 113
  8. theorem OAI.QuarticPowerFree.homogeneousSpace_finrank line 134
  9. theorem OAI.QuarticPowerFree.homogeneousSpace_finite line 151
  10. def OAI.QuarticPowerFree.normPair_simplexTuple line 169
  11. theorem OAI.QuarticPowerFree.normPair_mem_simplexTuple line 172
  12. theorem OAI.QuarticPowerFree.normPair_card_antidiagonalTuple line 181
  13. theorem OAI.QuarticPowerFree.normPair_card_simplexTuple line 200
  14. def OAI.QuarticPowerFree.weightedTuple line 212
  15. theorem OAI.QuarticPowerFree.mem_weightedTuple line 216
  16. def OAI.QuarticPowerFree.tupleQuot line 231
  17. def OAI.QuarticPowerFree.tupleRem line 233
  18. theorem OAI.QuarticPowerFree.tuple_divmod_injective line 235
  19. theorem OAI.QuarticPowerFree.weightedTuple_upper line 249
  20. theorem OAI.QuarticPowerFree.weightedTuple_lower line 277
  21. theorem OAI.QuarticPowerFree.simplexTuple_power_bounds line 325
  22. theorem OAI.QuarticPowerFree.prod_weight_comultiples line 334
  23. theorem OAI.QuarticPowerFree.weightedTuple_power_bounds line 341
  24. theorem OAI.QuarticPowerFree.nearby_power_error line 367
  25. theorem OAI.QuarticPowerFree.weightedTuple_volume_error_with_scale line 381
  26. theorem OAI.QuarticPowerFree.weightedTuple_volume_error line 445
  27. def OAI.QuarticPowerFree.shiftedTupleCount line 472
  28. theorem OAI.QuarticPowerFree.shiftedTuple_volume_error line 475
  29. def OAI.QuarticPowerFree.PairSector line 524
  30. instance OAI.QuarticPowerFree.(instance at line 526) line 526
  31. instance OAI.QuarticPowerFree.(instance at line 527) line 527
  32. def OAI.QuarticPowerFree.sectorPoint line 529
  33. theorem OAI.QuarticPowerFree.sectorPoint_normal line 534
  34. theorem OAI.QuarticPowerFree.sectorPoint_injective line 540
  35. theorem OAI.QuarticPowerFree.sectorPoint_surjective line 565
  36. def OAI.QuarticPowerFree.sectorWeight line 574
  37. def OAI.QuarticPowerFree.sectorShift line 579
  38. theorem OAI.QuarticPowerFree.sector_weight_identity line 584
  39. theorem OAI.QuarticPowerFree.sectorWeight_pos line 591
  40. def OAI.QuarticPowerFree.normalPairTuples line 595
  41. theorem OAI.QuarticPowerFree.mem_normalPairTuples line 601
  42. def OAI.QuarticPowerFree.sectorTuples line 619
  43. theorem OAI.QuarticPowerFree.mem_sectorTuples line 626
  44. theorem OAI.QuarticPowerFree.card_normalPairTuples line 638
  45. theorem OAI.QuarticPowerFree.normalPairTuples_volume_error line 669
  46. theorem OAI.QuarticPowerFree.sector_reciprocal_sum line 692
  47. theorem OAI.QuarticPowerFree.sector_coefficient line 698
  48. theorem OAI.QuarticPowerFree.normalPairTuples_hilbert_error line 730
  49. def OAI.QuarticPowerFree.ambientPairTuples line 741
  50. theorem OAI.QuarticPowerFree.mem_ambientPairTuples line 746
  51. def OAI.QuarticPowerFree.pairTranslate line 764
  52. theorem OAI.QuarticPowerFree.pairTranslate_weight line 768
  53. theorem OAI.QuarticPowerFree.pairTranslate_injective line 775
  54. theorem OAI.QuarticPowerFree.ambientPairTuples_card_cut line 785
  55. theorem OAI.QuarticPowerFree.pairFilteredDifference_hilbert_error line 850