OAI/Probability/SKValue/Variation/ContactVariations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValue.OrderParameter.zero line 12
  2. def OAI.SKValue.OrderParameter.add line 19
  3. def OAI.SKValue.OrderParameter.atom line 26
  4. def OAI.SKValue.OrderParameter.removeBelow line 48
  5. lemma OAI.SKValue.OrderParameter.removeBelow_sub line 55
  6. def OAI.SKValue.contactPotential line 72
  7. lemma OAI.SKValue.IsDiffusion.moment_difference_integrable line 76
  8. lemma OAI.SKValue.integral_atom_mul line 88
  9. lemma OAI.SKValue.IsMinimizer.contactPotential_nonneg line 105
  10. lemma OAI.SKValue.IsDiffusion.contactPotential_continuous line 112
  11. lemma OAI.SKValue.IsDiffusion.contactPotential_hasDerivAt line 124
  12. lemma OAI.SKValue.IsMinimizer.moment_eq_at_contact line 141