Commit 2023-05-29 14:32 6e48706d

View on Github →

feat: port MeasureTheory.Measure.Complex (#4471)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Complex.lean

added theorem MeasureTheory.ComplexMeasure.absolutelyContinuous_eNNReal_iff

added def MeasureTheory.ComplexMeasure.equivSignedMeasure

added def MeasureTheory.ComplexMeasure.equivSignedMeasureₗ

added def MeasureTheory.ComplexMeasure.im

added def MeasureTheory.ComplexMeasure.re

added theorem MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure

added theorem MeasureTheory.SignedMeasure.im_toComplexMeasure

added theorem MeasureTheory.SignedMeasure.re_toComplexMeasure

added def MeasureTheory.SignedMeasure.toComplexMeasure

added theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply