CodeNumerics.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Numerical estimates used in the fixed-length binary conversion.

def OAI.TreeEdit.BinaryLower.Code.segmentThreshold line 13
Source documentation
The segment threshold used in the prescribed-length code construction.
```
noncomputable def segmentThreshold (M : ℕ) : ℕ :=
…
```
theorem OAI.TreeEdit.BinaryLower.Code.eventually_short_pair_error line 17
Source documentation
Eventually the error from the short block-pair spans fits within half a block.
```
theorem eventually_short_pair_error :
    ∀ᶠ M : ℕ in atTop,
      0 < M ∧ 2 * (M : ℝ) * segmentThreshold M ≤ (M : ℝ) ^ 2 / 2 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold
theorem OAI.TreeEdit.BinaryLower.Code.exists_short_pair_threshold line 43
Source documentation
An absolute integer threshold exists, as required in the manuscript.
```
theorem exists_short_pair_threshold :
    ∃ M₀ : ℕ, ∀ M : ℕ, M₀ ≤ M →
      0 < M ∧ 2 * (M : ℝ) * segmentThreshold M ≤ (M : ℝ) ^ 2 / 2 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold
theorem OAI.TreeEdit.BinaryLower.Code.deficit_from_additive line 50
Source documentation
Removing the additive error in the block-matching estimate gives the constant 402. The nonzero original deficit is integral, hence at least one.
```
theorem deficit_from_additive {P r δ e : ℝ}
    (hP : 0 ≤ P) (hr : 1 ≤ r)
    (hadd : P * r ≤ 201 * δ + e) (herr : e ≤ P / 2) :
    P / 402 * r ≤ δ := by
…
```
theorem OAI.TreeEdit.BinaryLower.Code.edit_lower_from_deficit line 59
Source documentation
Combining the deficit inequality with the two ordinary-edit comparisons produces exactly the constant 804, without changing the edit metric.
```
theorem edit_lower_from_deficit {P r r' d d' : ℝ}
    (hP : 0 ≤ P) (hdeficit : P / 402 * r ≤ r')
    (hleft : r' ≤ d') (hright : d ≤ 2 * r) :
    P / 804 * d ≤ d' := by
…
```

theorem OAI.TreeEdit.BinaryLower.Code.block_counts_to_additive line 68

Source documentation

The equal-label and unequal-label counts combine into the additive estimate. All quantities are natural cardinalities, so no rounding is hidden.

theorem block_counts_to_additive {M P a₀ L r matched equal unequal δ : ℕ}
    (hpartition : matched = equal + unequal)
    (htotal : matched + δ = M * P)
    (hdeficit : r + L = M)
    (hequal : equal ≤ P * L)
    (hunequal : unequal ≤ 200 * δ + 2 * M * a₀) :
    P * r ≤ 201 * δ + 2 * M * a₀ := by
…

theorem OAI.TreeEdit.BinaryLower.Code.natural_deficit_from_additive line 78
Source documentation
Integral form of the error absorption, including the zero-deficit case.
```
theorem natural_deficit_from_additive {P r δ e : ℕ}
    (hadd : P * r ≤ 201 * δ + e) (herr : 2 * e ≤ P) :
    P * r ≤ 402 * δ := by
…
```
theorem OAI.TreeEdit.BinaryLower.Code.real_deficit_of_natural line 89
Source documentation
Cast the integral matching conclusion into the exact real-valued lower bound used in the statement of the fixed-length conversion theorem.
```
theorem real_deficit_of_natural {P r δ : ℕ}
    (h : P * r ≤ 402 * δ) :
    (P : ℝ) / 402 * r ≤ δ := by
…
```
theorem OAI.TreeEdit.BinaryLower.Code.segmentThreshold_eq line 96
Source documentation
The two common formulas for the segment threshold agree at positive M.
```
theorem segmentThreshold_eq (M : ℕ) :
    segmentThreshold M =
      Nat.ceil (40 * Real.logb 2 ((M : ℝ) ^ 3)) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold
theorem OAI.TreeEdit.BinaryLower.Code.code_failure_power_bound line 105
Source documentation
Elementary failure tail at the source logarithmic segment threshold.
```
theorem code_failure_power_bound {M : ℕ} (hM : 1 ≤ M) :
    (9 / 10 : ℝ) ^ segmentThreshold M * (M : ℝ) ^ 12 ≤ 1 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold
theorem OAI.TreeEdit.BinaryLower.Code.code_union_bound_lt_one line 147
Source documentation
The segment-comparison count times the failure bound is below one.
```
theorem code_union_bound_lt_one {M : ℕ} (hM : 2 ≤ M) :
    (M : ℝ) ^ 2 * ((M : ℝ) ^ 2 + 1) ^ 3 *
      (9 / 10 : ℝ) ^ segmentThreshold M < 1 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold

theorem OAI.TreeEdit.BinaryLower.Code.exists_code_numerical_threshold line 173

Source documentation

One absolute threshold supplies both probabilistic and deterministic estimates.

theorem exists_code_numerical_threshold :
    ∃ M₀ : ℕ, ∀ M : ℕ, M₀ ≤ M →
      2 ≤ M ∧
      2 * (M : ℝ) * segmentThreshold M ≤ (M : ℝ) ^ 2 / 2 ∧
      (M : ℝ) ^ 2 * ((M : ℝ) ^ 2 + 1) ^ 3 *
        (9 / 10 : ℝ) ^ segmentThreshold M < 1 := by
…

Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold

theorem OAI.TreeEdit.BinaryLower.Code.code_union_bound_for_alphabet line 186
Source documentation
Alphabet sizes below M only decrease the comparison count.
```
theorem code_union_bound_for_alphabet {K M : ℕ} (hK : K ≤ M) (hM : 2 ≤ M) :
    (K : ℝ) ^ 2 * ((M : ℝ) ^ 2 + 1) ^ 3 *
      (9 / 10 : ℝ) ^ segmentThreshold M < 1 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold
theorem OAI.TreeEdit.BinaryLower.Code.segmentThreshold_le_square line 194
Source documentation
The short-pair threshold is no larger than the block width once its error-absorption inequality holds.
```
theorem segmentThreshold_le_square {M : ℕ} (hM : 1 ≤ M)
    (h : 2 * (M : ℝ) * segmentThreshold M ≤ (M : ℝ) ^ 2 / 2) :
    segmentThreshold M ≤ M ^ 2 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Code.segmentThreshold