OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryImageMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.boundary_image_mass_bounds line 15

   Source documentation

   A compact lower/upper sandwich gives one positive comparison constant for the absolute boundary image masses throughout the map family.

   theorem boundary_image_mass_bounds
       {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,
         ENNReal.ofReal (Real.exp (height (f p x))) ≤
           ENNReal.ofReal K * μ (B p '' (actS x '' U)) ∧
   …

2. theorem OAI.PolycyclicRecognition.exponential_mass_bounds_of_abs_sub_le line 64

   Source documentation

   A bounded change of scalar height changes its exponential mass by one uniform multiplicative constant.

   theorem exponential_mass_bounds_of_abs_sub_le
       {a b K C : ℝ} {m : ℝ≥0∞} (hK : 0 ≤ K)
       (hab : |a - b| ≤ C)
       (hlower : ENNReal.ofReal (Real.exp a) ≤ ENNReal.ofReal K * m)
       (hupper : m ≤ ENNReal.ofReal K * ENNReal.ofReal (Real.exp a)) :
       ENNReal.ofReal (Real.exp b) ≤ ENNReal.ofReal (K * Real.exp C) * m ∧
         m ≤ ENNReal.ofReal (K * Real.exp C) * ENNReal.ofReal (Real.exp b) := by
   …