mathlib3 documentation


Complex measure #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves some elementary results about complex measures. In particular, we prove that a complex measure is always in the form s + it where s and t are signed measures.

The complex measure is defined to be vector measure over , this definition can be found in measure_theory.measure.vector_measure and is known as measure_theory.complex_measure.

Main definitions #

Tags #

Complex measure

Given s and t signed measures, s + it is a complex measure


The complex measures form an equivalence to the type of pairs of signed measures.