OAI/MathematicalPhysics/Boltzmann/Approximation/RegularizedLogBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An integrable logarithmic majorant for positive regularized densities

  1. theorem OAI.BoltzmannNonuniqueness.abs_log_le_power_add_lower line 15
  2. def OAI.BoltzmannNonuniqueness.logarithmicMajorant line 24
  3. theorem OAI.BoltzmannNonuniqueness.logarithmicMajorant_integrable line 28
  4. theorem OAI.BoltzmannNonuniqueness.logarithm_weight_bound line 39
  5. theorem OAI.BoltzmannNonuniqueness.integrable_logarithm_weight line 87