Curried Filters #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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