OAI/GroupTheory/PolycyclicRecognition/Analysis/IndependentProfileLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.profile_increment_mem_of_independent_errors line 17

   Source documentation

   The independent starting-point law need only have the specified point in its support. The conclusion then holds at every supported profile.

   theorem profile_increment_mem_of_independent_errors
       {U V W ι : Type*} [TopologicalSpace U] [LocallyCompactSpace U]
       [SecondCountableTopology U] [TopologicalSpace V] [LocallyCompactSpace V]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       (S : Set C(V, W)) (hS : IsCompact S) (K : Set U) (hK : IsCompact K)
       [MeasurableSpace S] [BorelSpace S] [MeasurableSpace K] [BorelSpace K]
       (q : ℝ) (A : C(U, V)) {l : Filter ι} [l.NeBot]
       {T : ι → C(U, V)} {T₀ : C(U, V)} (hT : Tendsto T l (𝓝 T₀))
       (νs : ι → ProbabilityMeasure S) (ν : ProbabilityMeasure S)
       (hν : Tendsto νs l (𝓝 ν)) (η : ProbabilityMeasure K)
       {C : Set W} (hC : IsClosed C) (hne : C.Nonempty)
       (herr : Tendsto (fun i => ∫ f, ∫ z : K, Metric.infDist
   …