OAI/Analysis/VlasovMaxwell/Population/DyadicBalanceConstant.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RVM.dyadicBalanceConstant line 37
2. lemma OAI.RVM.dyadicBalanceConstant_pos line 40
3. lemma OAI.RVM.dyadic_power_min_summable line 49
4. lemma OAI.RVM.truncated_dyadic_crossing line 62
5. lemma OAI.RVM.crossing_normalisation line 92
6. lemma OAI.RVM.truncated_crossing_normalised line 107
7. lemma OAI.RVM.angular_crossing_sum line 136
8. lemma OAI.RVM.two_level_crossing_sum line 157