OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryFamilyMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.boundary_family_mass_and_trace_of_compact_shadows line 16

   Source documentation

   The compact shadows provide a single source window with uniform mass and trace bounds. A compact set with interior in the source can be retained inside this window for the subsequent averaging argument.

   theorem boundary_family_mass_and_trace_of_compact_shadows
       {P G S T : Type*} [Group G] [MetricSpace G] [IsTopologicalGroup G]
       [IsIsometricSMul G G] [ProperSpace G]
       [One S] [TopologicalSpace S]
       [Group T] [TopologicalSpace T] [IsTopologicalGroup T] [LocallyCompactSpace T]
       [MeasurableSpace T] [BorelSpace T]
       (actS : G →* Equiv.Perm S) (actT : G →* Equiv.Perm T)
       (hcontS : Continuous (fun g => actS g 1))
       (hcontT : Continuous (fun g => actT g 1))
       (B : P → S → T) (C : P → T → S) (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)
   …