OAI/GroupTheory/PolycyclicRecognition/Analysis/DiagonalAffineCellProfiles.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_diagonal_affine_cell_profiles line 17

   Source documentation

   An exhausting family of interior affine identities, convergent offsets, and supported joint laws produce the actual common good sets needed by the reflection-volume argument, including points over the boundary.

   theorem exists_diagonal_affine_cell_profiles
       {V W N : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W] [MeasurableSpace N]
       (q : V →ₗ[ℝ] W) (hq : Continuous q) (hqsurj : Function.Surjective q)
       (cell : Set W) (hconv : Convex ℝ cell) (hclosed : IsClosed cell)
       (hint : (interior cell).Nonempty)
       (S : Set C(V, W)) [MeasurableSpace S] [BorelSpace S]
       [BorelSpace (S × S)] [HasOuterApproxClosed (S × S)]
       (K : ℕ → Set V) (hK : ∀ j, IsCompact (K j))
       (hcover : ∀ C : Set V, IsCompact C → ∀ᶠ j in atTop, C ⊆ K j)
       (scale : ℕ → ℕ → ℝ) (hs : ∀ j, Tendsto (scale j) atTop atTop)
       (μ : Measure N) (Q : ℕ → ℕ → Set N)
   …