Moments.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Integrable moments of finite-entropy data

The weighted entropy assumption from the manuscript controls mass, kinetic energy, absolute entropy, and vector momentum. These conclusions use the actual integrability assumption rather than any default value of a Bochner integral.

theorem OAI.BoltzmannNonuniqueness.entropyMoment_nonneg line 19
theorem OAI.BoltzmannNonuniqueness.density_le_entropyMoment line 24
theorem OAI.BoltzmannNonuniqueness.energyDensity_le_entropyMoment line 30
theorem OAI.BoltzmannNonuniqueness.absEntropyDensity_le_entropyMoment line 35
theorem OAI.BoltzmannNonuniqueness.momentumDensity_norm_le_entropyMoment line 40
theorem OAI.BoltzmannNonuniqueness.FiniteEntropyDatum.integrable line 54
Source documentation
Finite weighted entropy gives finite mass.
```
theorem integrable : Integrable f := by
…
```
theorem OAI.BoltzmannNonuniqueness.FiniteEntropyDatum.integrable_energy line 60
Source documentation
The energy functional integrates an integrable density.
```
theorem integrable_energy : Integrable (fun z => ‖z.2‖ ^ 2 * f z) := by
…
```
theorem OAI.BoltzmannNonuniqueness.FiniteEntropyDatum.integrable_absEntropy line 68
Source documentation
This is absolute entropy, including the convention at zero from the model.
```
theorem integrable_absEntropy : Integrable (fun z => f z * |Real.log (f z)|) := by
…
```
theorem OAI.BoltzmannNonuniqueness.FiniteEntropyDatum.integrable_momentum line 79
Source documentation
The vector momentum integral is a genuine Bochner integral.
```
theorem integrable_momentum : Integrable (fun z => f z • z.2) := by
…
```
theorem OAI.BoltzmannNonuniqueness.FiniteEntropyDatum.integrable_entropy line 85