AffineProfileConcentration.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Concentration near a finite family of affine profiles

def OAI.PolycyclicRecognition.affineProfileClass line 19
Source documentation
Restrictions of the finitely many linear profiles, with arbitrary offsets.
```
def affineProfileClass {Z W L : Type*} [TopologicalSpace Z]
    [TopologicalSpace W] [Add W] (A : L → C(Z, W)) : Set C(Z, W) :=
…
```
theorem OAI.PolycyclicRecognition.affineProfileClass_nonempty line 23
theorem OAI.PolycyclicRecognition.isClosed_affineProfileClass line 31
Source documentation
One evaluation recovers the offset. This makes the affine class closed without requiring an a priori bound on its offsets.
```
theorem isClosed_affineProfileClass {Z W L : Type*} [TopologicalSpace Z]
    [TopologicalSpace W] [AddCommGroup W] [IsTopologicalAddGroup W] [T2Space W]
    [Finite L] (A : L → C(Z, W)) (z₀ : Z) :
    IsClosed (affineProfileClass A) := by
…
```
Mentions: OAI.PolycyclicRecognition.affineProfileClass

theorem OAI.PolycyclicRecognition.measure_closed_tendsto_zero_of_support line 57

Source documentation

A closed event disjoint from the support of the limit has probability converging to zero.

theorem measure_closed_tendsto_zero_of_support
    {S : Type*} [TopologicalSpace S] [MeasurableSpace S] [BorelSpace S]
    [HasOuterApproxClosed S] [HereditarilyLindelofSpace S]
    {μn : ℕ → ProbabilityMeasure S} {μ : ProbabilityMeasure S}
    (hμ : Tendsto μn atTop (𝓝 μ)) {B : Set S} (hB : IsClosed B)
    (hs : ∀ f ∈ (μ : Measure S).support, f ∉ B) :
    Tendsto (fun n => (μn n : Measure S) B) atTop (𝓝 0) := by
…

theorem OAI.PolycyclicRecognition.measure_closed_tendsto_zero_of_all_supported_limits line 73

Source documentation

Compactness turns a statement about every supported sequential limit into concentration for the original sequence.

theorem measure_closed_tendsto_zero_of_all_supported_limits
    {S : Type*} [TopologicalSpace S] [CompactSpace S] [MetrizableSpace S]
    [MeasurableSpace S] [BorelSpace S] (μn : ℕ → ProbabilityMeasure S)
    {B : Set S} (hB : IsClosed B)
    (hs : ∀ (ι : ℕ → ℕ), StrictMono ι → ∀ μ : ProbabilityMeasure S,
      Tendsto (μn ∘ ι) atTop (𝓝 μ) → ∀ f ∈ (μ : Measure S).support, f ∉ B) :
    Tendsto (fun n => (μn n : Measure S) B) atTop (𝓝 0) := by
…

theorem OAI.PolycyclicRecognition.affine_distance_concentration line 90

Source documentation

On a compact profile space, affine support of every weak limit gives vanishing probability of a fixed positive distance from the affine class.

theorem affine_distance_concentration
    {V W L : Type*} [TopologicalSpace V] [LocallyCompactSpace V]
    [NormedAddCommGroup W] [Nonempty L]
    (S : Set C(V, W)) [CompactSpace S] [MetrizableSpace S]
    [MeasurableSpace S] [BorelSpace S]
    (μn : ℕ → ProbabilityMeasure S) (Z : Set V) [CompactSpace Z]
    (A : L → C(Z, W))
    (hs : ∀ (ι : ℕ → ℕ), StrictMono ι → ∀ μ : ProbabilityMeasure S,
      Tendsto (μn ∘ ι) atTop (𝓝 μ) → ∀ f ∈ (μ : Measure S).support,
        f.val.restrict Z ∈ affineProfileClass A)
    {η : ℝ} (hη : 0 < η) :
    Tendsto (fun n => (μn n : Measure S)
…

Mentions: OAI.PolycyclicRecognition.affineProfileClass