OAI/Probability/RadialTransition/CanonicalCosts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.coreLift line 12
  2. theorem OAI.RadialTransition.continuous_coreLift line 14
  3. theorem OAI.RadialTransition.coreLift_nonneg line 17
  4. theorem OAI.RadialTransition.coreLift_bound line 19
  5. theorem OAI.RadialTransition.coreLift_compactSupport line 23
  6. theorem OAI.RadialTransition.integrable_coreLift line 33
  7. def OAI.RadialTransition.coreIntegral line 36
  8. theorem OAI.RadialTransition.coreIntegral_nonneg line 38
  9. theorem OAI.RadialTransition.familyPotential_le_core line 40
  10. theorem OAI.RadialTransition.probability_energy_family_upper line 45
  11. theorem OAI.RadialTransition.log_factorial_bounds line 58
  12. def OAI.RadialTransition.densityAt line 73
  13. theorem OAI.RadialTransition.finiteCanonical_bounds line 75