CartanPolarSourceVolumes.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Source volume and tile count with the same actual exponent

theorem OAI.PolycyclicRecognition.CartanWordModel.polar_source_kernel_exponent line 34

Source documentation

The source ideal exponent equals the ambient template exponent at the actual first radius. This is the equality needed for volume cancellation.

theorem polar_source_kernel_exponent
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
    (β : M.ConeIdealBases C)
    (hβ : M.IsMaximizingConeIdealBasis C bI (M.polarProbeWidths T hunimod eW K) β)
    {ε : ℝ} (hε : 0 ≤ ε) :
    (∑ j, M.coneIdealWordCost C
      ((M.supportIn T hunimod eW).weightSupport (normalizedPolarTemplates K ε 0))
      (β.val j)) = (M.supportIn T hunimod eW).templateSupport
        (normalizedPolarTemplates K ε 0) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.normalizedPolarTemplates

theorem OAI.PolycyclicRecognition.CartanWordModel.polar_source_cell_volumes line 52

Source documentation

The positive source coefficient and the exact source exponential rate are derived for the kernel measure actually used in the source count.

theorem polar_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)
    (π : F.N.carrier →* Q) (ι : I →* F.N.carrier)
    (hι : Topology.IsClosedEmbedding ι) (hrange : range ι = (π.ker : Set F.N.carrier))
    (μI : Measure I) [μI.IsHaarMeasure]
    (μQ : Measure Q) [μQ.IsOpenPosMeasure] [IsFiniteMeasureOnCompacts μQ]
    {d : ℕ} (eQ : (Fin d → ℝ) ≃ₜ Q)
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
…

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