OAI/Combinatorics/Progressions/Estimates/ObservedTruncationResidual.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.productConditionalMean_truncation_eq line 14
2. theorem OAI.Erdos3.productConditionalMean_lowDegreeTruncation line 26
3. theorem OAI.Erdos3.productTruncation_fiber_pairing line 33
4. theorem OAI.Erdos3.observed_truncation_square_error line 67
5. theorem OAI.Erdos3.observed_truncation_residual_square line 79
6. theorem OAI.Erdos3.observed_truncation_local_test_error line 104
7. theorem OAI.Erdos3.observed_truncation_atom_error line 155