TranslatedBoxMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Volume ratios for translated exponential boxes

theorem OAI.PolycyclicRecognition.measure_image_mul_right line 16
Source documentation
Right translation preserves the measure of every set, including sets whose measurability has not yet been established separately.
```
theorem measure_image_mul_right {G : Type*} [Group G] [MeasurableSpace G]
    [MeasurableMul G] (μ : Measure G) [μ.IsMulRightInvariant] (S : Set G) (k : G) :
    μ ((fun x => x * k) '' S) = μ S := by
…
```

theorem OAI.PolycyclicRecognition.exponential_box_radius_measure line 30

Source documentation

Enlarging the radius of a fixed exponential box multiplies its Haar volume by exactly the corresponding power, independently of the scale.

theorem exponential_box_radius_measure
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    {n : ℕ} (b₀ b : Basis (Fin n) ℝ L) {R : ℝ} (hR : 0 ≤ R) :
    (Measure.map ((Exp ∘ e) ∘ b₀.equivFun.symm) volume)
      (exponentialCoordinateBox (Exp ∘ e) b R) =
      ENNReal.ofReal (R ^ n) *
        (Measure.map ((Exp ∘ e) ∘ b₀.equivFun.symm) volume)
          (exponentialCoordinateBox (Exp ∘ e) b 1) := by
…

Mentions: OAI.PolycyclicRecognition.exponentialCoordinateBox

theorem OAI.PolycyclicRecognition.translated_box_increment_mem line 52

Source documentation

The conjugated increment lies in a small box; hence the translated source box times that increment lies in the translated product box.

theorem translated_box_increment_mem {G : Type*} [Group G]
    {B R : Set G} (hprod : ∀ x ∈ B, ∀ y ∈ B, x * y ∈ R)
    (k s : G) (hs : k * s * k⁻¹ ∈ B) {x : G}
    (hx : x ∈ (fun y => y * k) '' B) :
    x * s ∈ (fun y => y * k) '' R := by
…