OAI/MathematicalPhysics/Boltzmann/Branching/VelocityAveraging.lean

The needed Golse–Lions–Perthame–Sentis compactness specialization

This proves the exact input from Proposition 3 (pp. 115–116) and the evolution extension, Remark (2) (p. 119), JFA 76 (1988). The velocity measure is Lebesgue measure on a ball. Bounded value truncations have uniformly small Fourier tails; one common subsequence converges locally in L2. Uniform L1 approximation then constructs the global L1 limit and yields local L1 convergence for the original sources. No spatial tightness or extra compactness hypothesis is imposed.