OAI/Analysis/CoulombRadii/FieldAnalysis/GeometricRecursion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.square_recursion_bounded line 13
2. lemma OAI.Coulomb.normalized_square_step line 32
3. theorem OAI.Coulomb.geometric_screening_recursion line 44
4. theorem OAI.Coulomb.geometric_screening_recursion_all line 66
5. theorem OAI.Coulomb.deterministic_screening_tree line 89
6. theorem OAI.Coulomb.atomicRawSup_uniform line 107
7. theorem OAI.Coulomb.AtomicCutHistory.positive_field line 125
8. theorem OAI.Coulomb.AtomicCutHistory.positive_field_actual_counts line 142