mathlib3 documentation

measure_theory.function.ae_measurable_sequence

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

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
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
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 : ι) :
ae_seq hf p i x = f i x
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) μ} :
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 : ι) :
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)) :
∀ᵐ (a : α) μ, (i : ι), ae_seq hf p i a = ae_measurable.mk (f i) _ a
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)) :
∀ᵐ (a : α) μ, (i : ι), ae_seq hf p i a = f i a
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 : ι) :
ae_seq hf p n =ᵐ[μ] f 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)) :
( (n : ι), ae_seq hf p n) =ᵐ[μ] (n : ι), f n