OAI/Combinatorics/Progressions/Estimates/WeightedRudin.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RelativeChangSanders.IsWeightedDissociated.mono_K line 16
2. theorem OAI.Erdos3.RelativeChangSanders.IsWeightedDissociated.mono_subset line 23
3. theorem OAI.Erdos3.RelativeChangSanders.exp_weightedAverage_le_weightedAverage_exp line 47
4. theorem OAI.Erdos3.RelativeChangSanders.weighted_rudin_exp_ineq line 56