Sequence of measurable functions associated to a sequence of a.e.-measurable functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define here tools to prove statements about limits (infi, supr...) of sequences of
ae_measurable functions.
Given a sequence of a.e.-measurable functions f : ι → α → β with hypothesis
hf : ∀ i, ae_measurable (f i) μ, and a pointwise property p : α → (ι → β) → Prop such that we
have hp : ∀ᵐ x ∂μ, p x (λ n, f n x), we define a sequence of measurable functions ae_seq hf p
and a measurable set ae_seq_set hf p, such that
μ (ae_seq_set hf p)ᶜ = 0x ∈ ae_seq_set hf p → ∀ i : ι, ae_seq hf hp i x = f i xx ∈ ae_seq_set hf p → p x (λ n, f n x)
def
ae_seq_set
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(p : α → (ι → β) → Prop) :
set α
If we have the additional hypothesis ∀ᵐ x ∂μ, p x (λ n, f n x), this is a measurable set
whose complement has measure 0 such that for all x ∈ ae_seq_set, f i x is equal to
(hf i).mk (f i) x for all i and we have the pointwise property p x (λ n, f n x).
Equations
- ae_seq_set hf p = (measure_theory.to_measurable μ {x : α | (∀ (i : ι), f i x = ae_measurable.mk (f i) _ x) ∧ p x (λ (n : ι), f n x)}ᶜ)ᶜ
noncomputable
def
ae_seq
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(p : α → (ι → β) → Prop) :
A sequence of measurable functions that are equal to f and verify property p on the
measurable set ae_seq_set hf p.
Equations
- ae_seq hf p = λ (i : ι) (x : α), ite (x ∈ ae_seq_set hf p) (ae_measurable.mk (f i) _ x) _.some
theorem
ae_seq.mk_eq_fun_of_mem_ae_seq_set
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
{x : α}
(hx : x ∈ ae_seq_set hf p)
(i : ι) :
ae_measurable.mk (f i) _ x = f i x
theorem
ae_seq.ae_seq_eq_mk_of_mem_ae_seq_set
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
{x : α}
(hx : x ∈ ae_seq_set hf p)
(i : ι) :
ae_seq hf p i x = ae_measurable.mk (f i) _ x
theorem
ae_seq.ae_seq_eq_fun_of_mem_ae_seq_set
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
{x : α}
(hx : x ∈ ae_seq_set hf p)
(i : ι) :
theorem
ae_seq.prop_of_mem_ae_seq_set
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
{x : α}
(hx : x ∈ ae_seq_set hf p) :
p x (λ (n : ι), ae_seq hf p n x)
theorem
ae_seq.fun_prop_of_mem_ae_seq_set
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
{x : α}
(hx : x ∈ ae_seq_set hf p) :
p x (λ (n : ι), f n x)
theorem
ae_seq.ae_seq_set_measurable_set
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
{hf : ∀ (i : ι), ae_measurable (f i) μ} :
measurable_set (ae_seq_set hf p)
theorem
ae_seq.measurable
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(p : α → (ι → β) → Prop)
(i : ι) :
measurable (ae_seq hf p i)
theorem
ae_seq.measure_compl_ae_seq_set_eq_zero
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
[countable ι]
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(hp : ∀ᵐ (x : α) ∂μ, p x (λ (n : ι), f n x)) :
⇑μ (ae_seq_set hf p)ᶜ = 0
theorem
ae_seq.ae_seq_eq_mk_ae
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
[countable ι]
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(hp : ∀ᵐ (x : α) ∂μ, p x (λ (n : ι), f n x)) :
theorem
ae_seq.ae_seq_eq_fun_ae
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
[countable ι]
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(hp : ∀ᵐ (x : α) ∂μ, p x (λ (n : ι), f n x)) :
theorem
ae_seq.ae_seq_n_eq_fun_n_ae
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
[countable ι]
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(hp : ∀ᵐ (x : α) ∂μ, p x (λ (n : ι), f n x))
(n : ι) :
theorem
ae_seq.supr
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : ι → α → β}
{μ : measure_theory.measure α}
{p : α → (ι → β) → Prop}
[complete_lattice β]
[countable ι]
(hf : ∀ (i : ι), ae_measurable (f i) μ)
(hp : ∀ᵐ (x : α) ∂μ, p x (λ (n : ι), f n x)) :