OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanAllowedProbeChains.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.CartanWordModel.BoxProbeChains.inSamplingBox line 32

   Source documentation

   Reexpress an actual probe chain in the enlarged sampling basis. The word-basis comparison gives a constant radius for every prefix; all endpoints, coefficients and generator edges are preserved.

   def BoxProbeChains.inSamplingBox
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E C : Set W) (γ β : M.Bases) (t : Fin M.letterCount → ℝ)
       (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
         (M.boxCost T hunimod eW C) β.val)
       (ht : ∀ i, t i ≤ (M.supportIn T hunimod eW).weightSupport C i)
       (hw : ∀ i, 0 ≤ (M.supportIn T hunimod eW).weightSupport C i)
       {δ : ℝ} (hδ : 0 ≤ δ) (scale : ℕ → ℝ) (hr : ∀ n, 0 ≤ scale n)
       {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)]
       (probe : ∀ n, Y n → F.N.carrier)
       (P : M.BoxProbeChains T F hunimod eW b₀ E γ t scale probe) :
       M.BoxProbeChains T F hunimod eW b₀ E β
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates

2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_probe_switch_height line 92

   Source documentation

   Compact containment of the generator template supplies the strict switching heights in the actual Cartan profile coordinates.

   theorem exists_probe_switch_height
       {J : Type*} [Fintype J]
       (bD : Basis J ℝ H) (E U : Set W) (hE : IsCompact E) (hne : E.Nonempty)
       (hU : IsOpen U) (hEU : E ⊆ U) (i : Fin M.letterCount) :
       ∃ z : J → ℝ,
         eW (heightProjection T.character (bD.equivFun.symm z :
           GroupLieAlgebra (𝓘(ℝ, EG)) G)) ∈ U ∧
         (M.supportIn T hunimod eW).weightSupport E i < M.weight i (bD.equivFun.symm z) := by
   …

   Mentions: OAI.PolycyclicRecognition.heightProjection