VelocityWeight.lean`

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Removing a countable family of velocity windows from a null-set statement

theorem OAI.BoltzmannNonuniqueness.ae_prod_of_velocity_windows line 19
abbrev OAI.BoltzmannNonuniqueness.VelocityWeight.Transverse line 53
def OAI.BoltzmannNonuniqueness.VelocityWeight.transverse line 55
def OAI.BoltzmannNonuniqueness.VelocityWeight.axial line 58
def OAI.BoltzmannNonuniqueness.VelocityWeight.singularity line 60
def OAI.BoltzmannNonuniqueness.VelocityWeight.H line 62
def OAI.BoltzmannNonuniqueness.VelocityWeight.split line 67
Source documentation
The coordinate split is first axial, then transverse.
```
def split : Velocity ≃ᵐ (ℝ × Transverse) :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.VelocityWeight.Transverse
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.split_apply line 73
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.split_measurePreserving line 81
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.norm_sq_split line 91
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.singularity_nonneg line 97
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.locallyIntegrable_singularity line 101
Source documentation
The sharp local integrability range includes the manuscript's 1 < q < 2.
```
theorem locallyIntegrable_singularity {q : ℝ} (hq : q < 2) :
    LocallyIntegrable (singularity q) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.VelocityWeight.singularity
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.integrable_transverse_gaussian_rpow line 112
Source documentation
Gaussian decay retains transverse powers whenever their exponent exceeds -2.
```
theorem integrable_transverse_gaussian_rpow {β s : ℝ} (hβ : 0 < β) (hs : -2 < s) :
    Integrable (fun u : Transverse => ‖u‖ ^ s * Real.exp (-β * ‖u‖ ^ 2)) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.VelocityWeight.Transverse
def OAI.BoltzmannNonuniqueness.VelocityWeight.gaussianMajorant line 125
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.gaussianMajorant_nonneg line 128
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.integrable_gaussianMajorant line 133
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.H_nonneg line 157
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.H_le_gaussianMajorant line 161
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.integrable_H line 172
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.H_pos line 180
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.even_pow_mul_gaussian_le line 187
Source documentation
Absorbing an even power into half the Gaussian decay gives an explicit factorial constant.
```
theorem even_pow_mul_gaussian_le (r : ℝ) (n : ℕ) :
    r ^ (2 * n) * Real.exp (-r ^ 2) ≤
      (2 : ℝ) ^ n * (n.factorial : ℝ) * Real.exp (-r ^ 2 / 2) := by
…
```
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.H_even_moment_le line 209
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.integrable_even_moment_H line 229
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.integrable_moment_H line 241
Source documentation
The majorant has every natural polynomial velocity moment.
```
theorem integrable_moment_H {q : ℝ} (hq : q < 2) (n : ℕ) :
    Integrable (fun v : Velocity => ‖v‖ ^ n * H q v) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.VelocityWeight.H
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.one_add_rpow_le line 257
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.H_rpow_le line 278
Source documentation
Raising the majorant to a positive power multiplies its transverse singular exponent.
```
theorem H_rpow_le {p : ℝ} (hp : 0 ≤ p) (q : ℝ) (v : Velocity) :
    H q v ^ p ≤ (2 : ℝ) ^ p * gaussianMajorant p (p * q) v := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.VelocityWeight.H, OAI.BoltzmannNonuniqueness.VelocityWeight.gaussianMajorant
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.integrable_rpow_H line 304
Source documentation
The precise power-integrability range used for the initial cutoff solutions.
```
theorem integrable_rpow_H {p q : ℝ} (hp : 1 ≤ p) (hpq : p * q < 2) :
    Integrable (fun v : Velocity => H q v ^ p) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.VelocityWeight.H
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.exists_integrable_rpow_H line 317
def OAI.BoltzmannNonuniqueness.Published.velocityFourier line 338
theorem OAI.BoltzmannNonuniqueness.Published.velocityFourier_measurable line 341
theorem OAI.BoltzmannNonuniqueness.Published.velocityFourier_fiber_energy line 352
theorem OAI.BoltzmannNonuniqueness.Published.velocityFourier_fiber_memLp line 358
theorem OAI.BoltzmannNonuniqueness.Published.velocityFourier_integrable_sq line 364
theorem OAI.BoltzmannNonuniqueness.Published.velocityFourier_energy line 389
theorem OAI.BoltzmannNonuniqueness.Published.velocityFourier_support line 416