OAI/Combinatorics/Progressions/Estimates/CoveredQuotientCorrelation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.controlledPullback line 30
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.controlledPullback_frequency line 48
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.controlledPullback_observable_mk line 52
4. theorem OAI.Erdos3.exists_native_free_evaluation line 68
5. theorem OAI.Erdos3.exists_native_free_unit_observable line 152
6. def OAI.Erdos3.RationalFilteredNilmanifold.mapDifferenceObservable line 253
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.mapDifferenceObservable_reconstruct line 256
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_lower_rank_map_difference line 262
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_quotient_comparison_correlation line 338
10. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_quotient_comparison_correlation line 388
11. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.onSublattice_native_correlation line 421