FiniteNumeric.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic for the finite-tree obstruction

The parameter estimate and final rearrangement in prop:finite-lower hold with the explicit absolute constant 34.

lemma OAI.TreeEdit.BinaryLower.FiniteNumeric.period_ratio_bound line 14

theorem OAI.TreeEdit.BinaryLower.FiniteNumeric.finite_root_bound line 40

Source documentation

The final line of eq:finite-root-upper, with an explicit constant.

theorem finite_root_bound {k : ℕ} {M V : ℝ} (hk : 1 ≤ k) (hM : 0 ≤ M)
    (hV : V ≤ 4 * M *
      (2 * (k : ℝ) * (4 * (k : ℝ) ^ (10 * k)) / (k : ℝ) ^ (20 * k) +
        1 / (2 * (k : ℝ) ^ k))) :
    V ≤ 34 * M / (k : ℝ) ^ k := by
…

theorem OAI.TreeEdit.BinaryLower.FiniteNumeric.finite_distortion_bound line 58

Source documentation

Uniform root separation and the preceding upper displacement estimate force the source's (k/4)^k lower distortion, with constant 1/34.

theorem finite_distortion_bound {k : ℕ} {M V D : ℝ}
    (hk : 1 ≤ k) (hM : 0 < M) (hD : 0 < D)
    (hlower : M / ((4 : ℝ) ^ k * D) ≤ V)
    (hupper : V ≤ 34 * M / (k : ℝ) ^ k) :
    ((k : ℝ) / 4) ^ k / 34 ≤ D := by
…

theorem OAI.TreeEdit.BinaryLower.FiniteNumeric.averaging_length_le_rows line 77
Source documentation
The source averaging length J=4k^(10k) lies within the row budget T=k^(20k) already for every k≥2.
```
theorem averaging_length_le_rows {k : ℕ} (hk : 2 ≤ k) :
    4 * k ^ (10 * k) ≤ k ^ (20 * k) := by
…
```
theorem OAI.TreeEdit.BinaryLower.FiniteNumeric.sparse_period_twice_le line 91
Source documentation
The bound on a sparse character period at any internal depth implies the half-averaging-interval bound required by short-period detection.
```
theorem sparse_period_twice_le {k j r q : ℕ} (hk : 1 ≤ k)
    (hj : j < k) (hr : r < k)
    (hq : q ≤ 2 * k ^ (5 * j + 5 * r)) :
    2 * q ≤ 4 * k ^ (10 * k) := by
…
```