OAI/Probability/RadialTransition/CellDifferences.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.if_zero_sub line 16
2. lemma OAI.RadialTransition.pairWithin_sub line 20
3. lemma OAI.RadialTransition.pairBetween_sub line 28
4. lemma OAI.RadialTransition.pairWithin_abs_bound line 33
5. lemma OAI.RadialTransition.pairBetween_abs_bound line 54
6. lemma OAI.RadialTransition.double_sum_diagonal line 66
7. lemma OAI.RadialTransition.pairCellEnergy_sub line 79
8. lemma OAI.RadialTransition.pairCellEnergy_abs_bound line 85
9. lemma OAI.RadialTransition.pairCellEnergy_abs_difference line 117
10. lemma OAI.RadialTransition.pairCell_quadratic_bound line 128
11. lemma OAI.RadialTransition.cell_boltzmann_integrable line 147
12. lemma OAI.RadialTransition.cell_exponential_integrable line 156
13. lemma OAI.RadialTransition.pairCell_second_moment line 177
14. theorem OAI.RadialTransition.pairCell_log_perturbation line 210