CartanPolarLinkedSource.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Linking the actual polar samplers at the original neighboring cells

theorem OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.linked_chains_from_neighbor_boxes line 40

Source documentation

Dilation and enlarged-box containment turn the stored polar samplers into the linked chains used by concentration. The logarithmic base points and their common vanishing error are constructed from the original boxes.

theorem PolarTiledSamplerData.linked_chains_from_neighbor_boxes
    (ExpI : M.coneWordIdeal C → I) (ι : I →* F.N.carrier)
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {ε : ℝ} (hε : 0 ≤ ε) (β : M.ConeIdealBases C)
    (Rbox : ℝ) (scale : ℕ → ℝ) (φ : ℕ → I ≃ₜ* I)
    (D : M.PolarTiledSamplerData T F hunimod eW K ExpI ι bN ε β Rbox scale φ)
    {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)]
    (ψ : ∀ n, Y n →
      (closedBall (0 : Fin (finrank ℝ
        (cartanRootIdeal H ⧸ (M.coneWordIdeal C).toSubmodule)) → ℝ) 1) ×
      (M.coneIdealBox C ExpI
        ((M.supportIn T hunimod eW).weightSupport (normalizedPolarTemplates K ε 0))
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.normalizedPolarTemplates