WordBoxComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Comparing boxes with varying maximizing word bases

Only the target basis needs to maximize its costs. A small change in the costs of the finite word list introduces exactly its exponential error.

theorem OAI.PolycyclicRecognition.exists_word_box_comparison_constant line 22

Source documentation

A uniform basis-change bound for all cost functions.

theorem exists_word_box_comparison_constant
    (X : I → L) (S : Finset (FreeMagma I))
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (cost newCost : S → ℝ)
      (β γ : WordBasisSelections X S),
      IsMaximizingColumnBasis (wordListCoordinates X S b₀) cost β.val →
      ∀ {r ε : ℝ}, 0 ≤ r → (∀ w, newCost w ≤ cost w + ε) → ∀ v : L,
        ‖(exponentialRescaleBasis (WordBasisSelections.basis X S β)
          (fun j => cost (β.val j)) r).equivFun v‖ ≤
        D * Real.exp (ε * r) *
          ‖(exponentialRescaleBasis (WordBasisSelections.basis X S γ)
            (fun j => newCost (γ.val j)) r).equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.exists_sequence_word_box_envelope line 89

Source documentation

Vanishing errors in the costs and subexponential box radii admit one subexponential envelope in a single fixed maximizing basis.

theorem exists_sequence_word_box_envelope
    (X : I → L) (S : Finset (FreeMagma I))
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    (cost : S → ℝ) (β : WordBasisSelections X S)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates X S b₀) cost β.val)
    (scale ε R : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
    (hscale0 : ∀ n, 0 ≤ scale n) (hε : Tendsto ε atTop (𝓝 0))
    (hR0 : ∀ n, 0 ≤ R n) (hR : HasSubexponentialUpperBoundSeq scale R) :
    ∃ V : ℕ → ℝ, (∀ n, 0 ≤ V n) ∧ HasSubexponentialUpperBoundSeq scale V ∧
      ∀ n (newCost : S → ℝ) (γ : WordBasisSelections X S),
        (∀ w, newCost w ≤ cost w + ε n) → ∀ v : L,
        ‖(exponentialRescaleBasis (WordBasisSelections.basis X S γ)
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis