# 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 AEMeasurable functions. Given a sequence of a.e.-measurable functions f : ι → α → β with hypothesis hf : ∀ i, AEMeasurable (f i) μ, and a pointwise property p : α → (ι → β) → Prop such that we have hp : ∀ᵐ x ∂μ, p x (fun n ↦ f n x), we define a sequence of measurable functions aeSeq hf p and a measurable set aeSeqSet hf p, such that

• μ (aeSeqSet hf p)ᶜ = 0
• x ∈ aeSeqSet hf p → ∀ i : ι, aeSeq hf hp i x = f i x
• x ∈ aeSeqSet hf p → p x (fun n ↦ f n x)
def aeSeqSet {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } (hf : ∀ (i : ι), AEMeasurable (f i) μ) (p : α(ιβ)Prop) :
Set α

If we have the additional hypothesis ∀ᵐ x ∂μ, p x (fun n ↦ f n x), this is a measurable set whose complement has measure 0 such that for all x ∈ aeSeqSet, f i x is equal to (hf i).mk (f i) x for all i and we have the pointwise property p x (fun n ↦ f n x).

Equations
Instances For
noncomputable def aeSeq {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } (hf : ∀ (i : ι), AEMeasurable (f i) μ) (p : α(ιβ)Prop) :
ιαβ

A sequence of measurable functions that are equal to f and verify property p on the measurable set aeSeqSet hf p.

Equations
Instances For
theorem aeSeq.mk_eq_fun_of_mem_aeSeqSet {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α} (hx : x aeSeqSet hf p) (i : ι) :
AEMeasurable.mk (f i) x = f i x
theorem aeSeq.aeSeq_eq_mk_of_mem_aeSeqSet {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α} (hx : x aeSeqSet hf p) (i : ι) :
aeSeq hf p i x = AEMeasurable.mk (f i) x
theorem aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α} (hx : x aeSeqSet hf p) (i : ι) :
aeSeq hf p i x = f i x
theorem aeSeq.prop_of_mem_aeSeqSet {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α} (hx : x aeSeqSet hf p) :
p x fun (n : ι) => aeSeq hf p n x
theorem aeSeq.fun_prop_of_mem_aeSeqSet {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α} (hx : x aeSeqSet hf p) :
p x fun (n : ι) => f n x
theorem aeSeq.aeSeqSet_measurableSet {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} {hf : ∀ (i : ι), AEMeasurable (f i) μ} :
theorem aeSeq.measurable {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } (hf : ∀ (i : ι), AEMeasurable (f i) μ) (p : α(ιβ)Prop) (i : ι) :
Measurable (aeSeq hf p i)
theorem aeSeq.measure_compl_aeSeqSet_eq_zero {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} [] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) => f n x) :
μ (aeSeqSet hf p) = 0
theorem aeSeq.aeSeq_eq_mk_ae {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} [] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) => f n x) :
∀ᵐ (a : α) ∂μ, ∀ (i : ι), aeSeq hf p i a = AEMeasurable.mk (f i) a
theorem aeSeq.aeSeq_eq_fun_ae {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} [] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) => f n x) :
∀ᵐ (a : α) ∂μ, ∀ (i : ι), aeSeq hf p i a = f i a
theorem aeSeq.aeSeq_n_eq_fun_n_ae {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} [] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) => f n x) (n : ι) :
aeSeq hf p n =ᵐ[μ] f n
theorem aeSeq.iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} [] [] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) => f n x) :
⨆ (n : ι), aeSeq hf p n =ᵐ[μ] ⨆ (n : ι), f n
theorem aeSeq.iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ιαβ} {μ : } {p : α(ιβ)Prop} [] [] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) => f n x) :
⨅ (n : ι), aeSeq hf p n =ᵐ[μ] ⨅ (n : ι), f n