OAI/Analysis/CoulombRadii/Variational/SignAverage.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.observationScore_weighted_pow_integrable line 14
  2. theorem OAI.NeutralAtom.observationNoise_integral line 29
  3. theorem OAI.NeutralAtom.observationScore_pow_integrable line 37
  4. theorem OAI.NeutralAtom.observationScore_moment_le_factorial line 45
  5. theorem OAI.NeutralAtom.observationScore_moment_le_pow line 59
  6. def OAI.NeutralAtom.signAverage line 87
  7. def OAI.NeutralAtom.boolSign line 90
  8. theorem OAI.NeutralAtom.signAverage_const line 92
  9. theorem OAI.NeutralAtom.signAverage_nonneg line 99
  10. theorem OAI.NeutralAtom.signAverage_mono line 104
  11. theorem OAI.NeutralAtom.signAverage_add line 109
  12. theorem OAI.NeutralAtom.signAverage_const_mul line 114
  13. theorem OAI.NeutralAtom.signAverage_prod line 119
  14. theorem OAI.NeutralAtom.signAverage_exp_sum line 129
  15. theorem OAI.NeutralAtom.even_pow_le_factorial_exp line 152
  16. theorem OAI.NeutralAtom.signAverage_scaled_even_pow_le line 163
  17. theorem OAI.NeutralAtom.signAverage_even_pow_le_of_exp line 186
  18. theorem OAI.NeutralAtom.signAverage_sum_even_pow line 217
  19. instance OAI.NeutralAtom.observationNoiseLaw_negInvariant line 233
  20. theorem OAI.NeutralAtom.observationNoisePi_sign_preserving line 249
  21. theorem OAI.NeutralAtom.observationScore_memLp line 264
  22. theorem OAI.NeutralAtom.observationScorePi_sum_memLp line 271
  23. theorem OAI.NeutralAtom.observationScorePi_sum_pow_integrable line 281
  24. theorem OAI.NeutralAtom.weighted_sum_pow_le line 288
  25. theorem OAI.NeutralAtom.observationScore_sign line 319
  26. theorem OAI.NeutralAtom.observationScorePi_signed_moment line 324
  27. theorem OAI.NeutralAtom.integral_signAverage line 342
  28. theorem OAI.NeutralAtom.observationScorePi_moment_le line 351