OAI/Geometry/RCD/Sobolev/LogSumExpIntegrable.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the logarithmic sum from its two logarithms

  1. theorem OAI.RegularPointCoordinates.log_sum_exp_abs_le line 11
  2. theorem OAI.RegularPointCoordinates.integrable_log_sum_exp line 31
  3. theorem OAI.RegularPointCoordinates.log_sum_exp_integral_le line 40