OAI/GroupTheory/PolycyclicRecognition/Analysis/DeterministicProfileCenters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_deterministic_profile_centers line 16

   Source documentation

   The first-moment method chooses one deterministic profile whose mean error is no larger than the error between two independent profiles.

   theorem exists_deterministic_profile_centers
       {S Y : Type*} [TopologicalSpace S] [CompactSpace S] [T2Space S]
       [MeasurableSpace S] [BorelSpace S] [PseudoMetricSpace Y]
       (F : S → Y) (hF : Continuous F) (μ : ℕ → ProbabilityMeasure S) :
       ∃ center : ℕ → S, ∀ n,
         (∫ x, dist (F x) (F (center n)) ∂(μ n : Measure S)) ≤
           ∫ y, ∫ x, dist (F x) (F y) ∂(μ n : Measure S) ∂(μ n : Measure S) := by
   …

2. theorem OAI.PolycyclicRecognition.exists_deterministic_concentration_centers line 37

   Source documentation

   Vanishing mean pairwise distance gives deterministic centers with vanishing mean error. The centers may be selected independently at each scale.

   theorem exists_deterministic_concentration_centers
       {S Y : Type*} [TopologicalSpace S] [CompactSpace S] [T2Space S]
       [MeasurableSpace S] [BorelSpace S] [PseudoMetricSpace Y]
       (F : S → Y) (hF : Continuous F) (μ : ℕ → ProbabilityMeasure S)
       (hpair : Tendsto (fun n =>
         ∫ y, ∫ x, dist (F x) (F y) ∂(μ n : Measure S) ∂(μ n : Measure S))
         atTop (𝓝 0)) :
       ∃ center : ℕ → S, Tendsto (fun n =>
         ∫ x, dist (F x) (F (center n)) ∂(μ n : Measure S)) atTop (𝓝 0) := by
   …