OAI/Analysis/RotationWeights/MaskedEstimates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContinuousCircleWeight.endpoint_mask_integral_le line 84
2. theorem OAI.ContinuousCircleWeight.endpoint_masked_squares line 96
3. theorem OAI.ContinuousCircleWeight.masked_product_integral_le line 121
4. theorem OAI.ContinuousCircleWeight.retained_sum_enorm_le line 169
5. theorem OAI.ContinuousCircleWeight.convolution_cut_bound line 183
6. theorem OAI.ContinuousCircleWeight.two_endpoint_error_bound line 196