OAI/Analysis/CoulombRadii/Packets/NormalizedBandModulus.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NeutralAtom.norm_pow_difference_bound line 15
2. lemma OAI.NeutralAtom.normalized_density_difference line 26
3. lemma OAI.NeutralAtom.normalized_field_difference line 50
4. lemma OAI.NeutralAtom.mesh_width_ratio_formula line 118
5. lemma OAI.NeutralAtom.mesh_width_power_tendsto line 126
6. lemma OAI.NeutralAtom.mesh_normalized_density_bound line 141
7. lemma OAI.NeutralAtom.inverse_count_ball_subset line 162