OAI/Combinatorics/Progressions/Estimates/NativeCoveredCommonFactorization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitEval_zero_iff_coefficient_zero line 15
  2. theorem OAI.Erdos3.toAdd_hom_corrected_factor line 31
  3. theorem OAI.Erdos3.exists_native_dependent_orbit_factorization line 46
  4. theorem OAI.Erdos3.VectorPolynomial.CoefficientBound.add line 146
  5. theorem OAI.Erdos3.VectorPolynomial.CoefficientGrid.add line 153
  6. theorem OAI.Erdos3.toAdd_hom_corrected_reference line 168
  7. theorem OAI.Erdos3.sub_corrected_reference_add_errors line 175
  8. theorem OAI.Erdos3.exists_native_periodic_factorization_budget line 191
  9. theorem OAI.Erdos3.exists_native_periodic_dependent_factorization line 213
  10. theorem OAI.Erdos3.exists_common_reference_correction_budget line 320
  11. theorem OAI.Erdos3.exists_native_common_dependent_factorization line 342
  12. theorem OAI.Erdos3.exists_native_periodic_common_factorization line 521
  13. theorem OAI.Erdos3.exists_frozen_common_factorization_budget line 638
  14. theorem OAI.Erdos3.exists_native_frozen_common_factorization line 660
  15. theorem OAI.Erdos3.exists_native_covered_common_factorization line 765