OAI/NumberTheory/Jacobsthal/Siegel/RectangleThreshold.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangleThreshold line 17
  2. lemma OAI.Erdos970.WeightedTorusJets.Geometry.rectangleThreshold_pos line 20
  3. lemma OAI.Erdos970.WeightedTorusJets.Geometry.short_side_lower line 25
  4. lemma OAI.Erdos970.WeightedTorusJets.Geometry.short_side_le_threshold line 38
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangle_floor_product_gt_short_power line 48
  6. lemma OAI.Erdos970.WeightedTorusJets.Geometry.rectangleThreshold_product line 59
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangle_floor_product_gt line 74
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangle_floor_product_gt_nat line 107
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangle_jet_cutoff line 116
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangle_cutoff_lower line 126
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangle_cutoff_ge_nine line 137
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_mixed_derivatives_algebraMap line 153
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_rectangleJetIdeal_le_identity line 166
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_rectangle_has_shared_minimal_prime line 189
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_rectangle_shared_component_data line 208
  16. def OAI.Erdos970.WeightedTorusJets.Geometry.coefficientDerivationLinear line 244
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficientDerivationLinear_monomial line 250
  18. def OAI.Erdos970.WeightedTorusJets.Geometry.coefficientDerivation line 260
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficientDerivation_coeff line 281
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficientDerivation_monomial line 285
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficientDerivation_C line 291
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficientDerivation_X line 295
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivation_mem_span_of_vanishes line 299
  24. def OAI.Erdos970.WeightedTorusJets.Geometry.quotientDerivation line 311
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotientDerivation_mk line 318
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotientDerivation_pow_mk line 325
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficientDerivation_pow_monomial line 335
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficientDerivation_mem_rectangularIdeal line 345
  29. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularCoefficientDerivation line 353
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_mk line 360
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_X line 366
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_pow_monomial line 372
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularVariable_pow_eq_zero line 381
  34. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularMap line 390
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularMap_mk line 403
  36. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularMap_monomial line 407
  37. def OAI.Erdos970.WeightedTorusJets.Geometry.nilpotentDerivationExp line 421
  38. theorem OAI.Erdos970.WeightedTorusJets.Geometry.nilpotentDerivationExp_apply line 437
  39. theorem OAI.Erdos970.WeightedTorusJets.Geometry.scaledDerivation_pow_apply line 443
  40. theorem OAI.Erdos970.WeightedTorusJets.Geometry.scaledDerivation_pow_eq_zero line 454
  41. def OAI.Erdos970.WeightedTorusJets.Geometry.truncatedTaylor line 461
  42. theorem OAI.Erdos970.WeightedTorusJets.Geometry.truncatedTaylor_apply line 465
  43. theorem OAI.Erdos970.WeightedTorusJets.Geometry.map_truncatedTaylor line 473
  44. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorAlong line 494
  45. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorAlong_monomial line 503
  46. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularCoefficientDerivation_zero line 516
  47. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorAlong_zero line 527
  48. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree line 532
  49. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree_apply line 541
  50. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree_two_apply line 557
  51. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree_one_apply line 571
  52. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularTaylorThree_residue line 583