OAI/Analysis/IrrationalRotation/Sampling/ScalarSamplingEndpointVariation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.ScalarSampling.variation_add_le line 9
2. lemma OAI.Invariant233.ScalarSampling.variation_mul_le line 22
3. lemma OAI.Invariant233.ScalarSampling.monotone_variation_le_height line 54
4. lemma OAI.Invariant233.ScalarSampling.antitone_variation_le_height line 64
5. structure OAI.Invariant233.ScalarSampling.VariationControl line 71
6. lemma OAI.Invariant233.ScalarSampling.variation_step_le line 76
7. lemma OAI.Invariant233.ScalarSampling.VariationControl.mask line 96
8. lemma OAI.Invariant233.ScalarSampling.clipped_reciprocal_control line 122
9. def OAI.Invariant233.ScalarSampling.leftEndpointPiece line 140
10. def OAI.Invariant233.ScalarSampling.rightEndpointPiece line 144
11. lemma OAI.Invariant233.ScalarSampling.leftEndpointPiece_control line 148
12. lemma OAI.Invariant233.ScalarSampling.rightEndpointPiece_control line 165
13. lemma OAI.Invariant233.ScalarSampling.rawEndpoint_eq_pieces line 183
14. theorem OAI.Invariant233.ScalarSampling.rawEndpoint_variation_le line 208
15. theorem OAI.Invariant233.ScalarSampling.endpoint_no_wrap_on_unit line 226
16. lemma OAI.Invariant233.ScalarSampling.circleEndpoint_fract line 266
17. theorem OAI.Invariant233.ScalarSampling.circleEndpoint_variation_le line 272
18. theorem OAI.Invariant233.ScalarSampling.manuscriptEndpointKernel_variation_le line 285
19. theorem OAI.Invariant233.ScalarSampling.manuscriptEndpointKernel_sup_le line 293
20. theorem OAI.Invariant233.ScalarSampling.manuscriptEndpointKernel_BV_bound line 305
21. theorem OAI.Invariant233.ScalarSampling.manuscriptEndpointKernel_BV_bound_ten line 317