OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateKeptSymbolFactors.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.mark_log_on_slice line 42
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.chart_mark_degreeLE line 57
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.formal_mark line 65
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.formal_mark_group line 76
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.degree_lt_slice_length_of_dense line 123
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.degree_lt_slice_length line 144
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.exists_marked_chart_symbol_factors line 154
  8. theorem OAI.Erdos3.VectorPolynomial.adaptedChart_eq_of_chart_eq line 218
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.withKeep_chart_integerChart line 259
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.withKeep_chart_recovered line 269
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_withKeep_marked_frozen_symbol_factors line 275