OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactProbeSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.choose_compact_good_probe_sequence line 16

   Source documentation

   Extend the eventual Fubini selection to sequences defined at every scale. Initial exceptional scales use the full compact probability space; the actual good-probe property is retained eventually.

   theorem choose_compact_good_probe_sequence
       {X : Type*} [Nonempty X] {Y : ℕ → Type*}
       [∀ n, TopologicalSpace (Y n)] [∀ n, CompactSpace (Y n)]
       [∀ n, T2Space (Y n)] [∀ n, MeasurableSpace (Y n)] [∀ n, BorelSpace (Y n)]
       (ν : ∀ n, ProbabilityMeasure (Y n)) (Good : ∀ n, X → Set (Y n) → Prop)
       (h : ∀ᶠ n in atTop, ∃ x K, IsCompact K ∧ Good n x K ∧
         (1 / 4 : ℝ≥0∞) < (ν n : Measure (Y n)) K) :
       ∃ (x : ℕ → X) (K : ∀ n, Set (Y n)),
         (∀ n, IsCompact (K n) ∧ MeasurableSet (K n) ∧
           (1 / 4 : ℝ≥0∞) < (ν n : Measure (Y n)) (K n)) ∧
         ∀ᶠ n in atTop, Good n (x n) (K n) := by
   …