OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportedChainProbeSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_supported_chain_probe_sequence line 17

   Source documentation

   Finitely many measurable prefix comparisons can be selected together with a supported pair of profiles. The retained compact probe set has quarter mass, independent of the probability of the support neighborhood.

   theorem exists_supported_chain_probe_sequence
       {X S C : Type*} [Nonempty X] [MeasurableSpace X]
       [MetricSpace S] [MeasurableSpace S] [BorelSpace S] [BorelSpace (S × S)]
       [HasOuterApproxClosed (S × S)] [Fintype C]
       {Y : ℕ → Type*} [∀ n, TopologicalSpace (Y n)] [∀ n, CompactSpace (Y n)]
       [∀ n, T2Space (Y n)] [∀ n, MeasurableSpace (Y n)] [∀ n, BorelSpace (Y n)]
       [∀ n, Nonempty (Y n)]
       (μ : ProbabilityMeasure X) (ν : ∀ n, ProbabilityMeasure (Y n))
       (carrying : Set X) (hcarrying : MeasurableSet carrying)
       (hfull : (μ : Measure X) carryingᶜ = 0)
       [∀ n, (ν n : Measure (Y n)).InnerRegular]
       (profile : ℕ → X → S × S) (hp : ∀ n, Measurable (profile n))
   …