OAI/Analysis/CoulombIonization/FieldAnalysis/InnerCapStatistic.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.innerFieldVolume line 15
  2. lemma OAI.CoulombAtom.innerFieldVolume_nonneg line 16
  3. lemma OAI.CoulombAtom.positiveCoreField_annular_sq_integrable line 18
  4. lemma OAI.CoulombAtom.positiveCoreField_annular_cauchy line 29
  5. def OAI.CoulombAtom.innerCapStatistic line 51
  6. lemma OAI.CoulombAtom.innerCapStatistic_nonneg line 56
  7. theorem OAI.CoulombAtom.actualInnerBoundaryCap_sq_le_statistic line 66
  8. theorem OAI.CoulombAtom.actual_inner_exterior_sq_statistic line 92
  9. def OAI.CoulombAtom.innerFieldAnnulusWeight line 115
  10. lemma OAI.CoulombAtom.innerFieldAnnulusWeight_integrable line 117
  11. lemma OAI.CoulombAtom.innerFieldAnnulusWeight_nonneg line 120
  12. lemma OAI.CoulombAtom.innerFieldAnnulusWeight_separation line 122
  13. lemma OAI.CoulombAtom.innerFieldAnnulus_weight_eq line 126
  14. lemma OAI.CoulombAtom.coreFieldSquare_annular_statistic_integrable line 132
  15. lemma OAI.CoulombAtom.coreFieldSquare_annular_fubini line 141
  16. lemma OAI.CoulombAtom.innerCapStatistic_coreSlice_integrable line 151
  17. def OAI.CoulombAtom.CoreObservationGraph.innerCapAverage line 163
  18. lemma OAI.CoulombAtom.CoreObservationGraph.fieldMoment_annular_integrable line 166
  19. lemma OAI.CoulombAtom.CoreObservationGraph.innerCapAverage_eq line 175
  20. def OAI.CoulombAtom.CoreObservationEnsemble.innerCapAverage line 211
  21. lemma OAI.CoulombAtom.CoreObservationEnsemble.fieldMoment_annular_integrable line 214
  22. lemma OAI.CoulombAtom.CoreObservationEnsemble.innerCapAverage_eq line 219
  23. lemma OAI.CoulombAtom.CoreObservationEnsemble.innerCapAverage_bound line 231