OAI/Analysis/CoulombRadii/FormDomain/ExplicitMultiplyGradient.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.energy_localization_identity line 13
  2. theorem OAI.NeutralAtom.groundState_localization line 33
  3. theorem OAI.NeutralAtom.localizationError_nonneg line 46
  4. theorem OAI.NeutralAtom.localizationError_le line 52
  5. theorem OAI.NeutralAtom.groundState_normalized_localization line 77
  6. theorem OAI.NeutralAtom.tendsto_integral_bounded_real_smul line 103
  7. theorem OAI.NeutralAtom.tendsto_integral_two_bounded_real_smul line 122
  8. def OAI.NeutralAtom.explicitMultiplyGradient line 152
  9. theorem OAI.NeutralAtom.HasWeakGradient.multiply_limit line 157
  10. theorem OAI.NeutralAtom.memLp_bounded_measurable_real_smul line 199
  11. theorem OAI.NeutralAtom.FormDomain.multiply_limit line 210
  12. def OAI.NeutralAtom.explicitLocalizationError line 243
  13. theorem OAI.NeutralAtom.energy_localization_explicit line 248
  14. def OAI.NeutralAtom.observationNoiseBase line 285
  15. theorem OAI.NeutralAtom.observationNoiseBase_contDiff line 287
  16. theorem OAI.NeutralAtom.observationNoiseBase_nonneg line 290
  17. theorem OAI.NeutralAtom.observationNoiseBase_formula line 293
  18. theorem OAI.NeutralAtom.observationNoiseBase_compact line 307
  19. theorem OAI.NeutralAtom.observationNoiseBase_integrable line 314
  20. theorem OAI.NeutralAtom.observationNoiseBase_integral_pos line 318
  21. def OAI.NeutralAtom.observationNoiseNormalizer line 324
  22. def OAI.NeutralAtom.observationNoiseDensity line 326
  23. theorem OAI.NeutralAtom.observationNoiseDensity_nonneg line 328
  24. theorem OAI.NeutralAtom.observationNoiseDensity_contDiff line 332
  25. theorem OAI.NeutralAtom.observationNoiseDensity_integrable line 335
  26. theorem OAI.NeutralAtom.observationNoiseDensity_mass line 338
  27. def OAI.NeutralAtom.observationNoiseLaw line 343
  28. instance OAI.NeutralAtom.observationNoiseLaw_probability line 346
  29. theorem OAI.NeutralAtom.observationNoiseDensity_formula line 353
  30. def OAI.NeutralAtom.observationTranslationScore line 358
  31. theorem OAI.NeutralAtom.observationTranslationScore_measurable line 360
  32. theorem OAI.NeutralAtom.observationNoiseDensity_even line 364
  33. theorem OAI.NeutralAtom.observationTranslationScore_odd line 368
  34. theorem OAI.NeutralAtom.observationNoiseDensity_hasDerivAt line 372
  35. theorem OAI.NeutralAtom.pow_mul_exp_neg_le_factorial line 386
  36. theorem OAI.NeutralAtom.observationScore_weighted_pow_bound line 393