aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
theorem aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet :
∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{f : ι → α → β} {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ)
{x : α}, x ∈ aeSeqSet hf p → ∀ (i : ι), aeSeq hf p i x = f i x
The theorem `aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet` states that for all indices `ι`, real numbers `α`, and real numbers `β` (where `α` and `β` have defined measurable spaces), given a function `f : ι → α → β`, a measure `μ : MeasureTheory.Measure α`, and a property `p : α → (ι → β) → Prop`, if all functions `f i` are almost everywhere measurable with measure `μ`, then for all `x : α` in the set `aeSeqSet hf p`, the function `aeSeq hf p i` equals `f i` at `x`. In simpler terms, this theorem says that in a sequence of almost everywhere measurable functions that equal `f` and satisfy property `p` on a given measurable set, any function in that sequence equals `f` at every point in that set.
More concisely: Given a measurable space `(α, Σ, μ)`, a function `f : ι → α → β`, and a property `p : α → (ι → β) → Prop`, if all functions `f i` are almost everywhere measurable with respect to `μ` and for all `x ∈ aeSeqSet hf p`, we have `aeSeq hf p i x = f i x`, where `hf` is a hypothesis proving `i` is almost everywhere defined by `p` with respect to `μ`.
|
aeSeq.measure_compl_aeSeqSet_eq_zero
theorem aeSeq.measure_compl_aeSeqSet_eq_zero :
∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{f : ι → α → β} {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [inst_2 : Countable ι]
(hf : ∀ (i : ι), AEMeasurable (f i) μ), (∀ᵐ (x : α) ∂μ, p x fun n => f n x) → ↑↑μ (aeSeqSet hf p)ᶜ = 0
This theorem states that for any type `ι`, `α`, and `β`, given measurable spaces over `α` and `β`, a function `f` from `ι` to a function from `α` to `β`, a measure `μ` on `α`, and a predicate `p` on `α` and a function from `ι` to `β`, given that `ι` is countable and for all `i` in `ι`, `f i` is almost everywhere measurable with respect to `μ`, if almost everywhere for `x` in `α`, `p x` applied to the function `n => f n x` holds, then the measure of the complement of the set where the sequence `f` is almost everywhere equal to a measurable sequence with respect to the predicate `p` is zero.
This essentially means that if we have a countable collection of functions that are almost everywhere measurable, and a property that holds almost everywhere, then the set of points where our sequence differs from a measurable sequence satisfying the property has measure zero.
More concisely: Given a countable family of almost everywhere measurable functions `f_i : ι → α → β` from a countable index type `ι` to measurable spaces `(α, Σα)` and `(β, Σβ)`, a measurable predicate `p : α → Prop`, and a measure `μ : Σα`, if for all `i` in `ι` and almost every `x` in `α`, `p x` holds for `f_i x`, then the measure of the set where the sequence `f_i` fails to converge almost everywhere to a measurable function satisfying `p` is zero.
|
aeSeq.proof_1
theorem aeSeq.proof_1 : ∀ {ι : Sort u_3} {α : Type u_2} {β : Type u_1} {f : ι → α → β}, ι → α → Nonempty β
This theorem states that for any sort `ι`, any types `α` and `β`, and any function `f` mapping from `ι` and `α` to `β`, there exists a value in `β` for any given `ι` and `α`. In other words, no matter the specifics of `ι`, `α`, `β`, and `f`, it's assured that we can always find a value in `β` when provided with any `ι` and `α`.
More concisely: For any sort `ι`, types `α` and `β`, and function `f`: ∀ (i : ι) (x : α), ∃ y : β, f i x.
|