OAI/Analysis/IrrationalRotation/Sampling/CircleSamplingGraph.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.CircleParameterData.measurable_samplingDensity line 17
  2. theorem OAI.Invariant233.CircleParameterData.samplingDensity_nonneg line 25
  3. theorem OAI.Invariant233.CircleParameterData.samplingTranslation_measurable line 30
  4. theorem OAI.Invariant233.CircleParameterData.samplingTranslation_measurePreserving line 34
  5. theorem OAI.Invariant233.CircleParameterData.coordinate_sub_samplingTranslation line 40
  6. theorem OAI.Invariant233.CircleParameterData.kernel_fract_first line 50
  7. theorem OAI.Invariant233.CircleParameterData.fract_sub_fract_right line 55
  8. theorem OAI.Invariant233.CircleParameterData.samplingDensity_inverse_translation line 62
  9. theorem OAI.Invariant233.CircleParameterData.samplingGraph_first_marginal line 74
  10. theorem OAI.Invariant233.CircleParameterData.samplingGraph_second_marginal line 81
  11. theorem OAI.Invariant233.CircleParameterData.samplingGraphAverage_first_marginal line 98
  12. theorem OAI.Invariant233.CircleParameterData.samplingGraphAverage_second_marginal line 112
  13. theorem OAI.Invariant233.CircleParameterData.samplingGraphAverage_finite line 126
  14. theorem OAI.Invariant233.CircleParameterData.samplingGraph_ae_graph line 140
  15. theorem OAI.Invariant233.CircleParameterData.samplingGraph_ae_positive_density line 150
  16. theorem OAI.Invariant233.CircleParameterData.samplingGraphAverage_ae_graph line 163
  17. theorem OAI.Invariant233.CircleParameterData.samplingGraphAverage_ae_positive_density_graph line 173
  18. theorem OAI.Invariant233.CircleParameterLaws.samplingAverage_eLpNorm_le_two line 192
  19. theorem OAI.Invariant233.CircleParameterLaws.samplingGraphAverage_ae_positive_graph line 224