MeasureTheory.AEEqFun.coeFn_inf
theorem MeasureTheory.AEEqFun.coeFn_inf :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] [inst_2 : SemilatticeInf β] [inst_3 : ContinuousInf β] (f g : α →ₘ[μ] β),
μ.ae.EventuallyEq ↑(f ⊓ g) fun x => ↑f x ⊓ ↑g x
The theorem `MeasureTheory.AEEqFun.coeFn_inf` states that for any type `α` that has a structure of a measurable space and any type `β` that has a structure of a topological space, a semilattice (i.e., a poset in which every two elements have a greatest lower bound), and where the infimum operation is continuous, given any measure `μ` on `α` and any two almost everywhere-equal functions `f` and `g` from `α` to `β` (i.e., functions that are equal except on a set of measure zero), the infimum of `f` and `g` as almost everywhere-equal functions is equal almost everywhere (i.e., except potentially on a set of measure zero) to the function that maps every point to the infimum of the values of `f` and `g` at that point.
In mathematical notations, the theorem asserts that if `f, g : α →ₘ[μ] β`, then `f ⊓ g =ᶠ[μ] (λx, f(x) ⊓ g(x))` almost everywhere.
More concisely: For measurable spaces `α` with measure `μ` and topological spaces `β` where infima of continuous functions exist, if `f` and `g` are almost everywhere equal functions from `α` to `β`, then their infimum as almost everywhere equal functions is equal to the pointwise infimum almost everywhere.
|
MeasureTheory.AEEqFun.mk_eq_mk
theorem MeasureTheory.AEEqFun.mk_eq_mk :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] {f g : α → β} {hf : MeasureTheory.AEStronglyMeasurable f μ}
{hg : MeasureTheory.AEStronglyMeasurable g μ},
MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk g hg ↔ μ.ae.EventuallyEq f g
The theorem `MeasureTheory.AEEqFun.mk_eq_mk` states that for any given types `α` and `β`, where `α` is a measurable space and `β` is a topological space, and for any given measure `μ` on `α`, if `f` and `g` are two functions from `α` to `β` that are almost everywhere strongly measurable with respect to `μ`, then the equivalence classes of `f` and `g` (constructed via `MeasureTheory.AEEqFun.mk`) are equal if and only if `f` and `g` are almost everywhere equal with respect to the measure `μ`. This is to say, two functions are considered equivalent in this context if they are equal except on a set of measure zero.
More concisely: For measurable spaces `α` and topological spaces `β`, given a measure `μ` on `α` and almost everywhere strongly measurable functions `f` and `g` from `α` to `β`, `MeasureTheory.AEEqFun.mk_eq_mk` theorem states that `f` and `g` have equal equivalence classes if and only if they are almost everywhere equal with respect to `μ`.
|
MeasureTheory.AEEqFun.zero_toGerm
theorem MeasureTheory.AEEqFun.zero_toGerm :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] [inst_2 : Zero β], MeasureTheory.AEEqFun.toGerm 0 = 0
The theorem `MeasureTheory.AEEqFun.zero_toGerm` states that for any measurable space `α`, a measure `μ` on that space, and any topological space `β` that has a zero element, the germ of the zero function (which maps every element of `α` to the zero element of `β`) under the measure `μ` is also the zero element. In other words, when we convert the "almost everywhere equal" zero function to a germ with respect to `μ`, we get the zero germ.
More concisely: For any measurable space `α`, measure `μ` on `α`, and topological space `β` with a zero element, the germ of the constant zero function from `α` to `β` with respect to `μ` is equal to the zero germ.
|
MeasureTheory.AEEqFun.instSMul.proof_1
theorem MeasureTheory.AEEqFun.instSMul.proof_1 :
∀ {γ : Type u_1} [inst : TopologicalSpace γ] {𝕜 : Type u_2} [inst_1 : SMul 𝕜 γ] [inst_2 : ContinuousConstSMul 𝕜 γ]
(c : 𝕜), Continuous fun x => c • id x
This theorem states that for any type `γ` equipped with a topological space structure, and any type `𝕜` equipped with a scalar multiplication (`SMul`) operation, if the scalar multiplication operation is continuously constant, then for any element `c` of type `𝕜`, the function that maps each element `x` of type `γ` to `c` times `x` (denoted by `c • id x`) is continuous.
More concisely: If a scalar multiplication operation on a type `𝕜` is continuous and `γ` is a topological space, then the function that maps each element `x` in `γ` to `c` times `x` (`c • id x`) is continuous for all `c` in `𝕜`.
|
MeasureTheory.AEEqFun.add_toGerm
theorem MeasureTheory.AEEqFun.add_toGerm :
∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace γ] [inst_2 : Add γ] [inst_3 : ContinuousAdd γ] (f g : α →ₘ[μ] γ),
(f + g).toGerm = f.toGerm + g.toGerm
The theorem `MeasureTheory.AEEqFun.add_toGerm` establishes that for any two almost everywhere strongly measurable functions `f` and `g` from a type `α` to a type `γ` (where `α` has a measurable space structure, `γ` has an addition operation and topological structure, and addition operation is continuous), the germ at almost every point of the measure `μ` of the sum of `f` and `g` is equal to the sum of the germs of `f` and `g`. In other words, the operation of taking the germ commutes with the addition of functions.
More concisely: For almost everywhere strongly measurable functions `f` and `g` from a measurable space `(α, Σ, μ)` to a topological additive group `(γ, +)`, the germs at almost every point of `μ` of `f + g` are equal to the sum of the germs of `f` and `g`.
|
MeasureTheory.AEEqFun.cast.proof_1
theorem MeasureTheory.AEEqFun.cast.proof_1 :
∀ {α : Type u_2} {β : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] (f : α →ₘ[μ] β), MeasureTheory.AEStronglyMeasurable (↑(Quotient.out' f)) μ
The theorem `MeasureTheory.AEEqFun.cast.proof_1` states that for any measure space `α`, measure `μ` on `α`, and topological space `β`, if we have a function `f` from `α` to `β` that is equivalent almost everywhere (denoted by `α →ₘ[μ] β`), then the function obtained by taking the equivalence class of `f` under almost everywhere equality (`Quotient.out' f`) and casting it to a function (`↑(Quotient.out' f)`), is almost everywhere strongly measurable with respect to `μ`. In simpler terms, it says that the function that represents an equivalence class under almost everywhere equality is almost everywhere strongly measurable.
More concisely: For any measure space `(α, Σ, μ)`, topological space `(β, τ)`, and almost everywhere equal functions `f: α → β`, the quotient function `↑(Quotient.out' f): Σ → τ` is almost everywhere μ-measurable.
|
MeasureTheory.AEEqFun.aestronglyMeasurable
theorem MeasureTheory.AEEqFun.aestronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] (f : α →ₘ[μ] β), MeasureTheory.AEStronglyMeasurable (↑f) μ
This theorem states that for any measure space `α` and topological space `β`, given a measure `μ` on `α` and a function `f` from `α` to `β` that is almost everywhere equal with respect to `μ`, this function `f` is also almost everywhere strongly measurable with respect to `μ`. In other words, the function `f` is almost everywhere equivalent to some strongly measurable function.
More concisely: If `α` is a measure space, `β` is a topological space, `μ` is a measure on `α`, and `f: α → β` is almost everywhere equal to some strongly measurable function, then `f` is almost everywhere strongly measurable with respect to `μ`.
|
MeasureTheory.AEEqFun.mk_coeFn
theorem MeasureTheory.AEEqFun.mk_coeFn :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] (f : α →ₘ[μ] β), MeasureTheory.AEEqFun.mk ↑f ⋯ = f
This theorem in Lean 4 is stating that for any type `α` with a measurable space structure, any measure `μ` on `α`, and any type `β` with a topological space structure, if you have an almost everywhere equal function `f` from `α` to `β`, the operation of constructing an equivalence class of `f` using the function `MeasureTheory.AEEqFun.mk` with `f` as an argument (where the `f` is passed as a representative of its own equivalence class), will yield `f` itself. In other words, it asserts the consistency of the equivalence class construction process in the context of almost everywhere equal functions.
More concisely: For any measurable space `(α, Σ, μ)`, topological space `(β, τ)`, and almost everywhere equal functions `f : α → β`, `MeasureTheory.AEEqFun.mk μ τ f = f`.
|
MeasureTheory.AEEqFun.comp_toGerm
theorem MeasureTheory.AEEqFun.comp_toGerm :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β),
(MeasureTheory.AEEqFun.comp g hg f).toGerm = Filter.Germ.map g f.toGerm
The theorem `MeasureTheory.AEEqFun.comp_toGerm` states that for any measurable space `α`, measure `μ` on `α`, topological spaces `β` and `γ`, a continuous function `g` from `β` to `γ`, and a function `f` from `α` to `β` that is almost everywhere strongly measurable with respect to `μ`, the germ (i.e., equivalence class of functions that are equal almost everywhere) of the composition of `g` and `f` (with the continuity of `g` taken into consideration) is equal to the result of mapping `g` over the germ of `f`.
In other words, we can lift the function `g` to the level of germs, and this operation commutes with the process of turning a function into its germ under almost everywhere equality.
More concisely: The theorem asserts that for measurable spaces `α`, `μ`, topological spaces `β` and `γ`, a continuous function `g` from `β` to `γ`, and a strongly measurable `f` from `α` to `β` almost everywhere, the germ of `g ∘ f` equals the germ of `g` applied to the germ of `f`.
|
MeasureTheory.AEEqFun.ext
theorem MeasureTheory.AEEqFun.ext :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] {f g : α →ₘ[μ] β}, μ.ae.EventuallyEq ↑f ↑g → f = g
This theorem states that for any types `α` and `β`, where `α` is a measurable space and `β` is a topological space, and for any measure `μ` over `α`, if two almost everywhere equal functions `f` and `g` (from `α` to `β` respect to measure `μ`) are equal almost everywhere (i.e., they are equal except on a set of measure zero), then `f` and `g` are actually equal. This is a statement about the uniqueness of functions in the context of measure theory.
More concisely: If `α` is a measurable space, `β` is a topological space, `μ` is a measure on `α`, and functions `f` and `g` from `α` to `β` are almost everywhere equal with respect to `μ`, then `f` and `g` are equal.
|
MeasureTheory.AEEqFun.coeFn_comp
theorem MeasureTheory.AEEqFun.coeFn_comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β),
μ.ae.EventuallyEq (↑(MeasureTheory.AEEqFun.comp g hg f)) (g ∘ ↑f)
This theorem states that for any types `α`, `β`, and `γ`, given a measurable space on `α`, a measure `μ` on `α`, topological spaces on `β` and `γ`, a continuous function `g` from `β` to `γ`, and an almost everywhere equal function `f` from `α` to `β` (relative to measure `μ`), the function obtained by the composition of the continuous function `g` and the almost everywhere equal function `f` is almost everywhere equal to the function obtained by first applying `f` and then `g` (i.e., `g ∘ f`). Here, almost everywhere equal means that the set of points where two functions differ has measure zero.
More concisely: Given measurable spaces `(α, Σα)`, `(β, Σβ)`, `(γ, Σγ)`, measures `μ` on `(α, Σα)`, topological spaces `(β, τβ)`, `(γ, τγ)`, a continuous function `g : β → γ`, and an almost everywhere equal `μ`-\`μ`-measurable functions `f : α → β`, `g ∘ f` is almost everywhere equal to `f ∘ g`.
|
MeasureTheory.AEEqFun.coeFn_mk
theorem MeasureTheory.AEEqFun.coeFn_mk :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ),
μ.ae.EventuallyEq (↑(MeasureTheory.AEEqFun.mk f hf)) f
The theorem `MeasureTheory.AEEqFun.coeFn_mk` states that for any measurable space `α`, topological space `β`, measure `μ` on `α`, and function `f` from `α` to `β` that is almost everywhere strongly measurable with respect to `μ`, the function `f` is almost everywhere equal to the function represented by the equivalence class of `f` under the relation of being almost everywhere equal. This is determined by the `MeasureTheory.AEEqFun.mk` function, which constructs the equivalence class based on the equivalence relation of being almost everywhere equal. It is worth mentioning that the "almost everywhere" condition is defined with respect to the measure `μ`.
More concisely: For any measurable space `α`, topological space `β`, measure `μ` on `α`, and almost everywhere strongly measurable function `f` from `α` to `β` with respect to `μ`, `f` is almost everywhere equal to its equivalence class representative under the almost everywhere equality relation with respect to `μ`.
|
MeasureTheory.AEEqFun.coeFn_comp₂
theorem MeasureTheory.AEEqFun.coeFn_comp₂ :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α]
{μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
[inst_3 : TopologicalSpace δ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ), μ.ae.EventuallyEq ↑(MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂) fun a => g (↑f₁ a) (↑f₂ a)
This theorem, `MeasureTheory.AEEqFun.coeFn_comp₂`, states that for any types `α`, `β`, `γ`, and `δ` where `α` has a measurable space structure and `β`, `γ`, `δ` are topological spaces, and given a measure `μ` on `α`, and two "almost everywhere"-equal functions `f₁` and `f₂` from `α` to `β` and `γ` respectively, if we have a function `g` from `β` to `γ` to `δ` that is continuous when uncurried, then the "almost everywhere"-equality of `g` composed with `f₁` and `f₂` (using the function `MeasureTheory.AEEqFun.comp₂`) is the same as the function obtained by applying `g` to the values of `f₁` and `f₂` at each point `a` in the "almost everywhere" sense (i.e., for almost all points in `α` with respect to the measure `μ`).
More concisely: For measurable spaces `(α, Σα)`, topological spaces `(β, τβ)`, `(γ, τγ)`, and `(δ, τδ)`, and a measure `μ` on `α`, if `f₁`, `f₂` are almost everywhere equal functions from `α` to `β` and `γ` respectively, and `g` is a continuous function from `β × γ` to `δ`, then `MeasureTheory.AEEqFun.comp₂ g f₁ f₂` is almost everywhere equal to `g ∘ (f₁, f₂)` on `α`.
|
MeasureTheory.AEEqFun.comp₂_toGerm
theorem MeasureTheory.AEEqFun.comp₂_toGerm :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α]
{μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
[inst_3 : TopologicalSpace δ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β)
(f₂ : α →ₘ[μ] γ), (MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂).toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.toGerm
The theorem `MeasureTheory.AEEqFun.comp₂_toGerm` states that for any types `α`, `β`, `γ`, and `δ` where `α` is a measurable space and `β`, `γ`, and `δ` are topological spaces, and for any measure `μ` over `α`, you can take a continuous binary function `g` from `β` and `γ` to `δ` and two almost everywhere-equivalent functions `f₁` and `f₂` from `α` to `β` and `γ` respectively. With these, you can compose `g` with `f₁` and `f₂` to get a new function, and then convert this to a germ (a representative of an equivalence class of functions that are equal almost everywhere). This operation is the same as first converting `f₁` and `f₂` to germs and then applying the binary function `g` to them within the germ space. In essence, it shows that transforming functions to germs and then applying a binary operation is the same as first applying the operation and then transforming the result to a germ.
More concisely: Given measurable spaces `α`, topological spaces `β`, `γ`, and `δ`, measure `μ` over `α`, continuous binary function `g` from `β` and `γ` to `δ`, and almost everywhere-equivalent functions `f₁` and `f₂` from `α` to `β` and `γ` respectively, the germ of the composition `g ∘ (f₁, f₂)` is equal to the composition of the germs of `f₁` and `f₂` with `g` within the germ space.
|
MeasureTheory.AEEqFun.induction_on
theorem MeasureTheory.AEEqFun.induction_on :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] (f : α →ₘ[μ] β) {p : (α →ₘ[μ] β) → Prop},
(∀ (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ), p (MeasureTheory.AEEqFun.mk f hf)) → p f
This theorem, `MeasureTheory.AEEqFun.induction_on`, states that for any types `α` and `β`, where `α` has a measurable space structure and `β` has a topological space structure, for any measure `μ` on `α`, and for any equivalence class `f` of almost everywhere measurable functions from `α` to `β` with respect to `μ`, if a property `p` holds for all constructors `MeasureTheory.AEEqFun.mk f hf`, where `f` is a function from `α` to `β`, and `hf` is a proof that `f` is almost everywhere strongly measurable, then the property `p` holds for `f`. Essentially, it's a form of mathematical induction tailored for equivalence classes of almost everywhere measurable functions.
More concisely: If `α` is a measurable space, `β` is a topological space, `μ` is a measure on `α`, `f` is an almost everywhere measurable function from `α` to `β`, and `p` is a property such that `p` holds for all constructors `MeasureTheory.AEEqFun.mk f hf`, then `p` holds for `f`.
|
MeasureTheory.AEEqFun.one_toGerm
theorem MeasureTheory.AEEqFun.one_toGerm :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] [inst_2 : One β], MeasureTheory.AEEqFun.toGerm 1 = 1
The theorem `MeasureTheory.AEEqFun.one_toGerm` states that for any types `α` and `β`, if `α` is a measurable space, `μ` is a measure on `α`, and `β` is a topological space with a specified one element, then the process of converting the constantly `1` valued equivalence class of functions (`1` is interpreted as the class of all measurable functions which equal `1` almost everywhere with respect to the measure `μ`) from `α` to `β` into a germ at almost every point with respect to `μ` (essentially "forgetting" that these functions are equal almost everywhere) results in the constant germ `1` at almost every point. In other words, the germ of the constant function `1` is just `1`.
More concisely: For any measurable spaces `α` and topological spaces `β` with a single element, the germ of the constant measurable function equal to 1 almost everywhere with respect to a measure `μ` on `α` is equal to the constant germ 1 on `β`.
|
MeasureTheory.AEEqFun.coeFn_add
theorem MeasureTheory.AEEqFun.coeFn_add :
∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace γ] [inst_2 : Add γ] [inst_3 : ContinuousAdd γ] (f g : α →ₘ[μ] γ),
μ.ae.EventuallyEq (↑(f + g)) (↑f + ↑g)
This theorem states that for any measurable space 'α' and topological space 'γ' with defined addition and continuity under addition, the function evaluation of the sum of two almost everywhere equal functions 'f' and 'g' (under the measure 'μ') is almost everywhere equal to the sum of the function evaluations of 'f' and 'g' individually. In simpler terms, it asserts that the addition operation for almost everywhere equal functions distributes over the function evaluations almost everywhere. This is under the condition that the functions are defined almost everywhere with respect to the measure 'μ'.
More concisely: For measurable functions $f, g : \alpha \rightarrow \gamma$ that are almost everywhere equal with respect to a measure $\mu$, the almost everywhere pointwise sum $f + g$ is almost everywhere equal to the pointwise sum of $f$ and $g$.
|
MeasureTheory.AEEqFun.mul_toGerm
theorem MeasureTheory.AEEqFun.mul_toGerm :
∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace γ] [inst_2 : Mul γ] [inst_3 : ContinuousMul γ] (f g : α →ₘ[μ] γ),
(f * g).toGerm = f.toGerm * g.toGerm
The theorem `MeasureTheory.AEEqFun.mul_toGerm` states that for any measurable space `α`, any type `γ` with a topological structure and a continuous multiplication operation, and any measure `μ` on `α`, given two almost everywhere-equal functions `f` and `g` from `α` to `γ` (denoted as `f, g : α →ₘ[μ] γ`), the germ (i.e., equivalence class under the relation of equality almost everywhere) of the product function `(f * g)` is equal to the product of the germs of `f` and `g`.
In other words, this theorem is about the compatibility of the operation of multiplication with the operation of taking germs for almost everywhere-equal functions. It says that multiplying the functions first and then taking the germ gives the same result as first taking the germs and then multiplying them.
More concisely: For measurable functions `f` and `g` almost everywhere equal on the measurable space `(α, Σ, μ)`, their product function `f * g` has the same germ (equivalence class under equality almost everywhere) as the pointwise product of their germs.
|
MeasureTheory.AEEqFun.induction_on₂
theorem MeasureTheory.AEEqFun.induction_on₂ :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] {α' : Type u_5} {β' : Type u_6} [inst_2 : MeasurableSpace α']
[inst_3 : TopologicalSpace β'] {μ' : MeasureTheory.Measure α'} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β')
{p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → Prop},
(∀ (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ) (f' : α' → β')
(hf' : MeasureTheory.AEStronglyMeasurable f' μ'),
p (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.mk f' hf')) →
p f f'
The theorem `MeasureTheory.AEEqFun.induction_on₂` states that for any two equivalence classes of almost everywhere strongly measurable functions `f` and `f'` (represented as `α →ₘ[μ] β` and `α' →ₘ[μ'] β'`), with respect to measures `μ` and `μ'`, and a property `p` that holds for the equivalence classes of all such functions, if the property `p` holds for the classes constructed from all almost everywhere strongly measurable functions `f` and `f'` (using the constructor `MeasureTheory.AEEqFun.mk`), then the property `p` must also hold for the equivalence classes `f` and `f'`. This can be seen as an induction principle for equivalence classes of almost everywhere strongly measurable functions.
More concisely: If `p` is a property that holds for the equivalence classes of all almost everywhere strongly measurable functions `f : α →ₘ[μ] β` and `f' : α' →ₘ[μ'] β'`, and `p` holds for the classes constructed from all such functions using the constructor `MeasureTheory.AEEqFun.mk`, then `p` also holds for the equivalence classes `f` and `f'`.
|
MeasureTheory.AEEqFun.coeFn_le
theorem MeasureTheory.AEEqFun.coeFn_le :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] [inst_2 : Preorder β] {f g : α →ₘ[μ] β}, μ.ae.EventuallyLE ↑f ↑g ↔ f ≤ g
This theorem states that for any types `α` and `β`, given a measurable space over `α`, a measure `μ` on that space, a topological space over `β`, a preorder (an order relation that is reflexive and transitive) on `β`, and two functions `f` and `g` from `α` to `β` that are equal almost everywhere with respect to measure `μ`, the function `f` is less than or equal to function `g` almost everywhere (with respect to the filter of co-null sets of the measure `μ`) if and only if `f` is less than or equal to `g`. Basically, this theorem establishes the connection between the pointwise order of functions and the order in the space of functions that are equal almost everywhere.
More concisely: Given measurable spaces `(α, ℳα)` and `(β, ℳβ)`, measures `μ` on `α`, a topological space `(β, τ)`, a preorder relation `≤` on `β`, and functions `f, g : α → β` equal almost everywhere with respect to `μ`, if `f ≤ g` almost everywhere with respect to the filter of co-null sets of `μ`, then `f ≤ g` pointwise.
|
MeasureTheory.AEEqFun.smul_toGerm
theorem MeasureTheory.AEEqFun.smul_toGerm :
∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace γ] {𝕜 : Type u_5} [inst_2 : SMul 𝕜 γ] [inst_3 : ContinuousConstSMul 𝕜 γ] (c : 𝕜)
(f : α →ₘ[μ] γ), (c • f).toGerm = c • f.toGerm
The theorem `MeasureTheory.AEEqFun.smul_toGerm` states that for any types `α`, `γ` and `𝕜`, given a measurable space instance for `α`, a measure `μ` on `α`, a topological space instance for `γ`, an instance of scalar multiplication (`SMul`) on `𝕜` and `γ`, and an instance of continuous constant scalar multiplication (`ContinuousConstSMul`) on `𝕜` and `γ`, for any scalar `c` of type `𝕜` and any function `f` from `α` to `γ` that is almost everywhere equal with respect to the measure `μ`, the germ (i.e., equivalence class of functions equal almost everywhere) of the scalar multiplication of `c` and `f` (denoted as `c • f`) is equal to the scalar multiplication of `c` and the germ of `f`. In other words, scalar multiplication commutes with the operation of taking germs of functions that are almost everywhere equal.
More concisely: For measurable functions `f: α → γ` and scalars `c` in a commutative ring `𝕜` with a measure `μ` on `α`, continuous scalar multiplication, and assuming `f` and `c • f` are equal almost everywhere, their germs are equal: `germ (c • f) = germ (c * f)`.
|
MeasureTheory.AEEqFun.coeFn_compMeasurePreserving
theorem MeasureTheory.AEEqFun.coeFn_compMeasurePreserving :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β}
(g : β →ₘ[ν] γ) (hf : MeasureTheory.MeasurePreserving f μ ν),
μ.ae.EventuallyEq (↑(g.compMeasurePreserving f hf)) (↑g ∘ f)
This theorem states that for every three types `α`, `β`, and `γ`, where `α` is a measurable space and `γ` is a topological space, for every measures `μ` on `α` and `ν` on `β`, for every function `f` from `α` to `β`, and for every almost everywhere equal function `g` from `β` to `γ` with respect to `ν`, if `f` is measure-preserving with respect to `μ` and `ν`, then the function obtained by composing `g` and `f` (in the sense of almost everywhere equal functions) is the same (up to a set of measure zero) as the function obtained by composing `g` and `f` in the usual sense, almost everywhere with respect to `μ`.
In other words, the composition of almost everywhere equal functions respects the composition of ordinary functions, provided we deal with measure-preserving functions and ignore differences on null sets.
More concisely: Given measurable spaces `α`, `β`, and `γ`, measures `μ` on `α` and `ν` on `β`, a measure-preserving function `f: α → β` between them, and almost everywhere equal functions `g: β → γ` and `h = g ∘ f: α → γ`, then `h` is almost everywhere equal to `g ∘ f` (ignoring null sets).
|
MeasureTheory.AEEqFun.coeFn_const
theorem MeasureTheory.AEEqFun.coeFn_const :
∀ (α : Type u_1) {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] (b : β),
μ.ae.EventuallyEq (↑(MeasureTheory.AEEqFun.const α b)) (Function.const α b)
The theorem `MeasureTheory.AEEqFun.coeFn_const` states that for any measurable space `α`, any topological space `β`, any measure `μ` on `α`, and any constant `b` of type `β`, the equivalence class of the constant function `b` (created using `MeasureTheory.AEEqFun.const`), when coerced, is almost everywhere equal (according to the measure `μ`) to the constant function `b` (created using `Function.const`). This theorem establishes a connection between the constant functions defined in the context of measure theory and typical constant functions.
More concisely: For any measurable space α, topological space β, measure μ on α, and constant b of type β, the coerced equivalence class of the constant function `MeasureTheory.AEEqFun.const b` is almost everywhere equal to the standard constant function `Function.const b`.
|
MeasureTheory.AEEqFun.coeFn_sup
theorem MeasureTheory.AEEqFun.coeFn_sup :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] [inst_2 : SemilatticeSup β] [inst_3 : ContinuousSup β] (f g : α →ₘ[μ] β),
μ.ae.EventuallyEq ↑(f ⊔ g) fun x => ↑f x ⊔ ↑g x
The theorem `MeasureTheory.AEEqFun.coeFn_sup` states that for any two almost everywhere equal functions `f` and `g` from a measurable space `α` to a topological space `β` equipped with a semilattice structure and a continuous supremum operation, and for any measure `μ` on `α`, the supremum of `f` and `g` (denoted by `f ⊔ g`) is also an almost everywhere equal function. Moreover, this supremum function is almost everywhere equal to the function that sends each point `x` in `α` to the supremum of the values of `f` and `g` at `x` (denoted by `↑f x ⊔ ↑g x`). The equality is almost everywhere with respect to the measure `μ`, meaning that the set of points in `α` where the two functions do not agree has measure zero.
More concisely: For measurable functions $f$ and $g$ from a measurable space to a topological semilattice with a continuous supremum operation, if $f$ and $g$ are almost everywhere equal with respect to some measure, then their supremum is almost everywhere equal to the pointwise supremum, and this equality holds almost everywhere with respect to the measure.
|
MeasureTheory.AEEqFun.instNeg.proof_1
theorem MeasureTheory.AEEqFun.instNeg.proof_1 :
∀ {γ : Type u_1} [inst : TopologicalSpace γ] [inst_1 : AddGroup γ] [inst_2 : TopologicalAddGroup γ],
Continuous fun a => -a
This theorem states that for any type `γ`, if `γ` is a topological space, an additive group, and a topological additive group, then the function that takes an element `a` from `γ` and returns its additive inverse `-a` is a continuous function. In mathematical terms, for all `a` in `γ`, the function `f(a) = -a` is continuous. This means that for any sequence of elements in `γ` converging to `a`, their additive inverses also converge to `-a`.
More concisely: If `γ` is a topological space, an additive group, then the additive inverse function `a ↔- a` is a continuous function on `γ`.
|
MeasureTheory.AEEqFun.stronglyMeasurable
theorem MeasureTheory.AEEqFun.stronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace β] (f : α →ₘ[μ] β), MeasureTheory.StronglyMeasurable ↑f
This theorem states that for any given measurable space 'α', measure 'μ' of 'α', and any function 'f' from 'α' to topological space 'β' (where 'f' is an equivalence class of measurable functions modulo almost everywhere equality with respect to measure 'μ'), the function 'f' is strongly measurable. Here, a function is defined as being strongly measurable if it is the limit of simple functions, in a sense that for every point in 'α', the function values at that point given by the sequence of simple functions converges to the function value of 'f' at that point.
More concisely: Given a measurable space 'α', measure 'μ', and a measurable function 'f' from 'α' to a topological space 'β' (up to almost everywhere equality), 'f' is strongly measurable if and only if it is the limit of measurable simple functions.
|