OAI/MathematicalPhysics/Boltzmann/Branching/VaryingBoundedMultiplier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted Fatou for entropy production with convergent kernel multipliers

  1. theorem OAI.BoltzmannNonuniqueness.lintegral_varying_production_le_liminf line 14
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.tendsto_L1_bounded_mul_zero line 54