OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPolarSourceProbability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.source_probability_data line 33

   Source documentation

   The measured cone and counted sampler supply the original probability cell, its positive exponential volume, and all regularity needed for concentration. No probability law or volume bound is added as an input.

   theorem PolarTiledSamplerData.source_probability_data
       (D : M.MeasuredCone F C)
       (haarI : NilpotentExponentialHaarInput D.I.modelSpace D.I.carrier)
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       {ε : ℝ} (hε : 0 ≤ ε) (β : M.ConeIdealBases C)
       (hβ : M.IsMaximizingConeIdealBasis C bI (M.polarProbeWidths T hunimod eW K) β)
       (R : ℝ) (scale : ℕ → ℝ) (φ : ℕ → D.I.carrier ≃ₜ* D.I.carrier)
       (P : M.PolarTiledSamplerData T F hunimod eW K
         (D.maps.expI ∘ D.I.equiv) D.maps.inclusion bN ε β R scale φ) :
       let Z := TiledProbeChainData.sourceQuotientCell
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceQuotientCell