OAI/Analysis/RotationWeights/RationalGraphs.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CircleModel.upperExceptional line 61
2. def OAI.CircleModel.lowerExceptional line 63
3. lemma OAI.CircleModel.measurableSet_upperExceptional line 65
4. lemma OAI.CircleModel.measurableSet_lowerExceptional line 67
5. lemma OAI.CircleModel.measure_Xi_upper line 69
6. lemma OAI.CircleModel.measure_Xi_lower line 74
7. lemma OAI.CircleModel.measure_upperExceptional line 79
8. lemma OAI.CircleModel.measure_lowerExceptional line 88
9. lemma OAI.CircleSampling.graphTolerance_pos line 105
10. lemma OAI.CircleSampling.oldGraphBad_bound line 109
11. lemma OAI.CircleSampling.measure_iUnion_le_ofReal_tsum line 135
12. lemma OAI.CircleSampling.tailGraphBad_subset line 143
13. lemma OAI.CircleSampling.tailGraphBad_bound line 162
14. lemma OAI.CircleSampling.sampleBound_div_window line 190
15. lemma OAI.CircleSampling.graphBad_bound line 204
16. lemma OAI.CircleSampling.graphBad_tendsto line 212
17. lemma OAI.CircleSampling.frequency_dvd_of_le line 224
18. lemma OAI.CircleSampling.circle_nat_zero line 228
19. lemma OAI.CircleSampling.rational_annihilated line 230
20. lemma OAI.CircleSampling.rational_grid_lift line 238
21. lemma OAI.CircleSampling.rational_stage_index line 246
22. lemma OAI.CircleSampling.rational_tail_period line 254
23. lemma OAI.CircleSampling.integral_norm_le_sqrt line 264
24. lemma OAI.CircleSampling.setIntegral_norm_le_sqrt line 272
25. lemma OAI.CircleSampling.setIntegral_nonneg_le_sqrt line 293
26. lemma OAI.CircleSampling.integral_sq_le_of_error line 299
27. lemma OAI.CircleSampling.weightedMeasure_le_sqrt line 326
28. lemma OAI.CircleSampling.finiteMeasure_sqrt_uc line 335
29. lemma OAI.CircleSampling.weightedMeasure_l1_test line 361
30. lemma OAI.CircleSampling.weightedMeasure_test_restrict line 385
31. lemma OAI.CircleSampling.tendsto_integral_graph_error line 406
32. lemma OAI.CircleSampling.tendsto_graph_of_fst line 433