OAI/Combinatorics/EditApproximation/Coarse/CoarseGridInvariant.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarseChildAllowance_grid line 10

   Source documentation

   One descended allowance acquires only one factor of the fixed root base in its denominator. This includes the literal sampled child label.

    theorem coarseChildAllowance_grid (B q L j : ℕ) (allowance : ℚ) (draw : Fin B)
       (hB : 0 < B) (hq : 0 < q) (hL : 0 < L)
       (ha : allowance.den ∣ (L * B * q) ^ j) :
       ((1 / (L : ℚ)) * coarseChildThreshold B q allowance draw).den ∣
         (L * B * q) ^ (j + 1) := by
   …

   Mentions: OAI.EditApproximation.coarseChildThreshold

2. theorem OAI.EditApproximation.coarseDescendant_grid line 29

   Source documentation

   Every descendant array lives on the same denominator constructed for its root; it is unnecessary to normalize any array sum by a gcd.

    theorem coarseDescendant_grid {B d : ℕ} {α : Type*} [DecidableEq α]
       (k q L j : ℕ) (frame : List (Option α)) (tree : CoarseSourceTree B α d)
       (draws : CoarseThresholdDraws B d) (allowance : ℚ)
       (hB : 0 < B) (hq : 0 < q) (hL : 0 < L)
       (ha : allowance.den ∣ (L * B * q) ^ j) (start : ℕ) (shift : Fin (2 * k + 1)) :
       (coarseThresholdEstimate k q (1 / L) frame tree draws allowance start shift).den ∣
         coarseCommonDenominator 1 q L B (j + d) := by
   …

   Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseThresholdEstimate, OAI.EditApproximation.coarseCommonDenominator

3. theorem OAI.EditApproximation.coarseDescendant_magnitude line 43

   Source documentation

   Uniform root magnitude for every descendant and pruning outcome.

    theorem coarseDescendant_magnitude {B d : ℕ} {α : Type*} [DecidableEq α]
       (k q L D n : ℕ) (frame : List (Option α)) (tree : CoarseSourceTree B α d)
       (draws : CoarseThresholdDraws B d) (allowance : ℚ)
       (hB : 2 ≤ B) (hq : 0 < q) (hL : 0 < L) (hd : d ≤ D)
       (hn : tree.word.length ≤ n) (ha : 0 ≤ allowance) (hak : allowance ≤ k)
       (start : ℕ) (shift : Fin (2 * k + 1)) :
       |coarseThresholdEstimate k q (1 / L) frame tree draws allowance start shift| ≤
         ((n + B * k * B ^ D : ℕ) : ℚ) := by
   …

   Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseThresholdEstimate