OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportedProbeSelection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.finite_bad_union_tendsto_zero line 20

   Source documentation

   A fixed finite set of probe comparisons succeeds simultaneously in probability. No independence between the separate comparisons is needed.

   theorem finite_bad_union_tendsto_zero
       {X J : Type*} [MeasurableSpace X] [Fintype J]
       (μ : ℕ → Measure X) (bad : ℕ → J → Set X)
       (hlim : ∀ j, Tendsto (fun n => μ n (bad n j)) atTop (𝓝 0)) :
       Tendsto (fun n => μ n (⋃ j, bad n j)) atTop (𝓝 0) := by
   …

2. theorem OAI.PolycyclicRecognition.exists_compact_probes_from_supported_profiles line 34

   Source documentation

   Deterministic comparison concentration and a supported weak profile limit supply one starting point and a compact set of good probes at shrinking profile tolerances. This does not condition a measure on a singleton.

   theorem exists_compact_probes_from_supported_profiles
       {X S : Type*} [MeasurableSpace X] [TopologicalSpace S]
       [MeasurableSpace S] [BorelSpace S] [HasOuterApproxClosed S]
       {Y : ℕ → Type*} [∀ n, MeasurableSpace (Y n)] [∀ n, TopologicalSpace (Y n)]
       [∀ n, Nonempty (Y n)]
       (μ : ProbabilityMeasure X) (ν : ∀ n, ProbabilityMeasure (Y n))
       [∀ n, (ν n : Measure (Y n)).InnerRegular]
       (profile : ℕ → X → S) (hp : ∀ n, Measurable (profile n))
       (limitLaw : ProbabilityMeasure S)
       (hlim : Tendsto (fun n => ProbabilityMeasure.map μ (profile n)) atTop (𝓝 limitLaw))
       {f : S} (hf : f ∈ (limitLaw : Measure S).support)
       (U : ℕ → Set S) (hU : ∀ j, IsOpen (U j)) (hfU : ∀ j, f ∈ U j)
   …