OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactSetMeanApproximation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_set_mean_approximation line 17

   Source documentation

   Pairwise concentration and concentration near a prescribed set give one deterministic point of that set whose mean approximation error vanishes.

   theorem exists_set_mean_approximation
       {S Y : Type*} [TopologicalSpace S] [CompactSpace S] [T2Space S]
       [MeasurableSpace S] [BorelSpace S] [PseudoMetricSpace Y]
       (F : S → Y) (hF : Continuous F) (T : Set Y) (hne : T.Nonempty)
       (μ : ℕ → ProbabilityMeasure S)
       (hpair : Tendsto (fun n => ∫ y, ∫ x, dist (F x) (F y)
         ∂(μ n : Measure S) ∂(μ n : Measure S)) atTop (𝓝 0))
       (hset : Tendsto (fun n => ∫ x, infDist (F x) T ∂(μ n : Measure S)) atTop (𝓝 0)) :
       ∃ c : ℕ → Y, (∀ n, c n ∈ T) ∧
         Tendsto (fun n => ∫ x, dist (F x) (c n) ∂(μ n : Measure S)) atTop (𝓝 0) := by
   …

2. theorem OAI.PolycyclicRecognition.pair_mean_tendsto_zero_of_probability line 68

   Source documentation

   On a compact sample space, distance concentration in probability implies the pairwise first-moment hypothesis used above.

   theorem pair_mean_tendsto_zero_of_probability
       {S Y : Type*} [TopologicalSpace S] [CompactSpace S] [SecondCountableTopology S]
       [MeasurableSpace S] [BorelSpace S] [PseudoMetricSpace Y]
       (F : S → Y) (hF : Continuous F) (μ : ℕ → ProbabilityMeasure S)
       (hp : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure S).prod (μ n : Measure S) {p | ε ≤ dist (F p.1) (F p.2)})
           atTop (𝓝 0)) :
       Tendsto (fun n => ∫ y, ∫ x, dist (F x) (F y)
         ∂(μ n : Measure S) ∂(μ n : Measure S)) atTop (𝓝 0) := by
   …

3. theorem OAI.PolycyclicRecognition.set_distance_mean_tendsto_zero_of_probability line 90

   Source documentation

   Compactness also bounds the distance to any fixed nonempty target set.

   theorem set_distance_mean_tendsto_zero_of_probability
       {S Y : Type*} [TopologicalSpace S] [CompactSpace S]
       [MeasurableSpace S] [BorelSpace S] [PseudoMetricSpace Y]
       (F : S → Y) (hF : Continuous F) (T : Set Y)
       (μ : ℕ → ProbabilityMeasure S)
       (hp : ∀ ε : ℝ, 0 < ε → Tendsto (fun n =>
         (μ n : Measure S) {x | ε ≤ infDist (F x) T}) atTop (𝓝 0)) :
       Tendsto (fun n => ∫ x, infDist (F x) T ∂(μ n : Measure S)) atTop (𝓝 0) := by
   …