OAI/Combinatorics/Progressions/Sampling/PreparedConcreteSlicedForecastPrecision.lean

GitHub source file

4 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 statement text; different proof or body), OAI/Combinatorics/Progressions/Sampling/PreparedConcreteSlicedForecastModelLogs.lean:11 (same statement text; different proof or body), OAI/Combinatorics/Progressions/Sampling/PreparedSlicedForecastComparisonLogs.lean:212 (same statement text; different proof or body). Qualify references as OAI.Erdos3.VectorPolynomial.and_rec_projection@path.

2. theorem OAI.Erdos3.VectorPolynomial.preparedActualSlicedForecastSetup_scalar_values line 30
3. theorem OAI.Erdos3.VectorPolynomial.preparedActualSlicedForecastModelPrecision line 92
4. theorem OAI.Erdos3.VectorPolynomial.preparedConcreteSlicedForecastPrecision line 181