LossIntegrability.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Loss frequency and its first-moment bound

The angular normalization gives the loss-frequency formula from Section 2, equation eq:frequency. Fubini is used only with an explicit integrability hypothesis for the original collision integrand. Separate first-moment conditions ensure that the frequency integral itself is finite.

def OAI.BoltzmannNonuniqueness.frequency line 23
Source documentation
The loss frequency in the paper's normal parametrization.
```
def frequency (f : Density) (x : Position) (v : Velocity) : ℝ :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity
theorem OAI.BoltzmannNonuniqueness.loss_eq_mul_frequency line 27
Source documentation
Fubini and angular normalization identify the original loss collision integral.
```
theorem loss_eq_mul_frequency (f : Density) (x : Position) (v : Velocity)
    (hi : Integrable (fun p : Velocity × Sphere =>
      collisionKernel v p.1 p.2 * f (x, v) * f (x, p.1))
      ((volume : Measure Velocity).prod sphereArea)) :
    loss f x v = f (x, v) * frequency f x v := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.Sphere, OAI.BoltzmannNonuniqueness.collisionKernel, OAI.BoltzmannNonuniqueness.sphereArea, OAI.BoltzmannNonuniqueness.loss, OAI.BoltzmannNonuniqueness.frequency
theorem OAI.BoltzmannNonuniqueness.frequency_integrand_norm_le line 45
theorem OAI.BoltzmannNonuniqueness.integrable_abs_firstMoment line 54
theorem OAI.BoltzmannNonuniqueness.integrable_frequency_integrand line 60
Source documentation
Finite mass and first absolute velocity moment make the frequency integrable.
```
theorem integrable_frequency_integrand (f : Density) (x : Position) (v : Velocity)
    (hf : Integrable (fun w : Velocity => f (x, w)))
    (hm : Integrable (fun w : Velocity => ‖w‖ * f (x, w))) :
    Integrable (fun w : Velocity => ‖v - w‖ * f (x, w)) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity

theorem OAI.BoltzmannNonuniqueness.abs_frequency_le line 73

Source documentation

An absolute bound valid for signed densities as well as nonnegative ones.

theorem abs_frequency_le (f : Density) (x : Position) (v : Velocity)
    (hf : Integrable (fun w : Velocity => f (x, w)))
    (hm : Integrable (fun w : Velocity => ‖w‖ * f (x, w))) :
    |frequency f x v| ≤ 2 * Real.pi *
      (‖v‖ * (∫ w : Velocity, |f (x, w)|) +
        ∫ w : Velocity, ‖w‖ * |f (x, w)|) := by
…

Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.frequency

theorem OAI.BoltzmannNonuniqueness.frequency_nonneg line 98
theorem OAI.BoltzmannNonuniqueness.collisionKernel_le_norm line 123
theorem OAI.BoltzmannNonuniqueness.integrable_loss_of_moments line 129
theorem OAI.BoltzmannNonuniqueness.gaussian_gain_eq_frequency line 149