absolutelyContinuous_ennreal_iff — Mathlib

English

A complex measure c is absolutely continuous with respect to a vector measure μ valued in ENNReal iff both its real and imaginary parts are absolutely continuous with respect to μ.

Русский

Комплексная мера c абсолютно непрерывна по отношению к векторной мере μ, если и только если и ее вещественная и мнимая части являются абсолютно непрерывными по отношению к μ.

LaTeX

$$c ≪ᵥ μ ↔ (re c ≪ᵥ μ) ∧ (im c ≪ᵥ μ)$$

Lean4

theorem absolutelyContinuous_ennreal_iff (c : ComplexMeasure α) (μ : VectorMeasure α ℝ≥0∞) :
    c ≪ᵥ μ ↔ ComplexMeasure.re c ≪ᵥ μ ∧ ComplexMeasure.im c ≪ᵥ μ :=
  by
  constructor <;> intro h
  · constructor <;> · intro i hi; simp [h hi]
  · intro i hi
    rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]
    exacts [by simp, h.2 hi, h.1 hi]

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