OAI/Combinatorics/Progressions/Estimates/FiniteEvenMomentTransfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.finiteWeightedLp_le_of_nat_moment line 13
2. theorem OAI.Erdos3.FiniteProbabilityWeights.even_moment_lp_le line 22
3. theorem OAI.Erdos3.finiteWeightedLp_le_of_moment_error line 43
4. theorem OAI.Erdos3.finiteWeightedLp_transfer_even line 63