OAI/Analysis/CoulombIonization/Localization/CoreHistoryOutMaximumBarrier.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.conditionalBlockMaximum line 17
  2. lemma OAI.CoulombAtom.conditionalBlockMaximum_nonneg line 22
  3. lemma OAI.CoulombAtom.conditionalBlockMaximum_aemeasurable line 29
  4. lemma OAI.CoulombAtom.conditionalBlockMaximum_next_join line 50
  5. lemma OAI.CoulombAtom.radial_nextBlockMaximum_bound line 60
  6. lemma OAI.CoulombAtom.radial_nextBlockMaximum_square_integrable line 70
  7. lemma OAI.CoulombAtom.nextBlockMaximum_square_fubini line 85
  8. lemma OAI.CoulombAtom.nextBlockMaximum_square_statistic_integrable line 108
  9. lemma OAI.CoulombAtom.ball_one_integrable line 126
  10. lemma OAI.CoulombAtom.ball_indicator_nuclear_separation line 134
  11. lemma OAI.CoulombAtom.fieldSquare_ball_weight_eq line 145
  12. lemma OAI.CoulombAtom.coreFieldSquare_ball_statistic_integrable line 155
  13. lemma OAI.CoulombAtom.coreFieldSquare_ball_fubini line 165
  14. lemma OAI.CoulombAtom.coreLawAverage_fieldSquare_ball_integrable line 180
  15. lemma OAI.CoulombAtom.radial_out_position_distance line 198
  16. theorem OAI.CoulombAtom.radial_nextBlockMaximum_sq_spatial line 207
  17. theorem OAI.CoulombAtom.radial_nextBlockMaximum_moment_spatial line 250
  18. def OAI.CoulombAtom.CoreObservationGraph.outMoment line 279
  19. lemma OAI.CoulombAtom.CoreObservationGraph.outMoment_nonneg line 287
  20. lemma OAI.CoulombAtom.CoreObservationGraph.outMoment_spatial line 292