OAI/Combinatorics/Progressions/Linear/AllocatedKernelSiteReferenceData.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedKernelSiteParameter line 10
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteParameter_bounds line 13
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteParameter_mono line 22
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteParameter_refined_budget line 29
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteSourceLog_mono line 42
  6. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedKernelSiteSourceLog_bound line 65
  7. def OAI.Erdos3.VectorPolynomial.allocatedKernelSiteScale line 101
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteScale_cutoff line 104
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteScale_upper line 120
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteScale_affine_bad_probability line 137
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteScale_refined_window_size line 185
  12. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedKernelSiteScale_refined_residue_data line 228