OAI/Analysis/CoulombIonization/FieldAnalysis/ConditionalFieldIdentity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.coreCoulombAt_mass_zero line 18
  2. lemma OAI.CoulombAtom.normalizedCoreField_mul_mass line 34
  3. lemma OAI.CoulombAtom.coreSlice_mass_div line 43
  4. lemma OAI.CoulombAtom.coreSlice_mass_div_integrable line 49
  5. lemma OAI.CoulombAtom.coreSlice_cross_integrable line 60
  6. lemma OAI.CoulombAtom.integral_coreSlice_mass_div line 76
  7. lemma OAI.CoulombAtom.integral_coreSlice_cross line 100
  8. def OAI.CoulombAtom.conditionalFieldSum line 134
  9. lemma OAI.CoulombAtom.conditionalFieldSum_ae line 139
  10. lemma OAI.CoulombAtom.conditionalFieldSum_integrable line 154
  11. lemma OAI.CoulombAtom.integral_conditionalFieldSum line 162
  12. theorem OAI.CoulombAtom.priced_conditional_energy_identity line 182
  13. theorem OAI.CoulombAtom.fresh_cut_priced_localization_identity line 200