OAI/Analysis/CoulombRadii/FieldAnalysis/WeakDirectionalUnique.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Coulomb.weak_directional_uniqueline 62 - lemma
OAI.Coulomb.weak_directional_zero_on_openline 73 - lemma
OAI.Coulomb.smooth_compact_weak_directionalline 92 - lemma
OAI.Coulomb.weak_directional_eq_smoothline 119 - lemma
OAI.Coulomb.weak_directional_smooth_norm_sqline 135