OAI/Combinatorics/Progressions/Linear/ActualFixedSpatialSlicedRetainedKernelComparison.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.recoveredG line 48
2. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.rawTarget_eq_recoveredG line 61
3. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.targetAt_eq_recoveredG line 84
4. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredG line 158
5. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedForecastOutput_reduce line 172
6. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.recoveredRationalFactor line 186
7. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredRationalFactor line 195
8. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRationalBudget line 257
9. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRationalCap line 262
10. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredRationalFactor_nonneg line 281
11. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredRationalFactor_le_exp_of_modulus line 290
12. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredRationalFactor_abs_le_exp_of_modulus line 305
13. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredRationalFactor_le_exp line 318
14. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredRationalFactor_abs_le_cap line 334
15. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredG_eq_centered line 345
16. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRational_abs_le_layered line 355
17. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredG_mem_Icc line 361
18. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredG_lift_lipschitz line 373
19. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredG_spatial_lipschitz line 389
20. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredG_recovered_invariant line 402
21. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.retainedRecoveredRationalFactor_eq_reference line 482
22. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.recoveredRationalFactor_retained_comparison line 494
23. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.mul_relative_bounds line 511
24. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.recoveredG_retained_comparison line 522
25. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.recoveredG_retained_abs_sub_le line 537
26. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.recoveredG_retained_comparison_scaled line 554