ExponentialGoodCells.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Relative mass is unchanged by the actual translated exponential chart

theorem OAI.PolycyclicRecognition.measurableEmbedding_translated_exponential_basis line 24

Source documentation

The translated exponential coordinate map preserves Borel measurability of every independently selected good subset.

theorem measurableEmbedding_translated_exponential_basis
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    {n : ℕ} (b : Basis (Fin n) ℝ L) (k : G) :
    MeasurableEmbedding (fun y => ((Exp ∘ e) ∘ b.equivFun.symm) y * k) := by
…

theorem OAI.PolycyclicRecognition.translated_exponential_cell_ratio line 46

Source documentation

Both the good set and the original cell acquire exactly the same Jacobian, including the deterministic right suffix. No density estimate is lost when the independently sampled coordinate good set is put in the group.

theorem translated_exponential_cell_ratio
    (haar : NilpotentExponentialHaarInput E G)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G) (hnil : LieRing.IsNilpotent L)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    (X : I → L) (words : Finset (FreeMagma I))
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (β : WordBasisSelections X words)
    (cost : words → ℝ) (r : ℝ) (k : G)
    (A Q : Set (Fin (finrank ℝ L) → ℝ)) :
    let μ := Measure.map ((Exp ∘ e) ∘ b₀.equivFun.symm) volume
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.WordBasisSelections