OAI/Analysis/RotationWeights/FiniteSampling.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleSampling.continuousAt_repr line 47
  2. lemma OAI.CircleSampling.continuous_delta line 49
  3. lemma OAI.CircleSampling.repr_pos line 50
  4. lemma OAI.CircleSampling.continuousAt_weight line 57
  5. lemma OAI.CircleSampling.ae_repr_ne line 93
  6. lemma OAI.CircleSampling.ae_delta_ne line 99
  7. lemma OAI.CircleSampling.ae_continuousAt_uPos line 106
  8. lemma OAI.CircleSampling.ae_continuousAt_uNeg line 123
  9. lemma OAI.CircleSampling.ae_continuousAt_orientedWeight line 136
  10. lemma OAI.CircleSampling.ae_continuousAt_idealAverage line 144
  11. lemma OAI.CircleSampling.squared_ideal_test_bound line 166
  12. lemma OAI.CircleSampling.ideal_sampling_tendsto line 175
  13. lemma OAI.CircleSampling.finite_accuracy_of_sequential line 214
  14. abbrev OAI.CircleSampling.PhaseCube line 246
  15. lemma OAI.CircleSampling.sampling_finite_accuracy line 247
  16. lemma OAI.CircleSampling.closed_interval_in_open line 267
  17. lemma OAI.CircleSampling.fractional_interval line 276
  18. lemma OAI.CircleSampling.divisible_frequency_interval line 312
  19. lemma OAI.CircleSampling.finite_frequency_realization line 332
  20. def OAI.CircleSampling.fractionalCube line 370
  21. lemma OAI.CircleSampling.realize_phase_neighborhood line 373
  22. lemma OAI.CircleSampling.realize_finite_sampling line 407