OAI/NumberTheory/SiegelZeros/Structure/SelectedComponentTaylor.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.W23.actual_residue_rat_smul line 17
  2. def OAI.SiegelZeros.W23.rationalTorusDerivation line 22
  3. theorem OAI.SiegelZeros.W23.rationalTorusDerivation_commute line 26
  4. theorem OAI.SiegelZeros.W23.rationalTorusDerivation_polynomial line 36
  5. theorem OAI.SiegelZeros.W23.iter_rationalTorus_polynomial line 42
  6. theorem OAI.SiegelZeros.W23.derivativeTriple_torus_polynomial line 51
  7. theorem OAI.SiegelZeros.W23.torus_rectangleGenerators_eq_image line 59
  8. theorem OAI.SiegelZeros.W23.derivativeIdeal_eq_torus_rectangle_span line 73
  9. theorem OAI.SiegelZeros.W23.localRectangleIdeal_eq_derivativeIdeal_map line 81
  10. theorem OAI.SiegelZeros.W23.component_next_rectangle_mem_maximal line 92
  11. abbrev OAI.SiegelZeros.W23.componentDerivation line 108
  12. def OAI.SiegelZeros.W23.componentJet line 113
  13. theorem OAI.SiegelZeros.W23.localized_derivativeIdeal_le_componentJet_ker line 121
  14. def OAI.SiegelZeros.W23.componentTaylor line 143
  15. theorem OAI.SiegelZeros.W23.componentTaylor_mk line 154
  16. def OAI.SiegelZeros.W23.componentFormalSeries line 159
  17. theorem OAI.SiegelZeros.W23.componentFormalSeries_coeff line 166
  18. theorem OAI.SiegelZeros.W23.componentTaylor_mk_eq_projection line 178
  19. theorem OAI.SiegelZeros.W23.exists_componentTaylor_of_rectangle_vanishing line 185
  20. theorem OAI.SiegelZeros.W23.componentDerivation_eq_localTorus_restrict line 237
  21. theorem OAI.SiegelZeros.W23.componentJet_ker_mono_cutoff line 250
  22. theorem OAI.SiegelZeros.W23.localized_derivativeIdeal_le_smaller_componentJet_ker line 266
  23. def OAI.SiegelZeros.W23.smallerComponentTaylor line 275
  24. theorem OAI.SiegelZeros.W23.smallerComponentTaylor_mk line 286
  25. theorem OAI.SiegelZeros.W23.smallerComponentTaylor_mk_eq_projection line 294
  26. theorem OAI.SiegelZeros.W23.smallerComponentTaylor_coeff line 302
  27. theorem OAI.SiegelZeros.W23.smallerComponentTaylor_residue line 316
  28. def OAI.SiegelZeros.W23.selectedCutoffs line 328
  29. theorem OAI.SiegelZeros.W23.selectedCutoffs_of_mem line 332
  30. theorem OAI.SiegelZeros.W23.selectedCutoffs_of_not_mem line 337
  31. theorem OAI.SiegelZeros.W23.selectedCutoffs_le line 342
  32. theorem OAI.SiegelZeros.W23.selectedCutoffs_multiindex_iff line 349
  33. def OAI.SiegelZeros.W23.selectedComponentTaylor line 363
  34. theorem OAI.SiegelZeros.W23.selectedComponentTaylor_mk line 369
  35. theorem OAI.SiegelZeros.W23.selectedComponentTaylor_mk_eq_projection line 376