DatumBounds.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Summable cold-jet datum bounds

Section 4 of the supplied manuscript bounds the mass and energy of each annulus by a constant times s_j², and its absolute entropy by a constant times s_j² (1 + |log s_j|). Those scalar bounds are summable for the stated geometric scales, and their tails converge to zero. Indices start at zero; the manuscript's indices starting at one are obtained by removing the first term.

def OAI.BoltzmannNonuniqueness.DatumBounds.scale line 27
Source documentation
The annular scale s₀ exp(-jη).
```
def scale (s₀ η : ℝ) (j : ℕ) : ℝ := s₀ * Real.exp (-(j : ℝ) * η)
```
def OAI.BoltzmannNonuniqueness.DatumBounds.entropyBound line 30
Source documentation
The summable majorant for the absolute entropy of one annulus.
```
def entropyBound (s₀ η : ℝ) (j : ℕ) : ℝ :=
…
```
theorem OAI.BoltzmannNonuniqueness.DatumBounds.scale_pos line 33
theorem OAI.BoltzmannNonuniqueness.DatumBounds.scale_pow line 36
theorem OAI.BoltzmannNonuniqueness.DatumBounds.log_scale line 42
theorem OAI.BoltzmannNonuniqueness.DatumBounds.abs_log_scale_le line 47
theorem OAI.BoltzmannNonuniqueness.DatumBounds.summable_scale_pow_mul_nat_pow line 57
Source documentation
Polynomial factors in the index remain summable against every positive power of the geometric scale. This is used with p = 2 and index powers zero and one below.
```
theorem summable_scale_pow_mul_nat_pow (s₀ : ℝ) {η : ℝ} (hη : 0 < η)
    (p k : ℕ) (hp : 0 < p) :
    Summable (fun j : ℕ => scale s₀ η j ^ p * (j : ℝ) ^ k) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.DatumBounds.scale
theorem OAI.BoltzmannNonuniqueness.DatumBounds.summable_scale_pow line 67
theorem OAI.BoltzmannNonuniqueness.DatumBounds.summable_scale_sq line 71
theorem OAI.BoltzmannNonuniqueness.DatumBounds.summable_index_mul_scale_sq line 75
theorem OAI.BoltzmannNonuniqueness.DatumBounds.entropyBound_nonneg line 79
theorem OAI.BoltzmannNonuniqueness.DatumBounds.entropyBound_le line 83
theorem OAI.BoltzmannNonuniqueness.DatumBounds.summable_scale_pow_log line 93
Source documentation
A positive scale power also absorbs the absolute logarithm; power four applies to the vanishing hot-seed entropy estimate in the same datum lemma.
```
theorem summable_scale_pow_log {s₀ η : ℝ} (hs₀ : 0 < s₀) (hη : 0 < η)
    (p : ℕ) (hp : 0 < p) :
    Summable (fun j : ℕ => scale s₀ η j ^ p * (1 + |Real.log (scale s₀ η j)|)) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.DatumBounds.scale
theorem OAI.BoltzmannNonuniqueness.DatumBounds.summable_entropyBound line 107
theorem OAI.BoltzmannNonuniqueness.DatumBounds.scale_tendsto_zero line 111
theorem OAI.BoltzmannNonuniqueness.DatumBounds.scale_pow_log_tendsto_zero line 115
def OAI.BoltzmannNonuniqueness.DatumBounds.massTail line 122
Source documentation
The mass and energy scalar remainder after the first N annuli.
```
def massTail (s₀ η : ℝ) (N : ℕ) : ℝ := ∑' j : ℕ, scale s₀ η (j + N) ^ 2
```
Mentions: OAI.BoltzmannNonuniqueness.DatumBounds.scale
def OAI.BoltzmannNonuniqueness.DatumBounds.entropyTail line 125
Source documentation
The absolute-entropy scalar remainder after the first N annuli.
```
def entropyTail (s₀ η : ℝ) (N : ℕ) : ℝ := ∑' j : ℕ, entropyBound s₀ η (j + N)
```
Mentions: OAI.BoltzmannNonuniqueness.DatumBounds.entropyBound
theorem OAI.BoltzmannNonuniqueness.DatumBounds.massTail_nonneg line 127
theorem OAI.BoltzmannNonuniqueness.DatumBounds.entropyTail_nonneg line 130
theorem OAI.BoltzmannNonuniqueness.DatumBounds.massTail_eq_tsum_sub_sum line 133
theorem OAI.BoltzmannNonuniqueness.DatumBounds.entropyTail_eq_tsum_sub_sum line 139
theorem OAI.BoltzmannNonuniqueness.DatumBounds.massTail_tendsto_zero line 146
theorem OAI.BoltzmannNonuniqueness.DatumBounds.entropyTail_tendsto_zero line 155
theorem OAI.BoltzmannNonuniqueness.DatumBounds.mass_partial_sums_tendsto line 165
Source documentation
Finite annular mass/energy bounds converge to their full sum.
```
theorem mass_partial_sums_tendsto (s₀ : ℝ) {η : ℝ} (hη : 0 < η) :
    Tendsto (fun N => ∑ j ∈ range N, scale s₀ η j ^ 2) atTop
      (𝓝 (∑' j : ℕ, scale s₀ η j ^ 2)) :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.DatumBounds.scale
theorem OAI.BoltzmannNonuniqueness.DatumBounds.entropy_partial_sums_tendsto line 171
Source documentation
Finite annular absolute-entropy bounds converge to their full sum.
```
theorem entropy_partial_sums_tendsto {s₀ η : ℝ} (hs₀ : 0 < s₀) (hη : 0 < η) :
    Tendsto (fun N => ∑ j ∈ range N, entropyBound s₀ η j) atTop
      (𝓝 (∑' j : ℕ, entropyBound s₀ η j)) :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.DatumBounds.entropyBound