OAI/Analysis/CoulombRadii/Localization/SmoothMultiplier.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.NeutralAtom.SmoothMultiplier line 13
  2. def OAI.NeutralAtom.multiplyWavefunction line 20
  3. def OAI.NeutralAtom.multiplyGradient line 23
  4. theorem OAI.NeutralAtom.memLp_bounded_real_smul line 27
  5. theorem OAI.NeutralAtom.integrable_test_real_smul line 37
  6. theorem OAI.NeutralAtom.IsAntisymmetric.multiply line 42
  7. theorem OAI.NeutralAtom.HasWeakGradient.multiply line 50
  8. theorem OAI.NeutralAtom.norm_multiplyWavefunction_sq line 88
  9. theorem OAI.NeutralAtom.integrable_weight_multiply line 93
  10. theorem OAI.NeutralAtom.FormDomain.multiply line 109
  11. theorem OAI.NeutralAtom.SmoothMultiplier.const line 127
  12. theorem OAI.NeutralAtom.SmoothMultiplier.add line 133
  13. theorem OAI.NeutralAtom.SmoothMultiplier.mul line 149
  14. def OAI.NeutralAtom.scaleWavefunction line 173
  15. def OAI.NeutralAtom.scaleGradient line 176
  16. theorem OAI.NeutralAtom.FormDomain.scale line 179
  17. theorem OAI.NeutralAtom.normSquared_scale line 189
  18. theorem OAI.NeutralAtom.energy_scale line 194
  19. theorem OAI.NeutralAtom.normSquared_nonneg line 202
  20. theorem OAI.NeutralAtom.ae_normSquared_eq_zero line 205
  21. theorem OAI.NeutralAtom.energy_nonneg_of_normSquared_zero line 213
  22. theorem OAI.NeutralAtom.rayleigh_lower_bound line 227
  23. theorem OAI.NeutralAtom.integrable_real_inner_of_memLp line 252
  24. theorem OAI.NeutralAtom.FormDomain.integrable_potential line 263
  25. theorem OAI.NeutralAtom.integrable_bounded_mul line 274
  26. theorem OAI.NeutralAtom.integral_affine_multiplier_sq line 281
  27. theorem OAI.NeutralAtom.integral_norm_add_smul_sq line 296
  28. def OAI.NeutralAtom.stateWeightedIntegral line 312
  29. def OAI.NeutralAtom.formMultiplierPairing line 315
  30. theorem OAI.NeutralAtom.multiplyGradient_affine line 321
  31. theorem OAI.NeutralAtom.normSquared_affine_multiplier line 332
  32. theorem OAI.NeutralAtom.energy_affine_multiplier line 340
  33. theorem OAI.NeutralAtom.minimizer_multiplier_pairing line 360
  34. def OAI.NeutralAtom.localizationError line 387
  35. theorem OAI.NeutralAtom.norm_multiplyGradient_sq line 391
  36. theorem OAI.NeutralAtom.integrable_localization_error line 411