WordTransferFormulaBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Derived polynomial sizes for the concrete fixed-depth word transfer

def OAI.Ostmann.WordTransferTemplate.WordsBounded line 13

theorem OAI.Ostmann.WordTransferTemplate.branching_formula_cost line 20

Source documentation

Every output formula is obtained by at most n substitutions, each of size at most B. This supplies the polynomial loss used by the analytic bound.

theorem branching_formula_cost {n : ℕ} (template : WordTransferTemplate σ n)
    (t : FrequencyTree ℤ n) (hn : NonzeroInternalFrequencies n t)
    (B C : ℕ) (hB : 1 ≤ B) (hC : 1 ≤ C) (hwords : template.WordsBounded B)
    (env : σ → HistoryFormula σ) (henv : ∀ i, (env i).cost ≤ C) :
    (∀ z ∈ (template.branching t hn).formulaLeaves env, z.2.cost ≤ C * B ^ (n + 1)) ∧
    (∀ F ∈ (template.branching t hn).pivotFormulas env, F.cost ≤ C * B ^ (n + 1)) := by
…

Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.HistoryFormula