CartanRestrictedNeighborLaw.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The neighboring law in the coordinates of the linked probe selection

theorem OAI.PolycyclicRecognition.CartanWordModel.restricted_neighbor_cube_law line 30

Source documentation

The actual Haar neighboring law gives the joint coordinate-cube law of the two original profiles restricted to any compact probe-height set. Supported pairs remain supported. No new limiting-law assumption is used.

theorem restricted_neighbor_cube_law
    [IsTopologicalGroup F.N.carrier]
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
    (hchartN : ∀ v, chartN v = F.ExpN v)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E : Set W) (β : M.Bases) (scale r : ℕ → ℝ)
    (base step : ℕ → F.N.carrier) (origin next : ℕ → cartanRootIdeal H)
    (horigin : ∀ n, F.ExpN (F.N.equiv (origin n)) = base n)
    (hnext : ∀ n, F.ExpN (F.N.equiv (next n)) = base n * step n)
    (hD : Continuous F.ExpD) (J : ℕ → G → W) (hJ : ∀ n, Continuous (J n))
    (x : ℕ → G) (bD : ℕ → Basis (Fin (finrank ℝ H)) ℝ H)
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanRootIdeal