mathlib3 documentation

order.filter.curry

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 #

Main statements #

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

Equations
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 γ} :
(∀ᶠ (a : α) in la, filter.tendsto (λ (b : β), f a b) lb lc) filter.tendsto f (la.curry lb) lc