OAI/Geometry/RCD/Sobolev/LogSumExpIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two-term log-sum-exp inequality under a probability measure

  1. theorem OAI.RegularPointCoordinates.log_sum_exp_support line 12
  2. theorem OAI.RegularPointCoordinates.log_sum_exp_integral line 38