OAI/GroupTheory/PolycyclicRecognition/Analysis/GoodProfileSampling.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_good_sampled_observations line 18

   Source documentation

   Pull the shrinking neighborhoods back to the actual independent sample space. Every retained sample approximates the prescribed supported profile, and their probability still has a subexponential lower bound.

   theorem exists_good_sampled_observations
       {X A E : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
       [HasOuterApproxClosed X] [MeasurableSpace A] [NormedAddCommGroup E]
       (samples : ℝ → ProbabilityMeasure A) (profile : ℝ → A → X)
       (hp : ∀ r, Measurable (profile r)) (ν : ProbabilityMeasure X)
       (hν : Tendsto (fun r => ProbabilityMeasure.map (samples r) (profile r)) atTop (𝓝 ν))
       {f : X} (hf : f ∈ (ν : Measure X).support) (observe : C(X, E)) :
       ∃ (B : ℝ → Set A) (ε : ℝ → ℝ),
         (∀ r, MeasurableSet (B r)) ∧ (∀ r, 0 < ε r) ∧ Tendsto ε atTop (𝓝 0) ∧
         HasSubexponentialLowerBound (fun r => ((samples r : Measure A) (B r)).toReal) ∧
         ∀ r a, a ∈ B r → ‖observe (profile r a) - observe f‖ < ε r := by
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound

2. theorem OAI.PolycyclicRecognition.exists_good_sampled_profiles line 55

   Source documentation

   The observable needed in the segment argument is restriction of a continuous profile to one fixed compact set. Its norm is the uniform norm.

   theorem exists_good_sampled_profiles
       {V W A : Type*} [TopologicalSpace V] [NormedAddCommGroup W]
       [MeasurableSpace A] (S : Set C(V, W))
       [MeasurableSpace S] [BorelSpace S] [HasOuterApproxClosed S]
       (K : Set V) (hK : IsCompact K)
       (samples : ℝ → ProbabilityMeasure A) (profile : ℝ → A → S)
       (hp : ∀ r, Measurable (profile r)) (ν : ProbabilityMeasure S)
       (hν : Tendsto (fun r => ProbabilityMeasure.map (samples r) (profile r)) atTop (𝓝 ν))
       {f : S} (hf : f ∈ (ν : Measure S).support) :
       ∃ (B : ℝ → Set A) (ε : ℝ → ℝ),
         (∀ r, MeasurableSet (B r)) ∧ (∀ r, 0 < ε r) ∧ Tendsto ε atTop (𝓝 0) ∧
         HasSubexponentialLowerBound (fun r => ((samples r : Measure A) (B r)).toReal) ∧
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound