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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} (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

• aeSeqSet hf p = (MeasureTheory.toMeasurable μ {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) => f n x}ᶜ)ᶜ

noncomputable def aeSeq {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} (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

• aeSeq hf p i x = if x ∈ aeSeqSet hf p then AEMeasurable.mk (f i) ⋯ x else ⋯.some

theorem aeSeq.mk_eq_fun_of_mem_aeSeqSet {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} {hf : ∀ (i : ι), AEMeasurable (f i) μ} : MeasurableSet (aeSeqSet hf p)

theorem aeSeq.measurable {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} (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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [Countable ι] (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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [Countable ι] (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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [Countable ι] (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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [Countable ι] (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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [SupSet β] [Countable ι] (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} [MeasurableSpace α] [MeasurableSpace β] {f : ι → α → β} {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [InfSet β] [Countable ι] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) => f n x) : ⨅ (n : ι), aeSeq hf p n =ᵐ[μ] ⨅ (n : ι), f n