CartanDilatedProbeChains.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transporting actual probe chains to the contact pivot

def OAI.PolycyclicRecognition.CartanWordModel.BoxProbeChains.dilate line 28

Source documentation

Exact dilation transports all measurable prefixes, generator amplitudes and endpoints. The chain length and prefix radius are unchanged.

def BoxProbeChains.dilate
    (hbij : Function.Bijective F.ExpN)
    (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E B : Set W) (hE : IsCompact E) (hne : E.Nonempty)
    (hB : IsCompact B) (hBne : B.Nonempty) (w : W)
    (γ : M.Bases) (scale : ℕ → ℝ)
    {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)]
    (probe : ∀ n, Y n → F.N.carrier)
    (P : M.BoxProbeChains T F hunimod eW b₀ E γ
      ((M.supportIn T hunimod eW).weightSupport B) scale probe) :
    M.BoxProbeChains T F hunimod eW b₀ ((fun x => x + w) '' E) γ
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.cartanRootIdeal