CartanPolarSourceCells.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Source volume on the original cells of the polar samplers

theorem OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.source_cell_volumes line 40

Source documentation

The exact positive source volume belongs to the same original quotient and kernel cells used by the counted sampler.

theorem PolarTiledSamplerData.source_cell_volumes
    (eI : M.coneWordIdeal C ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EI)) I)
    (ExpI : GroupLieAlgebra (𝓘(ℝ, EI)) I → I) (hExpI : IsGroupExponential ExpI)
    (haarI : NilpotentExponentialHaarInput EI I)
    (chartI : GroupLieAlgebra (𝓘(ℝ, EI)) I ≃ₜ I) (hchartI : ∀ v, chartI v = ExpI v)
    (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
    (πQ : F.N.carrier →* Q.carrier) (ι : I →* F.N.carrier)
    (hι : Topology.IsClosedEmbedding ι) (hrange : range ι = (πQ.ker : Set F.N.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) β)
…

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