CartanSelectedProbePaths.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Image paths for the selected actual probe chains

theorem OAI.PolycyclicRecognition.CartanWordModel.BoxProbeChains.ambient_step line 30

Source documentation

Inclusion into the ambient group retains the exact generator edge of the measured box chain, also after left translation by an anchor.

theorem BoxProbeChains.ambient_step
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E : Set W) (γ : M.Bases) (t : Fin M.letterCount → ℝ) (scale : ℕ → ℝ)
    {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)
    (n : ℕ) (y : Y n) (g : G) (j : Fin P.length) :
    g * F.inclusionN (F.ExpN (F.N.equiv (P.vertex n y j.succ))) =
      (g * F.inclusionN (F.ExpN (F.N.equiv (P.vertex n y j.castSucc)))) *
        Exp (P.coefficient n y j • (M.letter (P.mode n j) :
          GroupLieAlgebra (𝓘(ℝ, EG)) G)) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_selected_probe_paths line 49
Source documentation
One compact profile domain works for all three actual box chains and for arbitrary measurable anchor choices. On a retained good probe, the paths start at the corresponding anchors and end at the actual samplers. The only profile premise is the prefix estimate supplied by selection.
```
theorem exists_selected_probe_paths
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput