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 fun i ↦ support (f i) tendsto (𝓝 0).smallSets is a way of saying that f tends to the Dirac delta distribution.

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.

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

theorem Filter.bind_smallSets_gc {α : Type u_1} : GaloisConnection (fun (L : Filter (Set α)) => L.bind principal) smallSets

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

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

theorem Filter.Eventually.exists_mem_basis_of_smallSets {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop} (h₁ : ∀ᶠ (t : Set α) in l.smallSets, P t) (h₂ : l.HasBasis p s) : ∃ (i : ι), p i ∧ P (s i)

theorem Filter.Frequently.smallSets_of_forall_mem_basis {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop} (h₁ : ∀ (i : ι), p i → P (s i)) (h₂ : l.HasBasis p s) : ∃ᶠ (t : Set α) in l.smallSets, P t

theorem Filter.Eventually.exists_mem_of_smallSets {α : Type u_1} {l : Filter α} {p : Set α → Prop} (h : ∀ᶠ (t : Set α) in l.smallSets, p t) : ∃ s ∈ l, p s

No Frequently.smallSets_of_forall_mem (h : ∀ s ∈ l, p s) : ∃ᶠ t in l.smallSets, p t as Filter.frequently_smallSets_mem : ∃ᶠ t in l.smallSets, t ∈ l is preferred.

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

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

theorem Filter.eventually_smallSets {α : Type u_1} {l : Filter α} {p : Set α → Prop} : (∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t ⊆ s, p t

theorem Filter.eventually_smallSets' {α : Type u_1} {l : Filter α} {p : Set α → Prop} (hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s) : (∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, p s

theorem Filter.frequently_smallSets {α : Type u_1} {l : Filter α} {p : Set α → Prop} : (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, ∃ s ⊆ t, p s

theorem Filter.frequently_smallSets_mem {α : Type u_1} (l : Filter α) : ∃ᶠ (s : Set α) in l.smallSets, s ∈ l

@[simp]

theorem Filter.tendsto_image_smallSets {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : α → β} : Tendsto (fun (x : Set α) => f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb

theorem Filter.Tendsto.image_smallSets {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : α → β} : Tendsto f la lb → Tendsto (fun (x : Set α) => f '' x) la.smallSets lb.smallSets

Alias of the reverse direction of Filter.tendsto_image_smallSets.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Filter.smallSets_comap_eq_comap_image {α : Type u_1} {β : Type u_2} (l : Filter β) (f : α → β) : (comap f l).smallSets = comap (Set.image f) l.smallSets

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

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

theorem Filter.smallSets_iInf {α : Type u_1} {ι : Sort u_3} {f : ι → Filter α} : (iInf f).smallSets = ⨅ (i : ι), (f i).smallSets

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

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

theorem Filter.Tendsto.smallSets_mono {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {s t : α → Set β} (ht : Tendsto t la lb.smallSets) (hst : ∀ᶠ (x : α) in la, s x ⊆ t x) : Tendsto s la lb.smallSets

theorem Filter.Tendsto.of_smallSets {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {s : α → Set β} {f : α → β} (hs : Tendsto s la lb.smallSets) (hf : ∀ᶠ (x : α) in la, f x ∈ s x) : 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'.

@[simp]

theorem Filter.eventually_smallSets_eventually {α : Type u_1} {l l' : Filter α} {p : α → Prop} : (∀ᶠ (s : Set α) in l.smallSets, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x

@[simp]

theorem Filter.eventually_smallSets_forall {α : Type u_1} {l : Filter α} {p : α → Prop} : (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x

theorem Filter.Eventually.smallSets {α : Type u_1} {l : Filter α} {p : α → Prop} : (∀ᶠ (x : α) in l, p x) → ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x

Alias of the reverse direction of Filter.eventually_smallSets_forall.

theorem Filter.Eventually.of_smallSets {α : Type u_1} {l : Filter α} {p : α → Prop} : (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) → ∀ᶠ (x : α) in l, p x

Alias of the forward direction of Filter.eventually_smallSets_forall.

@[simp]

theorem Filter.eventually_smallSets_subset {α : Type u_1} {l : Filter α} {s : Set α} : (∀ᶠ (t : Set α) in l.smallSets, t ⊆ s) ↔ s ∈ l