MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq
theorem MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f g : α → E},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable g μ → μ.withDensityᵥ f = μ.withDensityᵥ g → μ.ae.EventuallyEq f g
The theorem states that for any measurable space `α` and measure `μ` on that space, and for any two functions `f` and `g` from `α` to a real complete normed group `E`, if both `f` and `g` are integrable with respect to `μ`, and the measures with respect to `μ` considering `f` and `g` as densities are the same, then `f` and `g` are equal almost everywhere. In other words, if two functions have the same density with respect to a measure, they differ only on a set of measure zero.
More concisely: If two integrable functions from a measurable space to a real complete normed group have the same density with respect to a measure, then they are equal almost everywhere.
|
MeasureTheory.withDensityᵥ_apply
theorem MeasureTheory.withDensityᵥ_apply :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] {f : α → E},
MeasureTheory.Integrable f μ → ∀ {s : Set α}, MeasurableSet s → ↑(μ.withDensityᵥ f) s = ∫ (x : α) in s, f x ∂μ
The theorem `MeasureTheory.withDensityᵥ_apply` states that for any types `α` and `E`, a measurable space `m` on `α`, a measure `μ` on `α`, and a function `f` from `α` to `E` where `E` is a normed add commutative group and also a normed space over the reals, if `f` is integrable with respect to the measure `μ`, then for any set `s` of type `α` that is a measurable set, the measure with density of `μ` with respect to `f` applied on `s` is equal to the definite integral of `f` over the set `s` with respect to the measure `μ`. In mathematical terms, this theorem asserts that given a measure `μ` and an integrable function `f`, the measure with density `f` with respect to `μ` evaluated on a measurable set `s` is equal to the integral of `f` over `s` with respect to `μ`, denoted as `∫ (x : α) in s, f x ∂μ`.
More concisely: For any measurable space `(α, μ)`, measurable set `s ⊆ α`, integrable function `f : α → E` (where `E` is a normed add commutative group and normed space over the reals), the measure with density of `μ` with respect to `f` on `s` equals the definite integral of `f` over `s` with respect to `μ`, i.e., `∫ (x : α) in s, f x ∂μ = μ(s, f)`.
|
MeasureTheory.withDensityᵥ_add
theorem MeasureTheory.withDensityᵥ_add :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] {f g : α → E},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable g μ → μ.withDensityᵥ (f + g) = μ.withDensityᵥ f + μ.withDensityᵥ g
The theorem `MeasureTheory.withDensityᵥ_add` states that for a measurable space `α`, equipped with a measure `μ`, and a normed add commutative group `E` that also forms a normed space over the real numbers, if two functions `f` and `g` from `α` to `E` are both integrable with respect to `μ`, then the measure with density of the sum of `f` and `g` is equal to the sum of the measure with density of `f` and the measure with density of `g`. This is essentially a linearity property of the operation of forming a measure with density.
More concisely: For measurable functions `f` and `g` from a measurable space `(α, Σ, μ)` to a normed add commutative group `E` over the real numbers, their sum `f + g` has the same measure with density as the sum of their individual measures with density, i.e., `∫(f + g) dμ = ∫f dμ + ∫g dμ`.
|
MeasureTheory.withDensityᵥ_neg
theorem MeasureTheory.withDensityᵥ_neg :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace ℝ E] {f : α → E}, μ.withDensityᵥ (-f) = -μ.withDensityᵥ f
This theorem states that for any measurable space `α` with a measure `μ`, and any real-valued function `f` defined on `α`, the measure with density `-f` is equal to the negation of the measure with density `f`. Here, `E` is any normed additive commutative group that is also a normed space over the real numbers. In other words, the measure-theoretic "with density" operation preserves the negation operation.
More concisely: For any measurable space `(α, Σ, μ)` and real-valued function `f` on `α`, the measure `μ` with density `-f` is equal to the negative of the measure with density `f`, i.e., `-μ{f} = μ{-f}`.
|