OAI/GroupTheory/PolycyclicRecognition/Analysis/GoodProfileSegment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_good_profiles_along_segment line 19

   Source documentation

   A supported weak profile limit gives one slowly improving family of good sheets on a compact neighborhood of the entire actual late segment. The endpoint scheme can be fixed before this selection.

   theorem exists_good_profiles_along_segment
       {V W A : Type*} [MetricSpace V] [LocallyCompactSpace V]
       [NormedAddCommGroup W] [MeasurableSpace A]
       (S : Set C(V, W)) [MeasurableSpace S] [BorelSpace S] [HasOuterApproxClosed S]
       (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)
       (Ψ : ℝ → C(V × ℝ, V)) (Ψ₀ : C(V × ℝ, V))
       (hΨ : Tendsto Ψ atTop (𝓝 Ψ₀)) (z : V) (T : ℝ)
       (U : Set V) (hU : IsOpen U) (hseg : ∀ t ∈ Icc 0 T, Ψ₀ (z, t) ∈ U) :
       ∃ (Q : Set V) (B : ℝ → Set A) (ζ : ℝ → ℝ),
   …