Admissibility.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

The entropy-class solution and nonuniqueness statement

The solution class follows Definition 2.1 with explicit integrability conditions. The renormalized equation uses derivatives of smooth periodic lifts, while integrals use volume on the unit torus and Euclidean velocity space.

abbrev OAI.BoltzmannNonuniqueness.Evolution line 23
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:52 (same declaration text).
abbrev OAI.BoltzmannNonuniqueness.SpaceTimePhase line 24
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:53 (same declaration text).
abbrev OAI.BoltzmannNonuniqueness.LiftedSpaceTimePhase line 25
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:54 (same declaration text).
def OAI.BoltzmannNonuniqueness.torusProjection line 27
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:56 (same declaration text).
def OAI.BoltzmannNonuniqueness.torusRepresentative line 31
Source documentation
A representative in the fundamental half-open unit cube, used only to evaluate periodic derivatives. Periodicity makes those derivatives independent of this choice.
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:60 (same declaration text).
```
def torusRepresentative (x : Position) : Velocity :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity
theorem OAI.BoltzmannNonuniqueness.torusProjection_representative line 34
def OAI.BoltzmannNonuniqueness.maxwellian line 39
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:63 (same declaration text).
theorem OAI.BoltzmannNonuniqueness.maxwellian_pos line 42
def OAI.BoltzmannNonuniqueness.entropyMoment line 46
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:66 (same declaration text).
def OAI.BoltzmannNonuniqueness.FiniteEntropyDatum line 50
Source documentation
The convention 0 |log 0| = 0 is automatic in this real-valued moment.
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:70 (same declaration text).
```
def FiniteEntropyDatum (f : Density) : Prop :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Density
def OAI.BoltzmannNonuniqueness.BoundedVelocitySupport line 53
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:73 (same declaration text).
def OAI.BoltzmannNonuniqueness.energy line 56
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:76 (same declaration text).
def OAI.BoltzmannNonuniqueness.momentum line 58
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:78 (same declaration text).
def OAI.BoltzmannNonuniqueness.relativeEntropy line 60
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:80 (same declaration text).
def OAI.BoltzmannNonuniqueness.extendedEntropyProduction line 65
Source documentation
Lower semicontinuous extension of (A-B) log(A/B) on the nonnegative quadrant. The off-quadrant value is immaterial for nonnegative densities.
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:85 (same declaration text).
```
def extendedEntropyProduction (A B : ℝ) : ℝ≥0∞ :=
…
```
def OAI.BoltzmannNonuniqueness.entropyDissipation line 70
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:90 (same declaration text).
structure OAI.BoltzmannNonuniqueness.Renormalization line 81
Source documentation
The renormalizations of Definition 2.1, with the right derivative at zero.
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:101 (same declaration text).
```
structure Renormalization where
…
```
structure OAI.BoltzmannNonuniqueness.KineticTest line 89
Source documentation
A smooth test, periodic in the spatial variable and compact in time and velocity.
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:109 (same declaration text).
```
structure KineticTest where
…
```
def OAI.BoltzmannNonuniqueness.KineticTest.transportDerivative line 96
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:116 (same declaration text).
structure OAI.BoltzmannNonuniqueness.MassTest line 102
Source documentation
Smooth local mass tests have no velocity cutoff, since their velocity dependence is introduced only by the transport derivative.
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:122 (same declaration text).
```
structure MassTest where
…
```
def OAI.BoltzmannNonuniqueness.MassTest.transportDerivative line 107
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:127 (same declaration text).
def OAI.BoltzmannNonuniqueness.relativeDensity line 111
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:131 (same declaration text).
def OAI.BoltzmannNonuniqueness.renormalizedIntegrand line 113
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:133 (same declaration text).
def OAI.BoltzmannNonuniqueness.nonnegativeTimes line 120
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:140 (same declaration text).
def OAI.BoltzmannNonuniqueness.boundedTimes line 121
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:141 (same declaration text).
structure OAI.BoltzmannNonuniqueness.AdmissibleGlobal line 125
Source documentation
Full global admissibility, including both separately renormalized collision terms, local mass, total momentum, and the every-time energy and entropy inequalities.
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:145 (same declaration text).
```
structure AdmissibleGlobal (f₀ : Density) (F : Evolution) : Prop where
…
```
Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Evolution
structure OAI.BoltzmannNonuniqueness.StrongEarly line 174
Source documentation
Additional regularity asserted on the common initial interval. The eLpNorm statement is strong L¹ continuity and cannot be made vacuous by a nonintegrable Bochner integral.
Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:194 (same declaration text).
```
structure StrongEarly (T : ℝ) (F : Evolution) : Prop where
…
```
Mentions: OAI.BoltzmannNonuniqueness.Evolution
def OAI.BoltzmannNonuniqueness.NonuniquenessStatement line 185
Source documentation
Two global solutions of one datum, differing on a common initial interval.
```
def NonuniquenessStatement : Prop :=
…
```
def OAI.BoltzmannNonuniqueness.PeriodicExistenceInput line 193
Source documentation
Periodic existence for continuation, as in Levermore–Masmoudi (2010), Theorem 4.1, including separate renormalized gain and loss integrability.
```
def PeriodicExistenceInput : Prop :=
…
```