English
If μ ≪ ν and f is μ-integrable, then ν.withDensityᵥ (μ.rnDeriv ν x).toReal • f equals μ.withDensityᵥ f as a vector measure.
Русский
Если μ прерывисто относится к ν и f интегрируема по μ, тогда объем с density RNDeriv μ на f в ν совпадает с μ.withDensityᵥ f как векторная мера.
LaTeX
$$$ ν.withDensityᵥ ( (μ.rnDeriv ν x).toReal • f(x) ) = μ.withDensityᵥ f $$$
Lean4
/-- Given a measure `μ` and an integrable function `f`, `μ.withDensityᵥ f` is
the vector measure which maps the set `s` to `∫ₛ f ∂μ`. -/
def withDensityᵥ {m : MeasurableSpace α} (μ : Measure α) (f : α → E) : VectorMeasure α E :=
if hf : Integrable f μ then
{ measureOf' := fun s => if MeasurableSet s then ∫ x in s, f x ∂μ else 0
empty' := by simp
not_measurable' := fun _ hs => if_neg hs
m_iUnion' := fun s hs₁ hs₂ =>
by
convert hasSum_integral_iUnion hs₁ hs₂ hf.integrableOn with n
· rw [if_pos (hs₁ n)]
· rw [if_pos (MeasurableSet.iUnion hs₁)] }
else 0
