OAI/Combinatorics/Progressions/Probability/AllocatedNormalizedConditionalHaar.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedGridlessProfile_window_mass line 48
2. def OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedCoveredProfile line 114
3. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedCoveredProfile_grid_multiplier line 125
4. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedCoveredProfile_conditional_mean line 142
5. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedGridlessProfile_window_integral_mass line 238
6. theorem OAI.Erdos3.VectorPolynomial.allocatedConditionalWindow_mass line 337
7. theorem OAI.Erdos3.VectorPolynomial.allocatedConditionalProfile_haar_error line 345
8. theorem OAI.Erdos3.VectorPolynomial.allocatedConditionalProfile_selected_haar_error line 467
9. theorem OAI.Erdos3.VectorPolynomial.allocatedConditionalProfile_natural_haar_error line 508
10. theorem OAI.Erdos3.VectorPolynomial.allocatedConditionalProfile_budgeted_haar_error line 541