OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRayBoundaryMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.RayBoundaryModel.exists_mass_and_equal_set_trace line 24

   Source documentation

   The common shadow bounds produce a compact source window with nonempty interior and both of the uniform inequalities used in the leaf/trace proof.

   theorem RayBoundaryModel.exists_mass_and_equal_set_trace
       (B : P → RS.cone.Q.carrier ≃ₜ RT.cone.Q.carrier) (f g : P → G → G)
       {Lf Lg ef eg E : ℝ} (hLf : 0 ≤ Lf) (hLg : 0 ≤ Lg)
       (hf : ∀ p x y, dist (f p x) (f p y) ≤ Lf * dist x y + ef)
       (hg : ∀ p x y, dist (g p x) (g p y) ≤ Lg * dist x y + eg)
       (hinv : ∀ p x, dist (g p (f p x)) x ≤ E)
       (KS : Set RS.cone.Q.carrier) (KT : Set RT.cone.Q.carrier)
       (hKS : IsCompact KS) (hKT : IsCompact KT)
       (hB : ∀ p x, ∃ z ∈ KT, B p (RS.action x 1) = RT.action (f p x) z)
       (hC : ∀ p x, ∃ z ∈ KS, (B p).symm (RT.action x 1) = RS.action (g p x) z)
       (μ : Measure RT.cone.Q.carrier) [μ.IsHaarMeasure] (height : G → ℝ)
       (hvolume : ∀ x V, μ (RT.action x '' V) =
   …