OAI/Combinatorics/BalancedRyser/Probability/PatternMarginals.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.PatternMarginals.weighted_lintegral_le_of_marginal_bound line 10
2. theorem OAI.Balanced.PatternMarginals.lintegral_moment_le_pow_of_marginal_bound line 41
3. theorem OAI.Balanced.PatternMarginals.integral_moment_le_pow_of_marginal_bound line 112
4. theorem OAI.Balanced.PatternMarginals.weighted_integral_le_of_marginal_bound line 151