OAI/Probability/RadialTransition/BoundedCore.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.clamp01 line 14
  2. theorem OAI.RadialTransition.clamp01_nonneg line 16
  3. theorem OAI.RadialTransition.clamp01_le_one line 17
  4. theorem OAI.RadialTransition.clamp01_eq_zero line 19
  5. theorem OAI.RadialTransition.clamp01_eq_one line 21
  6. theorem OAI.RadialTransition.clamp01_mono line 23
  7. theorem OAI.RadialTransition.continuous_clamp01 line 26
  8. def OAI.RadialTransition.microLength line 30
  9. def OAI.RadialTransition.shellStep line 31
  10. def OAI.RadialTransition.coreReal line 33
  11. def OAI.RadialTransition.corePotential line 39
  12. theorem OAI.RadialTransition.microLength_pos line 41
  13. theorem OAI.RadialTransition.shellStep_pos line 42
  14. theorem OAI.RadialTransition.coreReal_nonneg line 44
  15. theorem OAI.RadialTransition.coreReal_le line 51
  16. theorem OAI.RadialTransition.continuous_coreReal line 59
  17. theorem OAI.RadialTransition.continuous_corePotential line 69
  18. theorem OAI.RadialTransition.bounded_corePotential line 72
  19. theorem OAI.RadialTransition.coreReal_zero_plateau line 78
  20. theorem OAI.RadialTransition.coreReal_zero_outer line 89
  21. theorem OAI.RadialTransition.coreReal_full_left line 102
  22. theorem OAI.RadialTransition.coreReal_full_right line 113
  23. theorem OAI.RadialTransition.coreReal_full_of_not_shell line 125
  24. theorem OAI.RadialTransition.twice_pair_sum line 136
  25. theorem OAI.RadialTransition.sum_adj_indicator line 166
  26. theorem OAI.RadialTransition.core_energy_lower_small_diameter line 176