OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportedGoodSetSelection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.eventual_positive_mass_of_supported_weak_limit line 18

   Source documentation

   Each open neighborhood of a supported profile has a fixed positive mass along every sufficiently late member of the weakly convergent family.

   theorem eventual_positive_mass_of_supported_weak_limit
       {X ι : Type*} [TopologicalSpace X] [MeasurableSpace X]
       [OpensMeasurableSpace X] [HasOuterApproxClosed X]
       {l : Filter ι} [l.NeBot] {μs : ι → ProbabilityMeasure X} {μ : ProbabilityMeasure X}
       (hμ : Tendsto μs l (𝓝 μ)) {x : X} (hx : x ∈ (μ : Measure X).support)
       {U : Set X} (hU : IsOpen U) (hxU : x ∈ U) :
       ∃ c : ℝ, 0 < c ∧ ∀ᶠ i in l, c ≤ ((μs i : Measure X) U).toReal := by
   …

2. theorem OAI.PolycyclicRecognition.exists_supported_good_sets_subexponential line 41

   Source documentation

   For any prescribed shrinking sequence of open neighborhoods, the supported weak limit supplies good sets of subexponential mass.

   theorem exists_supported_good_sets_subexponential
       {X : Type*} [TopologicalSpace X] [MeasurableSpace X]
       [OpensMeasurableSpace X] [HasOuterApproxClosed X]
       {μs : ℝ → ProbabilityMeasure X} {μ : ProbabilityMeasure X}
       (hμ : Tendsto μs atTop (𝓝 μ)) {x : X} (hx : x ∈ (μ : Measure X).support)
       (U : ℕ → Set X) (hU : ∀ j, IsOpen (U j)) (hxU : ∀ j, x ∈ U j) :
       ∃ k : ℝ → ℕ, Tendsto k atTop atTop ∧
         HasSubexponentialLowerBound (fun r => ((μs r : Measure X) (U (k r))).toReal) := by
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBound