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
- aeSeqSet hf p = (MeasureTheory.toMeasurable μ {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) => f n x}ᶜ)ᶜ
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
- aeSeq hf p i x = if x ∈ aeSeqSet hf p then AEMeasurable.mk (f i) ⋯ x else Nonempty.some ⋯
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 : ι)
:
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)
:
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)
:
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 =ᶠ[MeasureTheory.Measure.ae μ] 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 =ᶠ[MeasureTheory.Measure.ae μ] ⨆ (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 =ᶠ[MeasureTheory.Measure.ae μ] ⨅ (n : ι), f n