OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportedPairAgreement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.supported_pair_eq_of_concentration line 15

   Source documentation

   Endpoint concentration identifies the two profiles in every supported joint limit. Intermediate chains may use a different compact profile family.

   theorem supported_pair_eq_of_concentration
       {V W A : Type*} [TopologicalSpace V] [NormedAddCommGroup W] [MeasurableSpace A]
       (S : Set C(V, W)) [MeasurableSpace S] [BorelSpace S]
       [BorelSpace (S × S)] [HasOuterApproxClosed (S × S)]
       (μ : ProbabilityMeasure A) (pair : ℕ → A → S × S) (hp : ∀ n, Measurable (pair n))
       (ν : ProbabilityMeasure (S × S))
       (hν : Tendsto (fun n => ProbabilityMeasure.map μ (pair n)) atTop (𝓝 ν))
       (Z : Set V) [CompactSpace Z]
       (hconc : ∀ η : ℝ, 0 < η → Tendsto (fun n => (μ : Measure A)
         {a | η ≤ dist ((pair n a).1.val.restrict Z) ((pair n a).2.val.restrict Z)})
         atTop (𝓝 0))
       {f : S × S} (hf : f ∈ (ν : Measure (S × S)).support) :
   …