WeightAlgebra.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Weight transfer on a collision plane

The exact Gaussian identity and polynomial transfer turn the normalized gain weight into the tilted cold measure used in ker:tilted-kernel.

def OAI.BoltzmannNonuniqueness.VelocityWeight.W line 19
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.W_pos line 21
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.rpow_neg_fifty line 25
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.H_ratio line 29
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.polynomial_ratio_le line 39
def OAI.BoltzmannNonuniqueness.VelocityWeight.tiltConstant line 47
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.tiltConstant_pos line 49
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.polynomial_le_gaussian line 51
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.collision_weight_ratio_le line 61
Source documentation
The complete weight ratio estimate preceding the tilted-kernel bound.
```
theorem collision_weight_ratio_le (q : ℝ) (p ξ v : Velocity)
    (h : inner ℝ (v - p) (ξ - v) = 0) :
    H q ξ / H q v ≤ tiltConstant *
      Real.exp (2 * ‖p‖ ^ 2 - ‖companionVelocity p ξ v‖ ^ 2) * (W q ξ / W q v) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.VelocityWeight.H, OAI.BoltzmannNonuniqueness.VelocityWeight.tiltConstant, OAI.BoltzmannNonuniqueness.companionVelocity, OAI.BoltzmannNonuniqueness.VelocityWeight.W
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.singular_fraction_le_one line 85
Source documentation
The singular part of the transverse normalization is uniformly bounded.
```
theorem singular_fraction_le_one {r : ℝ} (hr : 0 < r) (q : ℝ) :
    r ^ (-q) / (1 + r ^ (-q)) ≤ 1 := by
…
```
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.regular_fraction_le_power line 91
Source documentation
Near the axis, the regular part gains the positive power q-1.
```
theorem regular_fraction_le_power {r : ℝ} (hr : 0 < r) (q : ℝ) :
    r⁻¹ / (1 + r ^ (-q)) ≤ r ^ (q - 1) := by
…
```
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.regular_fraction_le_one line 99
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.inverse_weight_le_power line 108
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.shell_alternative line 118
Source documentation
The shell alternative used to extract either a cold or a Gaussian tail.
```
theorem shell_alternative (p k : Velocity) {R : ℝ}
    (h : R < ‖p‖ + ‖k‖) : R / 4 < ‖p‖ ∨ R / 2 < ‖p + k‖ := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.gaussian_shell_decay line 128
theorem OAI.BoltzmannNonuniqueness.VelocityWeight.axial_tilt_tail line 134
Source documentation
The axial exponential moment removes the tilted large-velocity tail.
```
theorem axial_tilt_tail {a u : ℝ} (hu : 0 ≤ u) (ha : u ≤ |a|) :
    Real.exp (2 * a ^ 2) ≤ Real.exp (-6 * u ^ 2) * Real.exp (8 * a ^ 2) := by
…
```