OAI/Analysis/IrrationalRotation/Sampling/ScalarSamplingContinuity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.ScalarSampling.continuousAt_ite_lt_of_ne line 11
2. lemma OAI.Invariant233.ScalarSampling.continuousAt_ite_le_of_ne line 23
3. theorem OAI.Invariant233.ScalarSampling.continuousAt_rawKernel_pair line 35
4. theorem OAI.Invariant233.ScalarSampling.continuousAt_circleKernel_pair line 54
5. theorem OAI.Invariant233.ScalarSampling.continuousAt_circleEndpoint_pair line 77
6. lemma OAI.Invariant233.ScalarSampling.ae_fract_sub_ne line 86
7. lemma OAI.Invariant233.ScalarSampling.ae_delta_fract_sub_ne line 98
8. theorem OAI.Invariant233.ScalarSampling.ae_joint_continuousAt_circleKernel line 110
9. theorem OAI.Invariant233.ScalarSampling.ae_joint_continuousAt_circleEndpoint line 123
10. theorem OAI.Invariant233.ScalarSampling.ae_joint_continuousAt_manuscriptPower line 135
11. theorem OAI.Invariant233.ScalarSampling.ae_joint_continuousAt_manuscriptEndpointPower line 145