OAI/Analysis/CoulombRadii/Propagation/InitializationBranch.lean
17 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.NeutralAtom.initialPropagationOffsetline 13 - def
OAI.NeutralAtom.initialPropagationErrorline 16 - lemma
OAI.NeutralAtom.initialPropagationOffset_continuousline 19 - lemma
OAI.NeutralAtom.initialPropagationError_nonnegline 28 - lemma
OAI.NeutralAtom.initialPropagationError_supportline 35 - lemma
OAI.NeutralAtom.initialPropagationError_measurableline 39 - lemma
OAI.NeutralAtom.initialPropagationError_ball_boundsline 48 - lemma
OAI.NeutralAtom.initial_core_sourceline 59 - lemma
OAI.NeutralAtom.initialPropagationOffset_base_weakline 66 - lemma
OAI.NeutralAtom.initialPropagationOffset_upperline 91 - lemma
OAI.NeutralAtom.initialPropagationOffset_weakline 107 - lemma
OAI.NeutralAtom.initialPropagationOffset_lowerline 153 - lemma
OAI.NeutralAtom.initialPropagationOffset_nonposline 175 - lemma
OAI.NeutralAtom.initialPropagationOffset_low_overlapline 192 - lemma
OAI.NeutralAtom.initialPropagationOffset_high_overlapline 210 - def
OAI.NeutralAtom.initialNextOffsetline 220 - lemma
OAI.NeutralAtom.initialNextOffset_continuousline 224