CartanBoxProbeChains.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Measurable chains for actual group-valued probes

structure OAI.PolycyclicRecognition.CartanWordModel.BoxProbeChains line 27

Source documentation

The data retained for each of the three probe templates. The common length and constants are independent of the scale and the probe point.

structure BoxProbeChains
    (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) where
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_actual_box_probe_chains line 57
Source documentation
Actual Borel probe endpoints in the group box admit simultaneous measurable generator chains. Coordinates are recovered through the published exponential homeomorphism, so no logarithmic sampler is assumed.
```
theorem exists_actual_box_probe_chains
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput

def OAI.PolycyclicRecognition.CartanWordModel.BoxProbeChains.reparametrize line 127

Source documentation

Use the original quotient/kernel probability cell as the probe space. Measurable reparametrization keeps every prefix, coefficient and endpoint, so the independent probe law can be chosen directly on that cell.

def BoxProbeChains.reparametrize
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E : Set W) (γ : M.Bases) (t : Fin M.letterCount → ℝ) (scale : ℕ → ℝ)
    {Y Z : ℕ → Type*} [∀ n, MeasurableSpace (Y n)] [∀ n, MeasurableSpace (Z n)]
    (probe : ∀ n, Y n → F.N.carrier)
    (P : M.BoxProbeChains T F hunimod eW b₀ E γ t scale probe)
    (ψ : ∀ n, Z n → Y n) (hψ : ∀ n, Measurable (ψ n)) :
    M.BoxProbeChains T F hunimod eW b₀ E γ t scale (fun n z => probe n (ψ n z)) where
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.nonempty_boxProbeChains line 153
Source documentation
Package the actual chains so the three templates can share their samplers while retaining their individual fixed lengths.
```
theorem nonempty_boxProbeChains
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput