OAI/Combinatorics/Progressions/Estimates/NativeMeanRowCorrelation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_large_nonnegative_weighted_term line 11
2. theorem OAI.Erdos3.mean_row_weighted_sum_norm_le line 30
3. theorem OAI.Erdos3.exists_mean_row_weighted_term line 39
4. theorem OAI.Erdos3.NativeIntegerExpansion.select_mean_row_correlation line 53
5. theorem OAI.Erdos3.mean_row_correlation_scale line 83
6. theorem OAI.Erdos3.exists_large_value_of_mean_row_correlation line 97
7. structure OAI.Erdos3.NativeMeanRowCorrelation line 125
8. def OAI.Erdos3.NativeMeanRowCorrelation.mono line 152
9. theorem OAI.Erdos3.NativeMeanRowCorrelation.exists_of_expansion line 158