OAI/Analysis/IrrationalRotation/Sampling/TrimmedCircleSamplingGraph.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CircleParameterData.samplingDensity_false_eq_orbitGraphDensity line 12
2. theorem OAI.Invariant233.CircleParameterData.samplingGraphAverage_ae_fst line 18
3. theorem OAI.Invariant233.CircleParameterData.trimmedSamplingGraphAverage_finite line 26
4. theorem OAI.Invariant233.CircleParameterData.trimmedSamplingGraphAverage_ae_good line 33
5. theorem OAI.Invariant233.CircleParameterData.trimmedSamplingGraphAverage_ae_density_graph line 39
6. theorem OAI.Invariant233.CircleParameterLaws.trimmedSamplingGraphAverage_ae_ordered line 55
7. theorem OAI.Invariant233.CircleParameterLaws.trimmedSamplingGraphAverage_ae_ratio_cap line 68
8. theorem OAI.Invariant233.CircleParameterLaws.trimmedSamplingGraphAverage_ae_positive_graph line 85
9. theorem OAI.Invariant233.CircleParameterLaws.trimmedSamplingGraphAverage_ae_rational line 91