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

theorem Filter.eventually_curry_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {p : α × β → Prop} : (∀ᶠ (x : α × β) in l.curry m, p x) ↔ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, p (x, y)

theorem Filter.frequently_curry_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} (p : α × β → Prop) : (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)

theorem Filter.mem_curry_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set (α × β)} : s ∈ l.curry m ↔ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, (x, y) ∈ s

theorem Filter.curry_le_prod {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} : l.curry m ≤ l ×ˢ m

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

theorem Filter.frequently_curry_prod_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β} : (∃ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ (x : α) in l, x ∈ s) ∧ ∃ᶠ (y : β) in m, y ∈ t

theorem Filter.eventually_curry_prod_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β} [l.NeBot] [m.NeBot] : (∀ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m

theorem Filter.prod_mem_curry {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β} (hs : s ∈ l) (ht : t ∈ m) : s ×ˢ t ∈ l.curry m