OAI/GroupTheory/PolycyclicRecognition/Analysis/DeterministicProbabilityComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.deterministic_distance_tendsto_zero_of_probability line 14

   Source documentation

   A constant event cannot have vanishing positive probability unless its deterministic error tends to zero.

   theorem deterministic_distance_tendsto_zero_of_probability
       {X Y : Type*} [MeasurableSpace X] [PseudoMetricSpace Y]
       (μ : ℕ → ProbabilityMeasure X) (a b : ℕ → Y)
       (hp : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure X) {_x | ε ≤ dist (a n) (b n)}) atTop (𝓝 0)) :
       Tendsto (fun n => dist (a n) (b n)) atTop (𝓝 0) := by
   …

2. theorem OAI.PolycyclicRecognition.deterministic_distance_tendsto_zero_of_coupled_profiles line 35

   Source documentation

   Two deterministic approximants agree asymptotically when their sampled profiles can be compared on a common probability law.

   theorem deterministic_distance_tendsto_zero_of_coupled_profiles
       {X Y : Type*} [MeasurableSpace X] [PseudoMetricSpace Y]
       (μ : ℕ → ProbabilityMeasure X) (a b : ℕ → Y) (f g : ℕ → X → Y)
       (hleft : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure X) {x | ε ≤ dist (a n) (f n x)}) atTop (𝓝 0))
       (hpair : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure X) {x | ε ≤ dist (f n x) (g n x)}) atTop (𝓝 0))
       (hright : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure X) {x | ε ≤ dist (g n x) (b n)}) atTop (𝓝 0)) :
       Tendsto (fun n => dist (a n) (b n)) atTop (𝓝 0) := by
   …