OAI/GroupTheory/PolycyclicRecognition/Analysis/IndependentSupportedSampling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.independent_supported_bad_probability_tendsto_zero line 15

   Source documentation

   Sequential concentration for every permitted deterministic suffix implies concentration for any independent laws carried by those sets.

   theorem independent_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, ∀ᵐ 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
   …