ScalarEntropyConvex.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The scalar relative-entropy balance along characteristic paths

theorem OAI.BoltzmannNonuniqueness.scalar_entropy_integral_balance line 23
def OAI.BoltzmannNonuniqueness.entropyDual line 75
theorem OAI.BoltzmannNonuniqueness.entropyDual_le line 77
theorem OAI.BoltzmannNonuniqueness.entropyDual_log_ratio line 93
theorem OAI.BoltzmannNonuniqueness.entropyDual_zero_tendsto line 101
theorem OAI.BoltzmannNonuniqueness.AxialSlices.intervalIntegrable_abs_rpow line 135
theorem OAI.BoltzmannNonuniqueness.AxialSlices.intervalIntegrable_abs_sub_rpow line 146
theorem OAI.BoltzmannNonuniqueness.AxialSlices.integral_abs_rpow_zero line 150
theorem OAI.BoltzmannNonuniqueness.AxialSlices.integral_abs_rpow_symmetric line 156
theorem OAI.BoltzmannNonuniqueness.AxialSlices.integral_abs_sub_rpow_le line 169
Source documentation
A power singularity has at most twice the endpoint mass on an interval of length b-a. This is the root-independent estimate in the large-slope case of ker:scalar-interval.
```
theorem integral_abs_sub_rpow_le {r a b t : ℝ} (hr : -1 < r) (hr₀ : r ≤ 0)
    (hab : a ≤ b) :
    (∫ x : ℝ in a..b, |x - t| ^ r) ≤ 2 * (b - a) ^ (r + 1) / (r + 1) := by
…
```
theorem OAI.BoltzmannNonuniqueness.AxialSlices.abs_affine_rpow line 230
theorem OAI.BoltzmannNonuniqueness.AxialSlices.intervalIntegrable_abs_affine_rpow line 235

theorem OAI.BoltzmannNonuniqueness.AxialSlices.integral_abs_affine_rpow_le line 246

Source documentation

Large-slope estimate obtained by rescaling the root-independent interval bound.

theorem integral_abs_affine_rpow_le {r a b A B : ℝ} (hr : -1 < r) (hr₀ : r ≤ 0)
    (hab : a ≤ b) (hB : B ≠ 0) :
    (∫ x : ℝ in a..b, |A - B * x| ^ r) ≤
      |B| ^ r * (2 * (b - a) ^ (r + 1) / (r + 1)) := by
…

theorem OAI.BoltzmannNonuniqueness.AxialSlices.small_slope_distance line 256
Source documentation
If the slope is small, the affine function stays a fixed distance from zero.
```
theorem small_slope_distance {A B R x : ℝ} (_hR : 0 ≤ R)
    (hAB : 2 * R * |B| ≤ |A|) (hx : |x| ≤ R) :
    |A| / 2 ≤ |A - B * x| := by
…
```

theorem OAI.BoltzmannNonuniqueness.AxialSlices.integral_abs_affine_rpow_le_small_slope line 267

Source documentation

The small-slope half of the scalar estimate, before combining the powers of the length.

theorem integral_abs_affine_rpow_le_small_slope {r a b A B R : ℝ}
    (hr : -1 < r) (hr₀ : r ≤ 0) (hab : a ≤ b)
    (hR : 0 ≤ R) (ha : -R ≤ a) (hb : b ≤ R) (hA : A ≠ 0)
    (hAB : 2 * R * |B| ≤ |A|) :
    (∫ x : ℝ in a..b, |A - B * x| ^ r) ≤ (b - a) * (|A| / 2) ^ r := by
…

def OAI.BoltzmannNonuniqueness.AxialSlices.scalarConstant line 279
theorem OAI.BoltzmannNonuniqueness.AxialSlices.scalarConstant_pos line 281
theorem OAI.BoltzmannNonuniqueness.AxialSlices.length_le_scaled_power line 286
theorem OAI.BoltzmannNonuniqueness.AxialSlices.integral_abs_affine_rpow_scalar_bound line 300
Source documentation
The scalar interval estimate ker:scalar-interval, with an explicit constant. The singular case A=0 is understood in the extended sense in the manuscript; the finite estimate needed off the exceptional line is stated here.
```
theorem integral_abs_affine_rpow_scalar_bound {r a b A B R : ℝ}
    (hr : -1 < r) (hr₀ : r ≤ 0) (hab : a < b) (hR : 0 < R)
    (ha : -R ≤ a) (hb : b ≤ R) (hA : A ≠ 0) :
    (∫ x : ℝ in a..b, |A - B * x| ^ r) ≤
      scalarConstant r * (R ^ (-r) * (b - a) ^ (r + 1) * |A| ^ r) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialSlices.scalarConstant

theorem OAI.BoltzmannNonuniqueness.AxialSlices.scalar_interval_bound line 356

Source documentation

The manuscript's scalar slice estimate in its q notation.

theorem scalar_interval_bound {q a b A B R : ℝ}
    (hq₁ : 1 < q) (hq₂ : q < 2) (hab : a < b) (hR : 0 < R)
    (ha : -R ≤ a) (hb : b ≤ R) (hA : A ≠ 0) :
    (∫ x : ℝ in a..b, |A - B * x| ^ (1 - q)) ≤
      scalarConstant (1 - q) * (R ^ (q - 1) * (b - a) ^ (2 - q) * |A| ^ (1 - q)) := by
…

Mentions: OAI.BoltzmannNonuniqueness.AxialSlices.scalarConstant

theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_convex line 381
theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_double line 393
theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_add_le line 402
theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_le_of_le line 414