WeakLimits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Passing packet estimates to weak limits

The ordinary-ball estimate in paper 031-01 is proved for each fixed ball, with a packet threshold that may depend on that ball. Portmanteau passes this estimate to the limit without a uniform threshold or an exchange of shrinking-radius and packet limits. Continuous diagonal transformations also preserve invariance in the weak limit.

theorem OAI.DukePrimeDegree.open_mass_le_of_tendsto line 26

Source documentation

Any eventual upper bound on the mass of a fixed open set passes to a weak probability limit.

theorem open_mass_le_of_tendsto
    (μs : I → ProbabilityMeasure X) (μ : ProbabilityMeasure X)
    (hlim : Tendsto μs L (𝓝 μ)) (U : Set X) (hU : IsOpen U)
    (C : ℝ≥0∞) (hbound : ∀ᶠ i in L, (μs i : Measure X) U ≤ C) :
    (μ : Measure X) U ≤ C := by
…

theorem OAI.DukePrimeDegree.ball_bounds_of_tendsto line 38

Source documentation

The radius and center dependent thresholds in the manuscript's vector box estimate suffice for a uniform ordinary-ball bound on the limit.

theorem ball_bounds_of_tendsto
    (μs : I → ProbabilityMeasure X) (μ : ProbabilityMeasure X)
    (hlim : Tendsto μs L (𝓝 μ)) (balls : X → ℝ → Set X)
    (hopen : ∀ x r, IsOpen (balls x r)) (n : ℕ)
    (hbound : ∀ K : Set X, IsCompact K →
      ∃ C r₀ : ℝ, 0 ≤ C ∧ 0 < r₀ ∧
        ∀ x ∈ K, ∀ r, 0 < r → r < r₀ →
          ∀ᶠ i in L, (μs i : Measure X) (balls x r) ≤ ENNReal.ofReal (C * r ^ n)) :
    ∀ K : Set X, IsCompact K →
      ∃ C r₀ : ℝ, 0 ≤ C ∧ 0 < r₀ ∧
        ∀ x ∈ K, ∀ r, 0 < r → r < r₀ →
          (μ : Measure X) (balls x r) ≤ ENNReal.ofReal (C * r ^ n) := by
…

theorem OAI.DukePrimeDegree.invariant_of_tendsto line 59

Source documentation

Push-forward invariance under a continuous transformation survives weak convergence. Eventual invariance is enough.

theorem invariant_of_tendsto
    (μs : I → ProbabilityMeasure X) (μ : ProbabilityMeasure X)
    (hlim : Tendsto μs L (𝓝 μ)) (T : X → X) (hT : Continuous T)
    (hinv : ∀ᶠ i in L, (μs i).map T = μs i) :
    μ.map T = μ := by
…

theorem OAI.DukePrimeDegree.measure_invariant_of_tendsto line 71

Source documentation

Weak limits of invariant probabilities remain invariant as measures.

theorem measure_invariant_of_tendsto
    (μs : I → ProbabilityMeasure X) (μ : ProbabilityMeasure X)
    (hlim : Tendsto μs L (𝓝 μ)) (T : X → X) (hT : Continuous T)
    (hinv : ∀ᶠ i in L, Measure.map T (μs i : Measure X) = (μs i : Measure X)) :
    Measure.map T (μ : Measure X) = (μ : Measure X) := by
…