OAI/Probability/SKValue/Equations/ShiftedPairing.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.abs_sum_mul_le_of_sq_bounds line 18
2. lemma OAI.SKValue.sum_fin_castSucc_sq_le line 27
3. lemma OAI.SKValue.sum_fin_succ_sq_le line 32
4. lemma OAI.SKValue.pointwise_le_sqrt_sum_sq line 37
5. def OAI.SKValue.shiftedPairing line 44
6. lemma OAI.SKValue.shiftedPairing_error line 47
7. lemma OAI.SKValue.shiftedPairing_tendsto_error_zero line 93
8. lemma OAI.SKValue.integral_sq_le_integral_sq line 118
9. lemma OAI.SKValue.integral_abs_le_sqrt_integral_sq line 125
10. lemma OAI.SKValue.square_difference_bound line 135
11. lemma OAI.SKValue.second_moment_perturbation line 145
12. lemma OAI.SKValue.uniform_moment_positive line 168
13. lemma OAI.SKValue.uniform_normalizer_convergence line 176
14. lemma OAI.SKValue.uniform_inverse_normalizer_convergence line 190