OAI/Analysis/CoulombRadii/RandomFields/ObservationSmallScale.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NeutralAtom.tendsto_positive_rpow_zero line 14
2. def OAI.NeutralAtom.singleObservationOffset line 19
3. lemma OAI.NeutralAtom.singleObservationOffset_scaled_tendsto line 22
4. lemma OAI.NeutralAtom.screenMass_small_offset line 49
5. lemma OAI.NeutralAtom.observation_displacement_ratio_tendsto line 68