mathlib documentation

measure_theory.function.ae_measurable_sequence

Sequence of measurable functions associated to a sequence of a.e.-measurable functions #

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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [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
def ae_seq {α : Type u_1} {β : Type u_2} {ι : Type u_4} [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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [measurable_space α] [measurable_space β] {f : ι → α → β} {μ : measure_theory.measure α} {p : α → (ι → β) → Prop} {hf : ∀ (i : ι), ae_measurable (f i) μ} :
theorem ae_seq.measurable {α : Type u_1} {β : Type u_2} {ι : Type u_4} [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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [measurable_space α] [measurable_space β] {f : ι → α → β} {μ : measure_theory.measure α} {p : α → (ι → β) → Prop} [encodable ι] (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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [measurable_space α] [measurable_space β] {f : ι → α → β} {μ : measure_theory.measure α} {p : α → (ι → β) → Prop} [encodable ι] (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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [measurable_space α] [measurable_space β] {f : ι → α → β} {μ : measure_theory.measure α} {p : α → (ι → β) → Prop} [encodable ι] (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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [measurable_space α] [measurable_space β] {f : ι → α → β} {μ : measure_theory.measure α} {p : α → (ι → β) → Prop} [encodable ι] (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 {α : Type u_1} {β : Type u_2} {ι : Type u_4} [measurable_space α] [measurable_space β] {f : ι → α → β} {μ : measure_theory.measure α} {p : α → (ι → β) → Prop} [complete_lattice β] [encodable ι] (hf : ∀ (i : ι), ae_measurable (f i) μ) (hp : ∀ᵐ (x : α) ∂μ, p x (λ (n : ι), f n x)) :
(⨆ (n : ι), ae_seq hf p n) =ᵐ[μ] ⨆ (n : ι), f n