OAI/NumberTheory/SiegelZeros/Structure/ArithmeticCutoffTransport.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.W19.support_iteratedInvariant_subset line 25
  2. theorem OAI.SiegelZeros.WeightedTorusJets.W19.support_mixedInvariant_subset line 35
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant_totalDegree_le line 42
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W19.inBox_mixedInvariant line 47
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W19.totalDegree_le_of_inBox line 58
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant_totalDegree_le_of_inBox line 69
  7. theorem OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant_totalDegree_lt_of_inBox line 79
  8. def OAI.SiegelZeros.WeightedTorusJets.W28.boundedDerivativePolynomial line 107
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W28.derivativeIdeal_eq_map_boundedDerivative line 112
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W28.source_vanishing_on_four_truncations line 128
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W28.original_hyperplane_basis_independent line 151
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actual_positive_component_length_lower line 157
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actual_component_length_lower line 183
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W28.derivative_component_height_bounds line 207
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W28.exists_actual_component_with_length_lower line 229
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actual_derivative_component_length_upper line 255
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actual_rectangularAssertion_of_localBezout line 277
  18. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actual_cutoff_spanning_of_localBezout line 296
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actual_selected_determinant_of_localBezout line 306
  20. def OAI.SiegelZeros.SiegelZerosAwei.W50.boxEnumeration line 333
  21. def OAI.SiegelZeros.SiegelZerosAwei.W50.boxExponents line 336
  22. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.boxExponents_injective line 339
  23. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.boxExponents_lt line 342
  24. def OAI.SiegelZeros.SiegelZerosAwei.W50.sourceCutoff line 347
  25. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.sourceCutoff_le line 350
  26. def OAI.SiegelZeros.SiegelZerosAwei.W50.ActualCutoffSpanning line 356
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W28.rowSpan_top_of_field_map line 382
  28. theorem OAI.SiegelZeros.WeightedTorusJets.W28.rowSpan_top_reindex line 401
  29. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actual_omega_independent line 414
  30. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actual_complex_cutoff_spanning line 429
  31. theorem OAI.SiegelZeros.WeightedTorusJets.W28.map_theta_eigenvalue line 449
  32. theorem OAI.SiegelZeros.WeightedTorusJets.W28.arithmeticRow_map_eq_sourceRow line 456
  33. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actualCutoffSpanning_of_localBezout line 488