The filter of small sets

This file defines the filter of small sets w.r.t. a filter f, which is the largest filter containing all powersets of members of f.

g converges to f.smallSets if for all s ∈ f, eventually we have g x ⊆ s.

An example usage is that if f : ι → E → ℝ is a family of nonnegative functions with integral 1, then saying that λ i, support (f i) tendsto (𝓝 0).smallSets is a way of saying that f tends to the Dirac delta distribution.

ink

def Filter.smallSets {α : Type u_1} (l : Filter α) : Filter (Set α)

The filter l.smallSets is the largest filter containing all powersets of members of l.

Equations

• Filter.smallSets l = Filter.lift' l Set.powerset

ink

theorem Filter.smallSets_eq_generate {α : Type u_1} {f : Filter α} : Filter.smallSets f = Filter.generate (Set.powerset '' f.sets)

ink

theorem Filter.HasBasis.smallSets {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Filter.HasBasis (Filter.smallSets l) p fun i => 𝒫 s i

ink

theorem Filter.hasBasis_smallSets {α : Type u_1} (l : Filter α) : Filter.HasBasis (Filter.smallSets l) (fun t => t ∈ l) Set.powerset

ink

theorem Filter.tendsto_smallSets_iff {α : Type u_2} {β : Type u_1} {la : Filter α} {lb : Filter β} {f : α → Set β} : Filter.Tendsto f la (Filter.smallSets lb) ↔ ∀ (t : Set β), t ∈ lb → Filter.Eventually (fun x => f x ⊆ t) la

g converges to f.smallSets if for all s ∈ f, eventually we have g x ⊆ s.

ink

theorem Filter.eventually_smallSets {α : Type u_1} {l : Filter α} {p : Set α → Prop} : Filter.Eventually (fun s => p s) (Filter.smallSets l) ↔ ∃ s, s ∈ l ∧ ((t : Set α) → t ⊆ s → p t)

ink

theorem Filter.eventually_small_sets' {α : Type u_1} {l : Filter α} {p : Set α → Prop} (hp : ⦃s t : Set α⦄ → s ⊆ t → p t → p s) : Filter.Eventually (fun s => p s) (Filter.smallSets l) ↔ ∃ s, s ∈ l ∧ p s

ink

theorem Filter.frequently_smallSets {α : Type u_1} {l : Filter α} {p : Set α → Prop} : Filter.Frequently (fun s => p s) (Filter.smallSets l) ↔ ∀ (t : Set α), t ∈ l → ∃ s, s ⊆ t ∧ p s

ink

theorem Filter.frequently_smallSets_mem {α : Type u_1} (l : Filter α) : Filter.Frequently (fun s => s ∈ l) (Filter.smallSets l)

ink

theorem Filter.HasAntitoneBasis.tendsto_smallSets {α : Type u_2} {l : Filter α} {ι : Type u_1} [inst : Preorder ι] {s : ι → Set α} (hl : Filter.HasAntitoneBasis l s) : Filter.Tendsto s Filter.atTop (Filter.smallSets l)

ink

theorem Filter.monotone_smallSets {α : Type u_1} : Monotone Filter.smallSets

ink

@[simp]

theorem Filter.smallSets_bot {α : Type u_1} : Filter.smallSets ⊥ = pure ∅

ink

@[simp]

theorem Filter.smallSets_top {α : Type u_1} : Filter.smallSets ⊤ = ⊤

ink

@[simp]

theorem Filter.smallSets_principal {α : Type u_1} (s : Set α) : Filter.smallSets (Filter.principal s) = Filter.principal (𝒫 s)

ink

theorem Filter.smallSets_comap {α : Type u_2} {β : Type u_1} (l : Filter β) (f : α → β) : Filter.smallSets (Filter.comap f l) = Filter.lift' l (Set.powerset ∘ Set.preimage f)

ink

theorem Filter.comap_smallSets {α : Type u_2} {β : Type u_1} (l : Filter β) (f : α → Set β) : Filter.comap f (Filter.smallSets l) = Filter.lift' l (Set.preimage f ∘ Set.powerset)

ink

theorem Filter.smallSets_infᵢ {α : Type u_1} {ι : Sort u_2} {f : ι → Filter α} : Filter.smallSets (infᵢ f) = ⨅ i, Filter.smallSets (f i)

ink

theorem Filter.smallSets_inf {α : Type u_1} (l₁ : Filter α) (l₂ : Filter α) : Filter.smallSets (l₁ ⊓ l₂) = Filter.smallSets l₁ ⊓ Filter.smallSets l₂

ink

instance Filter.smallSets_neBot {α : Type u_1} (l : Filter α) : Filter.NeBot (Filter.smallSets l)

Equations

• @Filter.smallSets_neBot = @Filter.smallSets_neBot.proof_1

ink

theorem Filter.Tendsto.smallSets_mono {α : Type u_2} {β : Type u_1} {la : Filter α} {lb : Filter β} {s : α → Set β} {t : α → Set β} (ht : Filter.Tendsto t la (Filter.smallSets lb)) (hst : Filter.Eventually (fun x => s x ⊆ t x) la) : Filter.Tendsto s la (Filter.smallSets lb)

ink

theorem Filter.Tendsto.of_smallSets {α : Type u_2} {β : Type u_1} {la : Filter α} {lb : Filter β} {s : α → Set β} {f : α → β} (hs : Filter.Tendsto s la (Filter.smallSets lb)) (hf : Filter.Eventually (fun x => f x ∈ s x) la) : Filter.Tendsto f la lb

Generalized squeeze theorem (also known as sandwich theorem). If s : α → Set β is a family of sets that tends to Filter.smallSets lb along la and f : α → β is a function such that f x ∈ s x eventually along la, then f tends to lb along la.

If s x is the closed interval [g x, h x] for some functions g, h that tend to the same limit 𝓝 y, then we obtain the standard squeeze theorem, see tendsto_of_tendsto_of_tendsto_of_le_of_le'.

ink

@[simp]

theorem Filter.eventually_smallSets_eventually {α : Type u_1} {l : Filter α} {l' : Filter α} {p : α → Prop} : Filter.Eventually (fun s => Filter.Eventually (fun x => x ∈ s → p x) l') (Filter.smallSets l) ↔ Filter.Eventually (fun x => p x) (l ⊓ l')

ink

@[simp]

theorem Filter.eventually_smallSets_forall {α : Type u_1} {l : Filter α} {p : α → Prop} : Filter.Eventually (fun s => (x : α) → x ∈ s → p x) (Filter.smallSets l) ↔ Filter.Eventually (fun x => p x) l

ink

theorem Filter.Eventually.smallSets {α : Type u_1} {l : Filter α} {p : α → Prop} : Filter.Eventually (fun x => p x) l → Filter.Eventually (fun s => (x : α) → x ∈ s → p x) (Filter.smallSets l)

Alias of the reverse direction of Filter.eventually_smallSets_forall.

ink

theorem Filter.Eventually.of_smallSets {α : Type u_1} {l : Filter α} {p : α → Prop} : Filter.Eventually (fun s => (x : α) → x ∈ s → p x) (Filter.smallSets l) → Filter.Eventually (fun x => p x) l

Alias of the forward direction of Filter.eventually_smallSets_forall.

ink

@[simp]

theorem Filter.eventually_smallSets_subset {α : Type u_1} {l : Filter α} {s : Set α} : Filter.Eventually (fun t => t ⊆ s) (Filter.smallSets l) ↔ s ∈ l