OAI/GroupTheory/PolycyclicRecognition/Geometry/WeightedBasisComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_uniform_rescaled_basis_comparison line 19

   Source documentation

   A fixed constant controls every selected word basis in every maximizing basis, at all nonnegative scales. Thus a varying basis in a sampling row can be replaced by the fixed maximizing basis without an exponential loss.

   theorem exists_uniform_rescaled_basis_comparison
       (X : I → L) (S : Finset (FreeMagma I))
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) :
       ∃ C : ℝ, 1 ≤ C ∧ ∀ (cost : S → ℝ) (β γ : WordBasisSelections X S),
         IsMaximizingColumnBasis (wordListCoordinates X S b₀) cost β.val →
         ∀ r : ℝ, 0 ≤ r → ∀ x : L,
           ‖(exponentialRescaleBasis (WordBasisSelections.basis X S β)
             (fun j => cost (β.val j)) r).equivFun x‖ ≤
           C * ‖(exponentialRescaleBasis (WordBasisSelections.basis X S γ)
             (fun j => cost (γ.val j)) r).equivFun x‖ := by
   …

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