OAI/GroupTheory/PolycyclicRecognition/Algebra/BackwardRecurrenceSets.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_backward_recurrence_sets line 17

   Source documentation

   Iterating the quantitative return estimate backwards produces the nested sets used in the segment-volume argument. The number and order of the increment laws are fixed before this construction.

   theorem exists_backward_recurrence_sets
       {G : Type*} [Group G] [MeasurableSpace G] [MeasurableMul₂ G] [MeasurableInv G]
       (μ : Measure G) [SFinite μ] [μ.IsMulRightInvariant]
       (σ : ℕ → Measure G) [∀ j, IsProbabilityMeasure (σ j)]
       (Q : Set G) (hQfin : μ Q ≠ ∞) (hQpos : 0 < (μ Q).toReal)
       (K R : ℕ → Set G) (hK : ∀ j, ∀ᵐ s ∂σ j, s ∈ K j)
       (hRfin : ∀ j, μ (R j) ≠ ∞) (hRpos : ∀ j, 0 < (μ (R j)).toReal)
       (hQR : ∀ j, ∀ a ∈ Q, ∀ s ∈ K j, a * s ∈ R j)
       (D : ℕ → ℝ) (hD : ∀ j, 0 < D j)
       (hvol : ∀ j, (μ (R j)).toReal ≤ D j * (μ Q).toReal)
       (h : ℕ) (A : Set G) (hA : MeasurableSet A) (hAQ : A ⊆ Q)
       (hApos : 0 < (μ A).toReal) :
   …