OAI/Combinatorics/Progressions/Sampling/PreparedConcreteSlicedForecastModelLogs.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.and_rec_projection line 11

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

  2. def OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastCapLog line 16
  3. def OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastPeriodLog line 21
  4. def OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastTailSiteLog line 30
  5. def OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastOutputLog line 39
  6. def OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastNativeLog line 55
  7. def OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastMassLog line 70
  8. theorem OAI.Erdos3.VectorPolynomial.preparedActualSlicedForecastSetup_scalar_values_extended line 96
  9. theorem OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastEarlyLogs line 128
  10. theorem OAI.Erdos3.VectorPolynomial.exists_preparedConcreteSlicedForecastCapLog_budget line 220
  11. def OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastCapExponent line 353
  12. theorem OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastCapExponent_two_le line 357
  13. theorem OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastCapLog_le_work line 362
  14. theorem OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastLateLogs line 412
  15. theorem OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastModelLogs line 493