OAI/GroupTheory/PolycyclicRecognition/Geometry/SupportedFlowLipschitz.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.le_on_support_of_ae_sample_bound line 16

   Source documentation

   Uniformly converging observables retain every uniform asymptotic bound on the support of a weak sample limit.

   theorem le_on_support_of_ae_sample_bound
       {X A : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
       [HasOuterApproxClosed X] [MeasurableSpace A]
       (samples : ℕ → ProbabilityMeasure A) (sample : ℕ → A → X)
       (hsample : ∀ n, Measurable (sample n)) (ν : ProbabilityMeasure X)
       (hν : Tendsto (fun n => ProbabilityMeasure.map (samples n) (sample n)) atTop (𝓝 ν))
       (obsn : ℕ → X → ℝ) (obs : X → ℝ) (hobs : Continuous obs)
       (hlim : TendstoUniformly obsn obs atTop)
       (ε : ℕ → ℝ) (hε : Tendsto ε atTop (𝓝 0)) (C : ℝ)
       (hbound : ∀ᶠ n in atTop, ∀ᵐ a ∂(samples n : Measure A),
         obsn n (sample n a) ≤ C + ε n)
       {f : X} (hf : f ∈ (ν : Measure X).support) : obs f ≤ C := by
   …

2. theorem OAI.PolycyclicRecognition.le_on_support_of_uniform_sample_bound line 58

   Source documentation

   The pointwise version of the almost-everywhere sample bound.

   theorem le_on_support_of_uniform_sample_bound
       {X A : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
       [HasOuterApproxClosed X] [MeasurableSpace A]
       (samples : ℕ → ProbabilityMeasure A) (sample : ℕ → A → X)
       (hsample : ∀ n, Measurable (sample n)) (ν : ProbabilityMeasure X)
       (hν : Tendsto (fun n => ProbabilityMeasure.map (samples n) (sample n)) atTop (𝓝 ν))
       (obsn : ℕ → X → ℝ) (obs : X → ℝ) (hobs : Continuous obs)
       (hlim : TendstoUniformly obsn obs atTop)
       (ε : ℕ → ℝ) (hε : Tendsto ε atTop (𝓝 0)) (C : ℝ)
       (hbound : ∀ᶠ n in atTop, ∀ a, obsn n (sample n a) ≤ C + ε n)
       {f : X} (hf : f ∈ (ν : Measure X).support) : obs f ≤ C := by
   …

3. def OAI.PolycyclicRecognition.profileFlowDistance line 72
4. theorem OAI.PolycyclicRecognition.continuous_profileFlowDistance line 79
5. theorem OAI.PolycyclicRecognition.lipschitz_supported_profile_flow line 94

   Source documentation

   A coarse Lipschitz bound with a vanishing additive error becomes an exact Lipschitz bound along the limiting horizontal flow.

   theorem lipschitz_supported_profile_flow
       {V W A : Type*} [TopologicalSpace V] [LocallyCompactSpace V]
       [PseudoMetricSpace W] [MeasurableSpace A]
       (S : Set C(V, W)) (hS : IsCompact S)
       [MeasurableSpace S] [BorelSpace S] [HasOuterApproxClosed S]
       (samples : ℕ → ProbabilityMeasure A) (sample : ℕ → A → S)
       (hsample : ∀ n, Measurable (sample n)) (ν : ProbabilityMeasure S)
       (hν : Tendsto (fun n => ProbabilityMeasure.map (samples n) (sample n)) atTop (𝓝 ν))
       (Fn : ℕ → C(V × ℝ, V)) (F : C(V × ℝ, V)) (hF : Tendsto Fn atTop (𝓝 F))
       (ε : ℕ → ℝ) (hε : Tendsto ε atTop (𝓝 0)) (C : ℝ≥0) (z : V)
       (hbound : ∀ᶠ n in atTop, ∀ a s t,
         dist ((sample n a).val (Fn n (z, s))) ((sample n a).val (Fn n (z, t))) ≤
   …