OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceCellProfileSegment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_good_cell_profiles_along_segment_sequence 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_cell_profiles_along_segment_sequence
       {V W A : Type*} [MetricSpace V] [LocallyCompactSpace V]
       [NormedAddCommGroup W] [MeasurableSpace A]
       (S : Set C(V, W)) [MeasurableSpace S] [BorelSpace S] [HasOuterApproxClosed S]
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (μ : Measure A) (cells : ℕ → Set A) (hcells : ∀ n, MeasurableSet (cells n))
       (hcell0 : ∀ n, μ (cells n) ≠ 0) (hcellfin : ∀ n, μ (cells n) ≠ ∞)
       (profile : ℕ → A → S)
       (hp : ∀ r, Measurable (profile r)) (ν : ProbabilityMeasure S)
       (hν : Tendsto (fun r => ProbabilityMeasure.map (cellProbabilityMeasure μ (cells r) (hcell0 r) (hcellfin r)) (profile r)) atTop (𝓝 ν))
       {f : S} (hf : f ∈ (ν : Measure S).support)
       (Ψ : ℕ → C(V × ℝ, V)) (Ψ₀ : C(V × ℝ, V))
   …

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure