OAI/MathematicalPhysics/Boltzmann/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nonuniqueness for the periodic hard-sphere Boltzmann equation

The exact main statement includes two distinct global renormalized solutions of one bounded-velocity initial datum, with local mass conservation, total momentum conservation, energy and entropy-dissipation inequalities, and strong early L1 continuity with integrable collisions.

  1. theorem OAI.BoltzmannNonuniqueness.nonuniqueness line 13

    Distinct definitions of this name: ComparatorChallenges/BoltzmannNonuniqueness.lean:204 (same statement text; different proof or body). Qualify references as OAI.BoltzmannNonuniqueness.nonuniqueness@path.