OAI/GroupTheory/PolycyclicRecognition/Analysis/ConditionedProbeSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.eventually_exists_compact_conditioned_probes line 17

   Source documentation

   The tolerance tends to zero by a slow diagonal choice. The starting profile event may have very small mass; the retained independent probe set still has measure greater than one quarter.

   theorem eventually_exists_compact_conditioned_probes
       {X Y : ℕ → Type*} [∀ n, MeasurableSpace (X n)]
       [∀ n, MeasurableSpace (Y n)] [∀ n, TopologicalSpace (Y n)]
       (μ : ∀ n, Measure (X n)) (ν : ∀ n, Measure (Y n))
       [∀ n, IsProbabilityMeasure (μ n)] [∀ n, IsProbabilityMeasure (ν n)]
       [∀ n, (ν n).InnerRegular]
       (E : ∀ n, ℕ → Set (X n)) (bad : ∀ n, ℕ → Set (X n × Y n))
       (hE : ∀ n j, MeasurableSet (E n j))
       (hbad : ∀ n j, MeasurableSet (bad n j))
       (hpos : ∀ j, ∃ c : ℝ≥0∞, 0 < c ∧ ∀ᶠ n in atTop, c ≤ μ n (E n j))
       (hlim : ∀ j, Tendsto (fun n => (μ n).prod (ν n) (bad n j)) atTop (𝓝 0)) :
       ∃ k : ℕ → ℕ, Tendsto k atTop atTop ∧ ∀ᶠ n in atTop,
   …