OAI/Probability/SKGap/Terminal/PairCrossLower.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.abs_pair_ps_coefficient line 11
2. lemma OAI.SKGap.abs_pair_mixed_coefficient line 26
3. lemma OAI.SKGap.mul_lower_from_abs line 42
4. lemma OAI.SKGap.pairCrossPolynomial_lower line 48
5. lemma OAI.SKGap.pair_young_cost line 59
6. lemma OAI.SKGap.pair_signed_cross_lower line 68
7. lemma OAI.SKGap.pair_energy_lower line 97
8. lemma OAI.SKGap.pairInterMean_swap line 125
9. lemma OAI.SKGap.pair_second_energy_lower line 136
10. lemma OAI.SKGap.pairInterMean_add line 144
11. lemma OAI.SKGap.pairInterMean_nonneg line 150
12. lemma OAI.SKGap.pair_signed_bound line 157