OAI/Analysis/CoulombRadii/FieldAnalysis/RetainedFineDensity.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.retainedFineDensity line 120
  2. lemma OAI.Coulomb.retainedFineDensity_nonneg line 123
  3. lemma OAI.Coulomb.retainedFineDensity_le line 127
  4. lemma OAI.Coulomb.retainedFineDensity_integrable line 132
  5. lemma OAI.Coulomb.retainedFineDensity_measurable line 136
  6. lemma OAI.Coulomb.retainedFineDensity_integral line 140
  7. lemma OAI.Coulomb.retainedFineDensity_coulomb_expansion line 148
  8. lemma OAI.Coulomb.coulombKernel_sub_symm line 165
  9. theorem OAI.Coulomb.retained_fine_pair_lower line 169
  10. lemma OAI.Coulomb.ae_position_injective line 224
  11. lemma OAI.Coulomb.ae_retained_fine_pair_lower line 248
  12. lemma OAI.Coulomb.retainedFineDensity_eq_sum_ite line 257
  13. lemma OAI.Coulomb.fineDensity_power_integrable line 262
  14. lemma OAI.Coulomb.retainedFineDensity_power_integrable line 270
  15. lemma OAI.Coulomb.retainedFineDensity_power_le line 279
  16. lemma OAI.Coulomb.retainedFineDensity_power_configuration_measurable line 285
  17. lemma OAI.Coulomb.retainedFineDensity_power_weight_integrable line 298
  18. theorem OAI.Coulomb.retained_fine_kinetic_lower line 310