ExponentialSubsetVolume.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Volume of arbitrary subsets in rescaled exponential coordinates

The change-of-coordinates determinant formula applies to the independently sampled good subset, not just to an entire box. The exponential chart is a measurable embedding, so this calculation does not assume absolute continuity of an arbitrarily selected word parametrization.

theorem OAI.PolycyclicRecognition.exponential_basis_image_eq line 24

Source documentation

Change of exponential basis on an arbitrary coordinate set.

theorem exponential_basis_image_eq
    {G : Type*} (Exp : L → G) (b₀ b : Basis (Fin n) ℝ L) (S : Set (Fin n → ℝ)) :
    (Exp ∘ b.equivFun.symm) '' S =
      (Exp ∘ b₀.equivFun.symm) '' ((Matrix.toLin' (b₀.toMatrix b)) '' S) := by
…

theorem OAI.PolycyclicRecognition.exponential_basis_subset_measure line 44

Source documentation

The exact determinant formula for every coordinate subset in the global nilpotent exponential chart.

theorem exponential_basis_subset_measure
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    (b₀ b : Basis (Fin n) ℝ L) (S : Set (Fin n → ℝ)) :
    (Measure.map ((Exp ∘ e) ∘ b₀.equivFun.symm) volume)
      (((Exp ∘ e) ∘ b.equivFun.symm) '' S) =
      ENNReal.ofReal |(b₀.toMatrix b).det| * volume S := by
…

theorem OAI.PolycyclicRecognition.exponential_rescaled_subset_measure line 70

Source documentation

The full exponential determinant remains valid after discarding any bad coordinate subset from the independently sampled domain.

theorem exponential_rescaled_subset_measure
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G)
    (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 : ℝ) (S : Set (Fin (finrank ℝ L) → ℝ)) :
    (Measure.map ((Exp ∘ e) ∘ b₀.equivFun.symm) volume)
      (((Exp ∘ e) ∘ (exponentialRescaleBasis (WordBasisSelections.basis X words β)
        (fun j => cost (β.val j)) r).equivFun.symm) '' S) =
      ENNReal.ofReal |(columnBasisMatrix (wordListCoordinates X words b₀) β.val).det| *
        ENNReal.ofReal (Real.exp (r * columnBasisWeight cost β.val)) * volume S := by
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.columnBasisWeight