OAI/Combinatorics/Progressions/Sampling/PreparedSlicedForecastComparisonLogs.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastPrimitiveCap line 10
  2. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastTailCap line 13
  3. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastTailLog line 16
  4. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastDensity line 19
  5. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastKernelLog line 22
  6. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastChildSize line 24
  7. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastPrimitiveCap_one_le line 27
  8. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastTailCap_primitive_le line 30
  9. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastTailCap_stride_le line 34
  10. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastTailCap_one_le line 37
  11. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastTailLog_nonneg line 42
  12. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastKernelLog_nonneg line 47
  13. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastDensity_pos line 52
  14. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastDensity_inv line 55
  15. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastTailCap_le_exp line 59
  16. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastChildSize_one_le line 79
  17. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastChildSize_pos line 82
  18. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastChildSize_lower line 86
  19. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastChildSize_upper line 90
  20. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastPrimitiveChoices line 94
  21. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastCommonFloorExponent line 125
  22. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastCommonFloor line 129
  23. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastCommonFloor_bounds line 134
  24. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastCommonFloorExponent_mono line 176
  25. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastCommonFloor_mono line 186
  26. theorem OAI.Erdos3.VectorPolynomial.preparedSlicedForecastCommonFloor_mono_comparison line 196
  27. theorem OAI.Erdos3.VectorPolynomial.and_rec_projection line 212

    Distinct definitions of this name: OAI/Combinatorics/Progressions/Sampling/PreparedActualSlicedForecastSetup.lean:527 (same declaration text), OAI/Combinatorics/Progressions/Sampling/PreparedConcreteSlicedForecastModelLogs.lean:11 (same declaration text), OAI/Combinatorics/Progressions/Sampling/PreparedConcreteSlicedForecastPrecision.lean:11 (same statement text; different proof or body). Qualify references as OAI.Erdos3.VectorPolynomial.and_rec_projection@path.

  28. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastSourceLog line 217
  29. theorem OAI.Erdos3.VectorPolynomial.preparedActualSlicedForecastSetup_comparison_logs line 235