OAI/Combinatorics/Progressions/Polynomial/OrdinaryPolynomialPhaseAffineInverse.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.OrdinaryPolynomialPhase.factorizationInputOffset line 11
  2. theorem OAI.Erdos3.OrdinaryPolynomialPhase.budget_le_factorizationInputOffset line 14
  3. theorem OAI.Erdos3.OrdinaryPolynomialPhase.le_factorizationInputBudget line 19
  4. theorem OAI.Erdos3.OrdinaryPolynomialPhase.factorizationInputBudget_nonneg line 23
  5. theorem OAI.Erdos3.OrdinaryPolynomialPhase.budget_le_factorizationInputBudget line 27
  6. theorem OAI.Erdos3.OrdinaryPolynomialPhase.factorizationInputBudget_le_power line 31
  7. theorem OAI.Erdos3.OrdinaryPolynomialPhase.exists_factorizationBudget line 43
  8. def OAI.Erdos3.OrdinaryPolynomialPhase.orbit line 65
  9. theorem OAI.Erdos3.OrdinaryPolynomialPhase.orbit_realEval line 74
  10. theorem OAI.Erdos3.OrdinaryPolynomialPhase.orbit_integerEval line 93
  11. theorem OAI.Erdos3.OrdinaryPolynomialPhase.orbit_buffered_eval line 101
  12. theorem OAI.Erdos3.OrdinaryPolynomialPhase.zero_base_orbit line 116
  13. theorem OAI.Erdos3.OrdinaryPolynomialPhase.orbit_eq_pure line 130
  14. theorem OAI.Erdos3.OrdinaryPolynomialPhase.orbit_log line 138
  15. theorem OAI.Erdos3.OrdinaryPolynomialPhase.phaseSlotCoefficient_rename line 147
  16. theorem OAI.Erdos3.OrdinaryPolynomialPhase.orbit_coordinate line 155
  17. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardDetectorOffset line 178
  18. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardDetectorPolynomial line 181
  19. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardDetectorOffset_phase line 184
  20. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardDetectorPolynomial_eval line 191
  21. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardDetectorPolynomial_bounds line 196
  22. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardDetectorPolynomial_stage_bounds line 215
  23. theorem OAI.Erdos3.OrdinaryPolynomialPhase.phasePair_finrank_le_of_geometry line 244
  24. theorem OAI.Erdos3.OrdinaryPolynomialPhase.phasePair_finrank_le line 271
  25. theorem OAI.Erdos3.OrdinaryPolynomialPhase.exists_polynomial_phase_factorization line 291
  26. theorem OAI.Erdos3.OrdinaryPolynomialPhase.orbit_symbol_constantCoefficient line 384
  27. theorem OAI.Erdos3.OrdinaryPolynomialPhase.pairOrbitSymbol_scalar_top line 405
  28. theorem OAI.Erdos3.OrdinaryPolynomialPhase.exists_ordinary_polynomial_phase_inverse line 458
  29. theorem OAI.Erdos3.OrdinaryPolynomialPhase.exists_ordinary_polynomial_phase_affine_inverse line 531