OAI/NumberTheory/SiegelZeros/Structure/RectangleThreshold.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleThreshold line 14
  2. lemma OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleThreshold_pos line 17
  3. lemma OAI.SiegelZeros.WeightedTorusJets.Geometry.short_side_lower line 22
  4. lemma OAI.SiegelZeros.WeightedTorusJets.Geometry.short_side_le_threshold line 35
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangle_floor_product_gt_short_power line 45
  6. lemma OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleThreshold_product line 56
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangle_floor_product_gt line 71
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangle_floor_product_gt_nat line 104
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangle_jet_cutoff line 113
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangle_cutoff_lower line 123
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangle_cutoff_ge_nine line 134
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_mixed_derivatives_algebraMap line 149
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_rectangleJetIdeal_le_identity line 162
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_rectangle_has_shared_minimal_prime line 185
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_rectangle_shared_component_data line 204
  16. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientDerivationLinear line 241
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientDerivationLinear_monomial line 247
  18. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientDerivation line 257
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientDerivation_coeff line 278
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientDerivation_monomial line 282
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientDerivation_C line 288
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientDerivation_X line 292
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivation_mem_span_of_vanishes line 296
  24. def OAI.SiegelZeros.WeightedTorusJets.Geometry.quotientDerivation line 308
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotientDerivation_mk line 315
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotientDerivation_pow_mk line 322
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientDerivation_pow_monomial line 332
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientDerivation_mem_rectangularIdeal line 342
  29. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularCoefficientDerivation line 350
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_mk line 357
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_X line 363
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_pow_monomial line 369
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularVariable_pow_eq_zero line 378
  34. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularMap line 387
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularMap_mk line 400
  36. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularMap_monomial line 404
  37. def OAI.SiegelZeros.WeightedTorusJets.Geometry.nilpotentDerivationExp line 418
  38. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.nilpotentDerivationExp_apply line 434
  39. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.scaledDerivation_pow_apply line 440
  40. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.scaledDerivation_pow_eq_zero line 451
  41. def OAI.SiegelZeros.WeightedTorusJets.Geometry.truncatedTaylor line 458
  42. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.truncatedTaylor_apply line 462
  43. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.map_truncatedTaylor line 470
  44. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorAlong line 491
  45. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorAlong_monomial line 500
  46. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_zero line 513
  47. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorAlong_zero line 524
  48. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree line 529
  49. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_apply line 538
  50. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_two_apply line 554
  51. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_one_apply line 568
  52. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_residue line 580