OAI/Analysis/IrrationalRotation/Sampling/ScalarSamplingTestVariation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.ScalarSampling.circleKernel_control line 10
  2. lemma OAI.Invariant233.ScalarSampling.circleEndpoint_control line 19
  3. lemma OAI.Invariant233.ScalarSampling.rawKernel_support_of_ne_zero line 29
  4. lemma OAI.Invariant233.ScalarSampling.circleKernel_target_no_wrap line 41
  5. lemma OAI.Invariant233.ScalarSampling.circleEndpoint_source_no_wrap line 55
  6. lemma OAI.Invariant233.ScalarSampling.mul_two_tests_bounds line 65
  7. theorem OAI.Invariant233.ScalarSampling.tested_circleKernel_control line 71
  8. theorem OAI.Invariant233.ScalarSampling.tested_circleEndpoint_control line 108
  9. theorem OAI.Invariant233.ScalarSampling.tested_circleKernel_BV_bound line 145
  10. theorem OAI.Invariant233.ScalarSampling.tested_circleEndpoint_BV_bound line 156
  11. theorem OAI.Invariant233.ScalarSampling.tested_manuscriptKernel_BV_bound line 167
  12. theorem OAI.Invariant233.ScalarSampling.tested_manuscriptEndpointKernel_BV_bound line 178
  13. theorem OAI.Invariant233.ScalarSampling.tested_manuscript_oriented_BV_bound_ten line 189