OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCellPairLaws.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.neighboring_cell_marginal_limits line 28

   Source documentation

   A joint neighboring-sheet limit has precisely the two marginal limits obtained by sampling the translated cells with suffixes k₀ and k₀ * k. Thus the single-sheet affinity theorem applies to both components.

   theorem neighboring_cell_marginal_limits
       [IsTopologicalGroup F.N.carrier]
       (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
       (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
       (hchartN : ∀ x, chartN x = F.ExpN x)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Set W) (β : M.Bases) (scale : ℕ → ℝ) (k₀ k : ℕ → F.N.carrier)
       {S : Type*} [TopologicalSpace S] [MeasurableSpace S] [BorelSpace S] [BorelSpace (S × S)]
       (profile : ℕ → F.N.carrier → S) (hp : ∀ n, Measurable (profile n))
       (ν : ProbabilityMeasure (S × S))
       (hν : Tendsto (fun n => ProbabilityMeasure.map
         (M.translatedGroupBoxProbability T F hunimod eW haarN chartN hchartN b₀ E β (scale n) (k₀ n))
   …

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