CompactSamplingMean.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Canonical affine choices for compactly carried sampling laws

theorem OAI.PolycyclicRecognition.integrable_continuous_of_ae_mem_compact line 15
def OAI.PolycyclicRecognition.canonicalAffineLabel line 25
Source documentation
The chosen label depends only on the law and the actual profile, so different sequences use the same choice at any shared parameter.
```
def canonicalAffineLabel
    {X Y L : Type*} [MeasurableSpace X] [PseudoMetricSpace Y]
    [Finite L] [Nonempty L]
    (μ : Measure X) (f : X → Y) (A : L → Y) : L := by
…
```
theorem OAI.PolycyclicRecognition.canonicalAffineLabel_mean_tendsto_zero line 32

theorem OAI.PolycyclicRecognition.compact_profile_probability_of_mean line 49

Source documentation

Compact support supplies the integrability required by Markov's inequality, including for the canonical minimizing affine label.

theorem compact_profile_probability_of_mean
    {X Y : Type*} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X]
    [PseudoMetricSpace Y]
    (μ : ℕ → ProbabilityMeasure X) (C : ℕ → Set X)
    (hC : ∀ n, IsCompact (C n)) (hfull : ∀ n, ∀ᵐ x ∂(μ n : Measure X), x ∈ C n)
    (f : ℕ → X → Y) (hf : ∀ n, Continuous (f n)) (a : ℕ → Y)
    (hm : Tendsto (fun n => ∫ x, dist (f n x) (a n) ∂(μ n : Measure X)) atTop (𝓝 0))
    {ε : ℝ} (hε : 0 < ε) :
    Tendsto (fun n => (μ n : Measure X) {x | ε ≤ dist (f n x) (a n)})
      atTop (𝓝 0) :=
…