Mathlib.Order.Filter.Curry

Module docstring

{"# Curried Filters

This file provides an operation (Filter.curry) on filters which provides the equivalence ∀ᶠ a in l, ∀ᶠ b in l', p (a, b) ↔ ∀ᶠ c in (l.curry l'), p c (see Filter.eventually_curry_iff).

To understand when this operation might arise, it is helpful to think of ∀ᶠ as a combination of the quantifiers ∃ ∀. For instance, ∀ᶠ n in atTop, p n ↔ ∃ N, ∀ n ≥ N, p n. A curried filter yields the quantifier order ∃ ∀ ∃ ∀. For instance, ∀ᶠ n in atTop.curry atTop, p n ↔ ∃ M, ∀ m ≥ M, ∃ N, ∀ n ≥ N, p (m, n).

This is different from a product filter, which instead yields a quantifier order ∃ ∃ ∀ ∀. For instance, ∀ᶠ n in atTop ×ˢ atTop, p n ↔ ∃ M, ∃ N, ∀ m ≥ M, ∀ n ≥ N, p (m, n). This makes it clear that if something eventually occurs on the product filter, it eventually occurs on the curried filter (see Filter.curry_le_prod and Filter.Eventually.curry), but the converse is not true.

Another way to think about the curried versus the product filter is that tending to some limit on the product filter is a version of uniform convergence (see tendsto_prod_filter_iff) whereas tending to some limit on a curried filter is just iterated limits (see Filter.Tendsto.curry).

In the \"generalized set\" intuition, Filter.prod and Filter.curry correspond to two ways of describing the product of two sets, namely s ×ˢ t = fst ⁻¹' s ∩ snd ⁻¹' t and s ×ˢ t = ⋃ x ∈ s, (x, ·) '' t.

Main definitions

Filter.curry: A binary operation on filters which represents iterated limits

Main statements

Filter.eventually_curry_iff: An alternative definition of a curried filter
Filter.curry_le_prod: Something that is eventually true on the a product filter is eventually true on the curried filter

Tags

uniform convergence, curried filters, product filters "}

Filter.eventually_curry_iff theorem

{p : α × β → Prop} : (∀ᶠ x : α × β in l.curry m, p x) ↔ ∀ᶠ x : α in l, ∀ᶠ y : β in m, p (x, y)

Full source

theorem eventually_curry_iff {p : α × β → Prop} :
    (∀ᶠ x : α × β in l.curry m, p x) ↔ ∀ᶠ x : α in l, ∀ᶠ y : β in m, p (x, y) :=
  Iff.rfl

Equivalence of Eventual Conditions in Curried Filter

Informal description

For any predicate $p$ on pairs $(x,y) \in \alpha \times \beta$, the following are equivalent: 1. The predicate $p$ holds eventually for all pairs in the curried filter $l.\text{curry}\, m$. 2. For $x$ eventually in $l$, the predicate $p(x,y)$ holds for $y$ eventually in $m$. In other words, $\forall^{\text{event}} (x,y) \in l.\text{curry}\, m,\ p(x,y) \leftrightarrow \forall^{\text{event}} x \in l,\ \forall^{\text{event}} y \in m,\ p(x,y)$.

Filter.frequently_curry_iff theorem

(p : (α × β) → Prop) : (∃ᶠ x in l.curry m, p x) ↔ ∃ᶠ x in l, ∃ᶠ y in m, p (x, y)

Full source

theorem frequently_curry_iff
    (p : (α × β) → Prop) : (∃ᶠ x in l.curry m, p x) ↔ ∃ᶠ x in l, ∃ᶠ y in m, p (x, y) := by
  simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]

Frequently in Curried Filter Equals Iterated Frequencies

Informal description

For any predicate $p : \alpha \times \beta \to \mathrm{Prop}$ and filters $l$ on $\alpha$ and $m$ on $\beta$, the following equivalence holds: $(\exists^\infty x \in l.\mathrm{curry}\, m, p(x)) \leftrightarrow (\exists^\infty x \in l, \exists^\infty y \in m, p(x, y))$. Here, $\exists^\infty$ denotes "frequently" (i.e., "for infinitely many" or "for a cofinal set"), meaning that the set of elements satisfying the predicate is not eventually empty in the filter.

Filter.mem_curry_iff theorem

{s : Set (α × β)} : s ∈ l.curry m ↔ ∀ᶠ x : α in l, ∀ᶠ y : β in m, (x, y) ∈ s

Full source

theorem mem_curry_iff {s : Set (α × β)} :
    s ∈ l.curry ms ∈ l.curry m ↔ ∀ᶠ x : α in l, ∀ᶠ y : β in m, (x, y) ∈ s := Iff.rfl

Characterization of Membership in Curried Filter

Informal description

For any set $s \subseteq \alpha \times \beta$, the set $s$ belongs to the curried filter $l.\text{curry}\, m$ if and only if for eventually all $x$ in $l$ and eventually all $y$ in $m$, the pair $(x, y)$ is in $s$.

Filter.curry_le_prod theorem

: l.curry m ≤ l ×ˢ m

Full source

theorem curry_le_prod : l.curry m ≤ l ×ˢ m := fun _ => Eventually.curry

Curried Filter is Finer than Product Filter

Informal description

For any filters $l$ on a type $\alpha$ and $m$ on a type $\beta$, the curried filter $l.\text{curry}\, m$ is finer than the product filter $l \times^s m$. In other words, $l.\text{curry}\, m \leq l \times^s m$.

Filter.Tendsto.curry theorem

 {f : α → β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ} (h : ∀ᶠ a in la, Tendsto (fun b : β => f a b) lb lc) :
  Tendsto (↿f) (la.curry lb) lc

Full source

theorem Tendsto.curry {f : α → β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ}
    (h : ∀ᶠ a in la, Tendsto (fun b : β => f a b) lb lc) : Tendsto (↿f) (la.curry lb) lc :=
  fun _s hs => h.mono fun _a ha => ha hs

Tendsto of Uncurried Function Along Curried Filter

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function, and let $l_a$, $l_b$, $l_c$ be filters on $\alpha$, $\beta$, $\gamma$ respectively. If for eventually all $a \in l_a$, the function $f(a, \cdot) : \beta \to \gamma$ tends to $l_c$ along $l_b$, then the uncurried function $\uncurry f : \alpha \times \beta \to \gamma$ tends to $l_c$ along the curried filter $l_a.\text{curry}\, l_b$.

Filter.frequently_curry_prod_iff theorem

: (∃ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ x in l, x ∈ s) ∧ ∃ᶠ y in m, y ∈ t

Full source

theorem frequently_curry_prod_iff :
    (∃ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ x in l, x ∈ s) ∧ ∃ᶠ y in m, y ∈ t := by
  simp [frequently_curry_iff]

Frequently Occurring Pairs in Curried Filter and Product Set

Informal description

For any filters $l$ and $m$ and sets $s$ and $t$, the following are equivalent: 1. There exist frequently many pairs $(x, y)$ in the curried filter $l.\text{curry}\, m$ such that $(x, y) \in s \times t$. 2. There exist frequently many $x \in l$ such that $x \in s$, and there exist frequently many $y \in m$ such that $y \in t$. In other words, the frequently occurring pairs in the product set $s \times t$ under the curried filter $l.\text{curry}\, m$ correspond precisely to the frequently occurring elements in $s$ under $l$ and frequently occurring elements in $t$ under $m$.

Filter.eventually_curry_prod_iff theorem

[NeBot l] [NeBot m] : (∀ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m

Full source

theorem eventually_curry_prod_iff [NeBot l] [NeBot m] :
    (∀ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m := by
  simp [eventually_curry_iff]

Characterization of Eventually in Curried Filter for Product Sets

Informal description

For non-trivial filters $l$ and $m$, the event that a pair $(x, y)$ belongs to the product set $s \times t$ eventually holds in the curried filter $l.\text{curry}\, m$ if and only if the set $s$ is in the filter $l$ and the set $t$ is in the filter $m$. In other words, \[ (\forall^\infty (x,y) \text{ in } l.\text{curry}\, m, \, (x,y) \in s \times t) \leftrightarrow s \in l \land t \in m. \]

Filter.prod_mem_curry theorem

(hs : s ∈ l) (ht : t ∈ m) : s ×ˢ t ∈ l.curry m

Full source

theorem prod_mem_curry (hs : s ∈ l) (ht : t ∈ m) : s ×ˢ t ∈ l.curry m :=
  curry_le_prod <| prod_mem_prod hs ht

Product Set Membership in Curried Filter

Informal description

For any sets $s$ in a filter $l$ and $t$ in a filter $m$, the product set $s \times t$ belongs to the curried filter $l.\text{curry}\, m$.