SelfSummability.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sampling_self_base_bound line 15

Source documentation

A concrete logarithmic estimate sufficient for the source exponent gap.

theorem sampling_self_base_bound (m : ℝ) (hm1 : 1 ≤ m) (hlarge : 802 ≤ m^(1/50 : ℝ)) :
    2+8*m^(3/5 : ℝ)*Real.log m ≤ m^(63/100 : ℝ) := by
…

theorem OAI.FiniteFactor.sourceSamplingSelfBudget_eventually line 31
theorem OAI.FiniteFactor.sourceSampling_inverse_square_summable line 65
Source documentation
The actual block growth makes the inverse-square stage sequence summable.
```
theorem sourceSampling_inverse_square_summable : Summable (fun stage => (sourceBlockSize stage : ℝ)^(-2 : ℝ)) := by
…
```
Mentions: OAI.FiniteFactor.sourceBlockSize
theorem OAI.FiniteFactor.sourceSamplingSelfBudget_summable line 82
Source documentation
Summability of the actual full-product self-pair budget.
```
theorem sourceSamplingSelfBudget_summable : Summable sourceSamplingSelfBudget := by
…
```
Mentions: OAI.FiniteFactor.sourceSamplingSelfBudget