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 at_top, p n ↔ ∃ N, ∀ n ≥ N, p n. A curried filter yields the quantifier order ∃ ∀ ∃ ∀. For instance, ∀ᶠ n in at_top.curry at_top, 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 at_top ×ˢ at_top, 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).

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

def Filter.curry {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) : Filter (α × β)

This filter is characterized by Filter.eventually_curry_iff: (∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y). Useful in adding quantifiers to the middle of Tendstos. See hasFDerivAt_of_tendstoUniformlyOnFilter.

Equations

• f.curry g = { sets := {s : Set (α × β) | ∀ᶠ (a : α) in f, ∀ᶠ (b : β) in g, (a, b) ∈ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

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

theorem Filter.curry_le_prod {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : f.curry g ≤ f.prod g

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