OAI/Analysis/IrrationalRotation/Sampling/CharacterSamplingTests.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.CharacterSampling.fract_sub_fract line 14
  2. theorem OAI.Invariant233.CharacterSampling.kernel_fract_right line 20
  3. lemma OAI.Invariant233.CharacterSampling.measurable_representative line 30
  4. lemma OAI.Invariant233.CharacterSampling.continuousAt_representative line 33
  5. lemma OAI.Invariant233.CharacterSampling.measurable_kernel line 37
  6. lemma OAI.Invariant233.CharacterSampling.kernel_nonneg line 44
  7. lemma OAI.Invariant233.CharacterSampling.kernel_le_height line 50
  8. lemma OAI.Invariant233.CharacterSampling.kernel_abs_le_height line 54
  9. theorem OAI.Invariant233.CharacterSampling.ae_joint_continuousAt_kernel line 59
  10. lemma OAI.Invariant233.CharacterSampling.measurable_squaredError line 85
  11. theorem OAI.Invariant233.CharacterSampling.ae_continuousAt_coordinateFactor line 98
  12. theorem OAI.Invariant233.CharacterSampling.ae_continuousAt_squaredError line 117
  13. lemma OAI.Invariant233.CharacterSampling.average_nonneg line 137
  14. lemma OAI.Invariant233.CharacterSampling.average_le_height line 145
  15. theorem OAI.Invariant233.CharacterSampling.squaredError_abs_le line 172
  16. theorem OAI.Invariant233.CharacterSampling.tendsto_integral_squaredError line 184
  17. theorem OAI.Invariant233.CharacterSampling.integrable_squaredError_comp line 201
  18. theorem OAI.Invariant233.CharacterSampling.lintegral_squaredError_eq line 211