OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPolarOffsetExponents.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.sum_polar_ideal_cost_smul line 20
2. theorem OAI.PolycyclicRecognition.CartanWordModel.polar_templateSupport_eq line 36

   Source documentation

   The common source maximizing basis computes every polar radius.

   theorem polar_templateSupport_eq (K : ProperCone ℝ (StrongDual ℝ W))
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal (heightConePreimage T eW K))))
         ℝ (M.coneWordIdeal (heightConePreimage T eW K)))
       (β : M.ConeIdealBases (heightConePreimage T eW K))
       (hβ : M.IsMaximizingConeIdealBasis (heightConePreimage T eW K) bI
         (M.polarProbeWidths T hunimod eW K) β) {c : ℝ} (hc : 0 ≤ c) :
       (M.supportIn T hunimod eW).templateSupport
         ((fun x : W => c • x) '' conePolarTemplate K) =
         c * ∑ j, M.coneIdealWordCost (heightConePreimage T eW K)
           (M.polarProbeWidths T hunimod eW K) (β.val j) := by
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage, OAI.PolycyclicRecognition.conePolarTemplate

3. theorem OAI.PolycyclicRecognition.CartanWordModel.polar_offset_exponent_balance line 63

   Source documentation

   Source radius 2ε/3, target radius ε/3, and the actual tiling rate have exactly matching exponents. The target cone and its dimension may differ.

   theorem polar_offset_exponent_balance (K : ProperCone ℝ (StrongDual ℝ W))
       (A : templateSymmetryGroup (M.supportIn T hunimod eW))
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal (heightConePreimage T eW K))))
         ℝ (M.coneWordIdeal (heightConePreimage T eW K)))
       (β : M.ConeIdealBases (heightConePreimage T eW K))
       (hβ : M.IsMaximizingConeIdealBasis (heightConePreimage T eW K) bI
         (M.polarProbeWidths T hunimod eW K) β)
       (bI' : Basis (Fin (finrank ℝ
         (M.coneWordIdeal (heightConePreimage T eW (transformedPolarCone K A.val)))))
         ℝ (M.coneWordIdeal (heightConePreimage T eW (transformedPolarCone K A.val))))
       (β' : M.ConeIdealBases (heightConePreimage T eW (transformedPolarCone K A.val)))
   …

   Mentions: OAI.PolycyclicRecognition.templateSymmetryGroup, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage, OAI.PolycyclicRecognition.transformedPolarCone