OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborFrameLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.cube_neighbor_frame_law line 29

   Source documentation

   Sampling the two fixed endpoints with one cube variable is exactly the original neighboring Haar-cell law, with its original base and step.

   theorem cube_neighbor_frame_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 : ∀ x, chartN x = F.ExpN x)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Set W) (β : M.Bases) (r : ℝ)
       (base finish step : F.N.carrier) (hfinish : finish = base * step)
       {X : Type*} [MeasurableSpace X]
       (profile : F.N.carrier → X) (hp : Measurable profile) :
       ProbabilityMeasure.map
         (cellProbabilityMeasure volume
   …

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