OAI/Combinatorics/Progressions/Probability/SelectedDensityNormalizedTwistRoot.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.coefficientCoverTiltedConstant line 8
  2. theorem OAI.Erdos3.VectorPolynomial.coefficientCoverTiltedConstant_ge_two line 11
  3. theorem OAI.Erdos3.VectorPolynomial.exists_selected_density_ambient_cover_tilted_comparison line 30
  4. theorem OAI.Erdos3.selectedResidueDensityPMF_approximation line 145
  5. def OAI.Erdos3.VectorPolynomial.normalizedPhysicalRootRadius line 167
  6. theorem OAI.Erdos3.VectorPolynomial.normalizedPhysicalRootRadius_nonneg line 171
  7. theorem OAI.Erdos3.VectorPolynomial.normalized_integerPhysicalSite_norm_le line 175
  8. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.selected_density_eval_sub_frozenSpatialEval_root line 197
  9. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.selected_density_eval_sub_frozenSpatialEval_root_zero line 222
  10. theorem OAI.Erdos3.VectorPolynomial.exists_selected_density_normalizedTwist_root_comparison line 264
  11. theorem OAI.Erdos3.VectorPolynomial.exists_selected_density_normalizedTwist_eval_comparison line 350