OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryVolumeTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.boundary_trace_bound_of_sandwich line 17

   Source documentation

   Equal source boundary sets have equal images. A fixed positive lower volume and finite upper volume then bound the difference of the two logarithmic Haar characters. The constant is independent of the map.

   theorem boundary_trace_bound_of_sandwich
       {P G S T : Type*} [Group G] [MeasurableSpace T]
       (actS : G →* Equiv.Perm S) (actT : G →* Equiv.Perm T)
       (B : P → S → T) (f : P → G → G) (μ : Measure T) (height : G → ℝ)
       (hvolume : ∀ g E, μ (actT g '' E) = ENNReal.ofReal (Real.exp (height g)) * μ E)
       (U : Set S) (Vminus Vplus : Set T)
       (hVminus0 : μ Vminus ≠ 0) (hVminusfinite : μ Vminus ≠ ⊤) (hVplusfinite : μ Vplus ≠ ⊤)
       (hsandwich : ∀ p x, actT (f p x) '' Vminus ⊆ B p '' (actS x '' U) ∧
         B p '' (actS x '' U) ⊆ actT (f p x) '' Vplus) :
       ∃ K : ℝ, 0 ≤ K ∧ ∀ p x y, actS x '' U = actS y '' U →
         |height (f p x) - height (f p y)| ≤ K := by
   …