OAI/Analysis/HardSphere/Geometry/InnerClmRealRight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.L2Multiplier.inner_clm_real_right line 19
2. lemma OAI.L2Multiplier.clm_comm line 25
3. lemma OAI.HardSphere.SmoothMultiplier.partial_real line 35
4. def OAI.HardSphere.SmoothMultiplier.derivativeScalar line 41
5. lemma OAI.HardSphere.SmoothMultiplier.onJet_fst line 45
6. lemma OAI.HardSphere.SmoothMultiplier.onJet_snd line 48
7. lemma OAI.HardSphere.SmoothMultiplier.inner_onScalar_right line 52
8. lemma OAI.HardSphere.SmoothMultiplier.inner_derivativeScalar_right line 57
9. lemma OAI.HardSphere.SmoothMultiplier.onScalar_derivativeScalar_comm line 63
10. theorem OAI.HardSphere.IsGroundVector.smooth_multiplier_identity line 68