OAI/Combinatorics/Progressions/Estimates/AllocatedRecenteredL1Source.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.finiteWeightedComplex_norm_sq_le line 11
2. theorem OAI.Erdos3.finiteSource_real_le_of_square_perturbation line 21
3. theorem OAI.Erdos3.BooleanCubeKernel.physicalReconstruction_weighted_sampled_error line 70
4. theorem OAI.Erdos3.BooleanCubeKernel.physicalReconstruction_source_of_sampled_square line 103
5. theorem OAI.Erdos3.BooleanCubeKernel.physicalReconstruction_source_of_sampled_square_geometric line 133
6. theorem OAI.Erdos3.BooleanCubeKernel.physicalReconstruction_source_of_sampled_l1_and_uniform line 198
7. theorem OAI.Erdos3.BooleanCubeKernel.physicalReconstruction_source_of_haar_l1_surrogate line 295
8. theorem OAI.Erdos3.BooleanCubeKernel.exists_translated_physical_jet_l1_perturbation line 342
9. theorem OAI.Erdos3.BooleanCubeKernel.exists_physical_rows_l1_source line 422
10. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredSelectedMean_l1_source line 557