OAI/Analysis/IrrationalRotation/Sampling/CircleSamplingGraphLimits.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.CircleParameterData.circleFiniteBase line 14
  2. instance OAI.Invariant233.CircleParameterData.circleFiniteBase_probability line 17
  3. def OAI.Invariant233.CircleParameterData.samplingGraphFinite line 22
  4. theorem OAI.Invariant233.CircleParameterLaws.samplingAverage_error_tendsto_zero line 34
  5. theorem OAI.Invariant233.CircleParameterLaws.tendsto_samplingGraph_first_marginal line 48
  6. theorem OAI.Invariant233.CircleParameterLaws.tendsto_samplingGraph_second_marginal line 65
  7. theorem OAI.Invariant233.CircleParameterLaws.samplingGraph_marginals_uniformlyAbsolutelyContinuous line 82
  8. theorem OAI.Invariant233.CircleParameterLaws.ell_nonneg_and_le line 112
  9. theorem OAI.Invariant233.CircleParameterLaws.tendsto_ell_zero line 127
  10. theorem OAI.Invariant233.CircleParameterLaws.samplingGraphAverage_ae_dist_lt line 135
  11. theorem OAI.Invariant233.CircleParameterLaws.tendsto_samplingGraph_translation line 155
  12. theorem OAI.Invariant233.CircleParameterLaws.tendsto_samplingGraph_translation_trimmed line 170