toFinite — Mathlib

English

For Measurable f,g: G→ℝ≥0∞, μ.withDensity f ∗ μ.withDensity g = μ.withDensity (mlconvolution f g μ).

Русский

Для измеримых f,g: G→ℝ≥0∞, μ.withDensity f ∗ μ.withDensity g = μ.withDensity (mlconvolution f g μ).

LaTeX

$$$ μ^{f} * μ^{g} = μ^{(mlconvolution f g μ)} $$$

Lean4

/-- A finite measure obtained from an s-finite measure `μ`, such that
`μ = μ.toFinite.withDensity (μ.rnDeriv µ.toFinite)`
(see `MeasureTheory.Measure.withDensity_rnDeriv_eq` along with
`MeasureTheory.absolutelyContinuous_toFinite`). If `μ` is non-zero, then `μ.toFinite` is a
probability measure. -/
noncomputable def toFinite (μ : Measure α) [SFinite μ] : Measure α :=
  μ.toFiniteAux[|univ]

Похожие утверждения