OAI/GroupTheory/PolycyclicRecognition/Analysis/EventualSupportedSampling.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.independent_eventually_supported_bad_probability_tendsto_zero line 15

   Source documentation

   The initial finitely many laws need not be carried by the permitted sets. The same selection argument applies after the eventual support bound.

   theorem independent_eventually_supported_bad_probability_tendsto_zero
       {A K : ℕ → Type*} [∀ n, MeasurableSpace (A n)] [∀ n, MeasurableSpace (K n)]
       (μ : ∀ n, ProbabilityMeasure (A n)) (ν : ∀ n, ProbabilityMeasure (K n))
       (D : ∀ n, Set (K n)) (hne : ∀ n, (D n).Nonempty)
       (hcarried : ∀ᶠ n in atTop, ∀ᵐ k ∂(ν n : Measure (K n)), k ∈ D n)
       (B : ∀ n, Set (A n × K n)) (hB : ∀ n, MeasurableSet (B n))
       (hp : ∀ k : ∀ n, K n, (∀ n, k n ∈ D n) →
         Tendsto (fun n => (μ n : Measure (A n)) ((fun a => (a, k n)) ⁻¹' B n))
           atTop (𝓝 0)) :
       Tendsto (fun n => (μ n : Measure (A n)).prod (ν n : Measure (K n)) (B n))
         atTop (𝓝 0) := by
   …

2. theorem OAI.PolycyclicRecognition.exists_eventually_chosen_sequence line 48

   Source documentation

   Choose the actual eventual geometric witnesses, filling unused early indices arbitrarily.

   theorem exists_eventually_chosen_sequence
       {X : ℕ → Type*} [∀ n, Nonempty (X n)] (P : ∀ n, X n → Prop)
       (hP : ∀ᶠ n in atTop, ∃ x, P n x) :
       ∃ x : ∀ n, X n, ∀ᶠ n in atTop, P n (x n) := by
   …