OAI/Combinatorics/Progressions/Estimates/CommonInducedCorrelation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.inducedMarkedLipschitzBound line 12
2. theorem OAI.Erdos3.exists_induced_marked_observable_explicit line 18
3. theorem OAI.Erdos3.induced_marked_observable_scaled_parameter line 103
4. theorem OAI.Erdos3.NativeRankRelation.CommonData.localPhaseMarkedOrbit_induced_value line 147
5. theorem OAI.Erdos3.NativeRankRelation.CommonData.induced_local_value_eq_nativeSpaceMap line 256
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_local_induced_comparison_correlation line 292