# Documentation

Mathlib.Order.Filter.Curry

# 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∀ᶠ a in l, ∀ᶠ b in l', p (a, b) ↔ ∀ᶠ c in (l.curry l'), p c∀ᶠ b in l', p (a, b) ↔ ∀ᶠ c in (l.curry l'), p c↔ ∀ᶠ c in (l.curry l'), p c∀ᶠ 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∀ᶠ n in at_top, p n ↔ ∃ N, ∀ n ≥ N, p n↔ ∃ N, ∀ n ≥ N, p n∃ N, ∀ n ≥ N, p n∀ n ≥ N, p 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)∀ᶠ n in at_top.curry at_top, p n ↔ ∃ M, ∀ m ≥ M, ∃ N, ∀ n ≥ N, p (m, n)↔ ∃ M, ∀ m ≥ M, ∃ N, ∀ n ≥ N, p (m, n)∃ M, ∀ m ≥ M, ∃ N, ∀ n ≥ N, p (m, n)∀ m ≥ M, ∃ N, ∀ n ≥ N, p (m, n)≥ M, ∃ N, ∀ n ≥ N, p (m, n)∃ N, ∀ n ≥ N, p (m, n)∀ n ≥ N, p (m, 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)∀ᶠ n in at_top ×ᶠ at_top, p n ↔ ∃ M, ∃ N, ∀ m ≥ M, ∀ n ≥ N, p (m, n)×ᶠ at_top, p n ↔ ∃ M, ∃ N, ∀ m ≥ M, ∀ n ≥ N, p (m, n)↔ ∃ M, ∃ N, ∀ m ≥ M, ∀ n ≥ N, p (m, n)∃ M, ∃ N, ∀ m ≥ M, ∀ n ≥ N, p (m, n)∃ N, ∀ m ≥ M, ∀ n ≥ N, p (m, n)∀ m ≥ M, ∀ n ≥ N, p (m, n)≥ M, ∀ n ≥ N, p (m, n)∀ n ≥ N, p (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 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 : ) (g : ) :
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)∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)× β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)∀ᶠ (y : β) in g, p (x, y). Useful in adding quantifiers to the middle of tendstos. See has_fderiv_at_of_tendsto_uniformly_on_filter.

Equations
• One or more equations did not get rendered due to their size.
theorem Filter.eventually_curry_iff {α : Type u_1} {β : Type u_2} {f : } {g : } {p : α × βProp} :
Filter.Eventually (fun x => p x) () Filter.Eventually (fun x => Filter.Eventually (fun y => p (x, y)) g) f
theorem Filter.curry_le_prod {α : Type u_1} {β : Type u_2} {f : } {g : } :
theorem Filter.Tendsto.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {la : } {lb : } {lc : } (h : Filter.Eventually (fun a => Filter.Tendsto (fun b => f a b) lb lc) la) :