OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCellTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.map_cube_eq_translated_groupBox_probability line 26
2. theorem OAI.PolycyclicRecognition.CartanWordModel.cube_profile_law_eq_cell_profile_law line 66

   Source documentation

   A raw sheet-profile law can equivalently be sampled in the standard coordinate cube. This transfers the coordinate affinity theorem to the original Haar cell without changing either probability law.

   theorem cube_profile_law_eq_cell_profile_law
       (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 : ℝ) (k : F.N.carrier)
       {X : Type*} [MeasurableSpace X] (profile : F.N.carrier → X) (hp : Measurable profile) :
       let cube := Icc (fun _ : Fin (finrank ℝ (cartanRootIdeal H)) => (-1 : ℝ)) (fun _ => (1 : ℝ))
   …

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

3. theorem OAI.PolycyclicRecognition.CartanWordModel.translated_groupBox_profile_law_mul_right line 90

   Source documentation

   Right translation of a sheet changes its deterministic suffix and preserves the original coordinate-cube sampling law exactly.

   theorem translated_groupBox_profile_law_mul_right
       [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 : ℝ) (k₀ k : F.N.carrier)
       {X : Type*} [MeasurableSpace X] (profile : F.N.carrier → X) (hp : Measurable profile) :
       ProbabilityMeasure.map
         (M.translatedGroupBoxProbability T F hunimod eW haarN chartN hchartN b₀ E β r k₀)
         (fun q => profile (q * k)) = ProbabilityMeasure.map
         (M.translatedGroupBoxProbability T F hunimod eW haarN chartN hchartN b₀ E β r (k₀ * k))
   …

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