Documentation

Mathlib.MeasureTheory.Function.AEMeasurableSequence

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

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
Instances For
    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
    Instances For
      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) μ} :
      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} [CompleteLattice β] [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} [CompleteLattice β] [Countable ι] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) => f n x) :
      ⨅ (n : ι), aeSeq hf p n =ᵐ[μ] ⨅ (n : ι), f n