HotGainReduction.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Algebraic reduction of the quadratic hot gain

Symmetry allows the output polynomial weight to be assigned to either incoming velocity. The resulting mixed gain has only one polynomial factor, while its two Gaussian factors cancel by collision energy conservation.

def OAI.BoltzmannNonuniqueness.HotWeight.G line 22
def OAI.BoltzmannNonuniqueness.HotWeight.polynomial line 24
theorem OAI.BoltzmannNonuniqueness.HotWeight.G_pos line 26
theorem OAI.BoltzmannNonuniqueness.HotWeight.polynomial_pos line 29
theorem OAI.BoltzmannNonuniqueness.HotWeight.H_mul_polynomial line 33
theorem OAI.BoltzmannNonuniqueness.HotWeight.H_eq_G_div line 42
theorem OAI.BoltzmannNonuniqueness.HotWeight.measurable_G line 45
theorem OAI.BoltzmannNonuniqueness.HotWeight.polynomial_pair_bound line 51
Source documentation
The fixed manuscript exponent m = 100 needs only this two-input estimate.
```
theorem polynomial_pair_bound (p ξ v : Velocity)
    (hv : ‖v‖ ^ 2 ≤ ‖p‖ ^ 2 + ‖ξ‖ ^ 2) :
    polynomial v ≤ (2 : ℝ) ^ (50 : ℕ) * (polynomial p + polynomial ξ) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.HotWeight.polynomial
theorem OAI.BoltzmannNonuniqueness.HotWeight.quadratic_ratio_bound line 67
Source documentation
The quadratic integrand is bounded by a symmetric mixed integrand.
```
theorem quadratic_ratio_bound (q : ℝ) (p ξ v : Velocity)
    (hv : ‖v‖ ^ 2 ≤ ‖p‖ ^ 2 + ‖ξ‖ ^ 2) :
    H q p * H q ξ / H q v ≤ (2 : ℝ) ^ (50 : ℕ) *
      ((H q p * G q ξ + G q p * H q ξ) / G q v) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.HotWeight.G
theorem OAI.BoltzmannNonuniqueness.HotWeight.quadratic_product_bound line 78
theorem OAI.BoltzmannNonuniqueness.HotWeight.mixed_plane_weight line 89
Source documentation
Both Gaussian factors cancel against the output Gaussian on the collision plane.
```
theorem mixed_plane_weight (q : ℝ) (p ξ v : Velocity)
    (h : inner ℝ (v - p) (ξ - v) = 0) :
    H q p * (G q ξ / G q v) =
      Real.exp (-‖companionVelocity p ξ v‖ ^ 2) * (polynomial p)⁻¹ *
        (W q p * W q ξ / W q v) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.HotWeight.G, OAI.BoltzmannNonuniqueness.companionVelocity, OAI.BoltzmannNonuniqueness.HotWeight.polynomial
def OAI.BoltzmannNonuniqueness.HotShellWeight.constant line 133
theorem OAI.BoltzmannNonuniqueness.HotShellWeight.constant_pos line 135
theorem OAI.BoltzmannNonuniqueness.HotShellWeight.polynomial_eighth_bound line 137
theorem OAI.BoltzmannNonuniqueness.HotShellWeight.polynomial_inv_le_one line 148
theorem OAI.BoltzmannNonuniqueness.HotShellWeight.gaussian_eighth_bound line 152
theorem OAI.BoltzmannNonuniqueness.HotShellWeight.decay line 162
def OAI.BoltzmannNonuniqueness.HotGainReduction.coefficient line 221
theorem OAI.BoltzmannNonuniqueness.HotGainReduction.coefficient_nonneg line 224
theorem OAI.BoltzmannNonuniqueness.HotGainReduction.pair_bound line 228
theorem OAI.BoltzmannNonuniqueness.HotGainReduction.quadratic_gain_le_mixed line 260
Source documentation
The factor H(v)/G(v) is essential: division by H(v) leaves a uniform mixed-gain problem normalized by G(v).
```
theorem quadratic_gain_le_mixed (q : ℝ) (v : Velocity) :
    nonnegativeGain (fun ξ => ENNReal.ofReal (H q ξ))
      (fun ξ => ENNReal.ofReal (H q ξ)) v ≤
    ENNReal.ofReal (coefficient q v) *
      nonnegativeGain (fun ξ => ENNReal.ofReal (H q ξ))
        (fun ξ => ENNReal.ofReal (G q ξ)) v := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.nonnegativeGain, OAI.BoltzmannNonuniqueness.HotGainReduction.coefficient