toComplexMeasure — Mathlib

English

For any signed measures s,t and set i, the i-th value of s.toComplexMeasure t is the pair (s i, t i).

Русский

Для любых смешанных мер s,t и множества i значение i-й компоненты s.toComplexMeasure t равно паре (s i, t i).

LaTeX

$$s.toComplexMeasure t i = ⟨s i, t i⟩$$

Lean4

/-- Given `s` and `t` signed measures, `s + it` is a complex measure -/
@[simps!]
def _root_.MeasureTheory.SignedMeasure.toComplexMeasure (s t : SignedMeasure α) : ComplexMeasure α
    where
  measureOf' i := ⟨s i, t i⟩
  empty' := by rw [s.empty, t.empty]; rfl
  not_measurable' i hi := by rw [s.not_measurable hi, t.not_measurable hi]; rfl
  m_iUnion' _ hf hfdisj := (Complex.hasSum_iff _ _).2 ⟨s.m_iUnion hf hfdisj, t.m_iUnion hf hfdisj⟩

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