OAI/Analysis/CoulombRadii/Propagation/PropagationRegularity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NeutralAtom.propagationCoreSource_measurable line 12
  2. lemma OAI.NeutralAtom.propagationStepError_measurable line 17
  3. lemma OAI.NeutralAtom.propagationCoreSource_abs_bound line 27
  4. lemma OAI.NeutralAtom.propagationStepError_abs_bound line 37
  5. lemma OAI.NeutralAtom.propagationCoreSource_ball_bounds line 46
  6. lemma OAI.NeutralAtom.propagationStepError_ball_bounds line 55
  7. lemma OAI.NeutralAtom.propagationRHS_locallyIntegrable line 64
  8. theorem OAI.NeutralAtom.WeakNuclearSubsolution.radialMaxSplice line 84
  9. structure OAI.NeutralAtom.PropagationStepHypotheses line 134
  10. lemma OAI.NeutralAtom.PropagationStepHypotheses.R_pos line 175
  11. lemma OAI.NeutralAtom.PropagationStepHypotheses.L_pos line 176
  12. lemma OAI.NeutralAtom.PropagationStepHypotheses.old_le_new line 177
  13. lemma OAI.NeutralAtom.PropagationStepHypotheses.next_continuous line 179
  14. lemma OAI.NeutralAtom.PropagationStepHypotheses.step_error_measurable line 183
  15. lemma OAI.NeutralAtom.PropagationStepHypotheses.step_error_bounds line 185
  16. lemma OAI.NeutralAtom.PropagationStepHypotheses.finite_step line 189