PublishedInputs.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Published analytic input for periodic hard-sphere nonuniqueness

GLPS1988Proposition3 expresses the velocity-localized, time-dependent specialization of Proposition 3 of F. Golse, P.-L. Lions, B. Perthame and R. Sentis, "Regularity of the moments of the solution of a transport equation", J. Functional Analysis 76 (1988), 110–125, pp. 115–116, DOI: 10.1016/0022-1236(88)90051-1. The passage to evolution equations is explained in their Remark (2), p. 119. In their notation, the velocity measure is supported on velocities (1,v); compact velocity support supplies their nonconcentration condition (2.14).

This compactness statement applies to uniformly integrable sources with bounded velocity support, independently of the cap and branching constructions.

The global continuation input is Theorem 4.1 of C. D. Levermore and N. Masmoudi, "From the Boltzmann equation to an incompressible Navier–Stokes–Fourier system", Arch. Rational Mech. Anal. 196 (2010), 753–809, pp. 765–767, DOI: 10.1007/s00205-009-0254-5. The elementary entropy estimate converts that continuation theorem to separate gain and loss integrability.

abbrev OAI.BoltzmannNonuniqueness.Published.Velocity line 43
abbrev OAI.BoltzmannNonuniqueness.Published.SpaceTime line 44
abbrev OAI.BoltzmannNonuniqueness.Published.KineticPhase line 45
def OAI.BoltzmannNonuniqueness.Published.transportResolvent line 48
Source documentation
The damped free-transport resolvent, with the incoming characteristic parametrization.
```
def transportResolvent (r : KineticPhase → ℝ) (z : KineticPhase) : ℝ :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Published.KineticPhase
def OAI.BoltzmannNonuniqueness.Published.resolventAverage line 52
Source documentation
A velocity average of the damped free-transport resolvent.
```
def resolventAverage (r : KineticPhase → ℝ) (ψ : Velocity → ℝ) (z : SpaceTime) : ℝ :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Published.KineticPhase, OAI.BoltzmannNonuniqueness.Published.Velocity, OAI.BoltzmannNonuniqueness.Published.SpaceTime
def OAI.BoltzmannNonuniqueness.Published.LocalL1Converges line 57
Source documentation
Local L¹ convergence is stated with the extended L¹ seminorm, so that an undefined Bochner integral cannot make a nonintegrable error appear to have zero norm.
```
def LocalL1Converges (f : ℕ → SpaceTime → ℝ) (g : SpaceTime → ℝ) : Prop :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Published.SpaceTime
def OAI.BoltzmannNonuniqueness.Published.GLPS1988Proposition3 line 66
Source documentation
A sequential specialization of GLPS (1988), Proposition 3, with the evolution-equation extension in Remark (2), p. 119. Boundedness and uniform integrability are both contained in UniformIntegrable. The hypothesis has no relation to the novel branching construction.
```
def GLPS1988Proposition3 : Prop :=
…
```
def OAI.BoltzmannNonuniqueness.Published.entropyProduction line 75
Source documentation
The entropy-production integrand for strictly positive incoming and outgoing products.
```
def entropyProduction (A B : ℝ) : ℝ := (A - B) * Real.log (A / B)
```
theorem OAI.BoltzmannNonuniqueness.Published.entropyProduction_nonneg line 77
theorem OAI.BoltzmannNonuniqueness.Published.gain_le_loss_add_entropy line 89
Source documentation
The positive-product case of the entropy bound used in the manuscript's continuation argument: gain is controlled by twice loss and entropy production. Zero-product boundary values are extended-real values in the Boltzmann dissipation and are not encoded using Real.log 0.
```
theorem gain_le_loss_add_entropy {A B : ℝ} (hA : 0 < A) (hB : 0 < B) :
    A ≤ 2 * B + (2 / Real.log 2) * entropyProduction A B := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Published.entropyProduction
theorem OAI.BoltzmannNonuniqueness.Published.child_energy_le line 117
Source documentation
The squared child speed cannot exceed s + 1 if its spherical coordinate is in [-1,1] and its radial coefficient lies between zero and s + 1.
```
theorem child_energy_le {s R Z : ℝ} (hR : 0 ≤ R) (hRs : R ≤ s + 1)
    (hZ : Z ≤ 1) : (s + 1 + R * Z) / 2 ≤ s + 1 := by
…
```
theorem OAI.BoltzmannNonuniqueness.Published.reference_exit_probability_le line 125
Source documentation
For squared parent speed at most 25, the upper-tail probability from the uniform [-1,1] coordinate is at most 1/26. The formula applies when its radial coefficient is positive; the deterministic zero-radius case is handled by child_energy_le.
```
theorem reference_exit_probability_le {s R : ℝ} (hs : s ≤ 25) (hR : 0 < R)
    (hRs : R ≤ s + 1) :
    max 0 ((1 / 2 : ℝ) + (s - 49) / (2 * R)) ≤ 1 / 26 := by
…
```
theorem OAI.BoltzmannNonuniqueness.Published.reference_retention_probability_ge line 134
Source documentation
The retained probability in the speed-five ball has the value used in Section 9.
```
theorem reference_retention_probability_ge {s R : ℝ} (hs : s ≤ 25) (hR : 0 < R)
    (hRs : R ≤ s + 1) :
    25 / 26 ≤ 1 - max 0 ((1 / 2 : ℝ) + (s - 49) / (2 * R)) := by
…
```
theorem OAI.BoltzmannNonuniqueness.Published.reference_potential_ge line 142
Source documentation
The branching potential is bounded below by 48π/13, as soon as the scalar retention bound and the minimal two-beam collision frequency have been established.
```
theorem reference_potential_ge {p ν : ℝ} (hp : 25 / 26 ≤ p)
    (hν : 4 * Real.pi ≤ ν) : 48 * Real.pi / 13 ≤ (2 * p - 1) * ν := by
…
```
theorem OAI.BoltzmannNonuniqueness.Published.reference_rate_le line 151
Source documentation
The associated single-particle jump rate is bounded by 48π.
```
theorem reference_rate_le {p ν : ℝ} (hp : p ≤ 1)
    (hν : ν ≤ 24 * Real.pi) (hν0 : 0 ≤ ν) : 2 * p * ν ≤ 48 * Real.pi := by
…
```