# 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

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 `tendsto`

s. See
`has_fderiv_at_of_tendsto_uniformly_on_filter`

.

## Equations

- One or more equations did not get rendered due to their size.