WeightedWordBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Word-length control by a weighted norm

Short-cost factors are accumulated until they leave a small identity ball. Each completed block has bounded word length and pays for that length.

theorem OAI.PolycyclicRecognition.seminorm_product_cost_bound line 22

Source documentation

The residual factor stays in the small ball; every flushed block is charged against the accumulated cost.

theorem seminorm_product_cost_bound
    (p w : GroupSeminorm G) (c : G → ℝ≥0) {δ : ℝ}
    (hδ : 0 < δ) (hδ1 : δ ≤ 1)
    (hpc : ∀ g, p g ≤ c g)
    (hlocal : ∀ g, p g ≤ δ → w g ≤ 1)
    (hwc : ∀ g, w g ≤ max 1 (c g : ℝ))
    (l : List G) :
    w l.prod ≤ (4 / δ) * (productCost c l : ℝ) + 1 := by
…

Mentions: OAI.PolycyclicRecognition.productCost