OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialCellMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.translated_exponential_cell_mass line 15

   Source documentation

   Every positive finite coordinate cell gives a positive finite Haar cell, with no restriction on the scale or the deterministic right suffix.

   theorem translated_exponential_cell_mass
       {L E N I : Type*} [LieRing L] [LieAlgebra ℝ L]
       [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
       [TopologicalSpace N] [ChartedSpace E N] [Group N]
       [LieGroup (𝓘(ℝ, E)) ⊤ N] [T2Space N] [SimplyConnectedSpace N]
       [MeasurableSpace N] [BorelSpace N]
       (haar : NilpotentExponentialHaarInput E N)
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) N) (hnil : LieRing.IsNilpotent L)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) N → N) (hExp : IsGroupExponential Exp)
       (chart : GroupLieAlgebra (𝓘(ℝ, E)) N ≃ₜ N) (hchart : ∀ x, chart x = Exp x)
       (X : I → L) (words : Finset (FreeMagma I))
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (β : WordBasisSelections X words)
   …

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

2. theorem OAI.PolycyclicRecognition.coordinate_cube_mass line 57

   Source documentation

   The finite-dimensional closed coordinate cube has positive finite mass.

   theorem coordinate_cube_mass {n : ℕ} {R : ℝ} (hR : 0 < R) :
       volume (Icc (fun _ : Fin n => -R) (fun _ => R)) ≠ 0 ∧
         volume (Icc (fun _ : Fin n => -R) (fun _ => R)) ≠ ∞ := by
   …