OAI/GroupTheory/PolycyclicRecognition/Algebra/IdealProductCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.ideal_basis_bracket_bound line 19

   Source documentation

   The restricted bracket has the same bound as the ambient adapted basis.

   theorem ideal_basis_bracket_bound {C : ℝ}
       (hbr : ∀ i j k, |(basisWithQuotientLifts U.toSubmodule bI bQ lift hlift).repr
         ⁅basisWithQuotientLifts U.toSubmodule bI bQ lift hlift i,
           basisWithQuotientLifts U.toSubmodule bI bQ lift hlift j⁆ k| ≤ C) :
       ∀ i j k, |bI.repr ⁅bI i, bI j⁆ k| ≤ C := by
   …

   Mentions: OAI.PolycyclicRecognition.basisWithQuotientLifts

2. theorem OAI.PolycyclicRecognition.ideal_product_coordinate_bound line 38

   Source documentation

   The ambient product of ideal exponentials remains in the ideal, with an explicit polynomial coordinate bound in its own basis.

   theorem ideal_product_coordinate_bound (C : ℝ) (hC : 0 ≤ C)
       (hbr : ∀ i j k, |bI.repr ⁅bI i, bI j⁆ k| ≤ C)
       {R : ℝ} (hR : 0 ≤ R) (u v : U)
       (hu : ‖bI.equivFun u‖ ≤ R) (hv : ‖bI.equivFun v‖ ≤ R) :
       ∃ w : U, ExpN (w : V) = ExpN (u : V) * ExpN (v : V) ∧
         ‖bI.equivFun w‖ ≤ sectionDynkinConstant (Fintype.card I) c C * (1 + R) ^ c := by
   …

   Mentions: OAI.PolycyclicRecognition.sectionDynkinConstant