OAI/Combinatorics/Progressions/Estimates/AllocatedZeroLayerFixedCenterExcess.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.integerBox_nonempty line 38
  2. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.NativeDetection line 44
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.NativeDetection.mono_tests line 67
  4. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.PolynomialGeometry line 78
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_fixedCenter_forecast_model line 117
  6. theorem OAI.Erdos3.positiveProjectionAccuracy_le_of_le line 204
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.NativeDetection.forecast_of_exp_threshold line 235
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.fixedCenter_excess_max_one_of_precision line 254
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.fixedCenter_forecast_source_bounds line 270
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.fixedCenter_excess_zero_layers line 331
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.fixedCenter_excess_zero_layers_of_spatial_cutoff line 368
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.fixedCenter_excess_zero_layers_le line 384