Documentation

Mathlib.MeasureTheory.Measure.Complex

Complex measure #

This file defines a complex measure to be a vector measure with codomain . Then we prove 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.

Main definitions #

Tags #

Complex measure

@[reducible, inline]
abbrev MeasureTheory.ComplexMeasure (α : Type u_2) [MeasurableSpace α] :
Type (max u_2 0)

A ComplexMeasure is a -vector measure.

Equations
Instances For
    @[simp]
    theorem MeasureTheory.ComplexMeasure.re_apply {α : Type u_1} {m : MeasurableSpace α} (v : MeasureTheory.VectorMeasure α ) :
    MeasureTheory.ComplexMeasure.re v = v.mapRange Complex.reLm.toAddMonoidHom Complex.continuous_re

    The real part of a complex measure is a signed measure.

    Equations
    Instances For
      @[simp]
      theorem MeasureTheory.ComplexMeasure.im_apply {α : Type u_1} {m : MeasurableSpace α} (v : MeasureTheory.VectorMeasure α ) :
      MeasureTheory.ComplexMeasure.im v = v.mapRange Complex.imLm.toAddMonoidHom Complex.continuous_im

      The imaginary part of a complex measure is a signed measure.

      Equations
      Instances For
        @[simp]
        theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply_re {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (t : MeasureTheory.SignedMeasure α) (i : Set α) :
        ((s.toComplexMeasure t) i).re = s i
        @[simp]
        theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply_im {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (t : MeasureTheory.SignedMeasure α) (i : Set α) :
        ((s.toComplexMeasure t) i).im = t i

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

        Equations
        • s.toComplexMeasure t = { measureOf' := fun (i : Set α) => { re := s i, im := t i }, empty' := , not_measurable' := , m_iUnion' := }
        Instances For
          theorem MeasureTheory.SignedMeasure.toComplexMeasure_apply {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {t : MeasureTheory.SignedMeasure α} {i : Set α} :
          (s.toComplexMeasure t) i = { re := s i, im := t i }
          theorem MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α) :
          (MeasureTheory.ComplexMeasure.re c).toComplexMeasure (MeasureTheory.ComplexMeasure.im c) = c
          theorem MeasureTheory.SignedMeasure.re_toComplexMeasure {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (t : MeasureTheory.SignedMeasure α) :
          MeasureTheory.ComplexMeasure.re (s.toComplexMeasure t) = s
          theorem MeasureTheory.SignedMeasure.im_toComplexMeasure {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (t : MeasureTheory.SignedMeasure α) :
          MeasureTheory.ComplexMeasure.im (s.toComplexMeasure t) = t
          @[simp]
          theorem MeasureTheory.ComplexMeasure.equivSignedMeasure_apply {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α) :
          MeasureTheory.ComplexMeasure.equivSignedMeasure c = (MeasureTheory.ComplexMeasure.re c, MeasureTheory.ComplexMeasure.im c)
          @[simp]
          theorem MeasureTheory.ComplexMeasure.equivSignedMeasure_symm_apply {α : Type u_1} {m : MeasurableSpace α} :
          ∀ (x : MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α), MeasureTheory.ComplexMeasure.equivSignedMeasure.symm x = match x with | (s, t) => s.toComplexMeasure t

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply {α : Type u_1} {m : MeasurableSpace α} {R : Type u_2} [Semiring R] [Module R ] [ContinuousConstSMul R ] [ContinuousConstSMul R ] :
            ∀ (a : MeasureTheory.ComplexMeasure α), MeasureTheory.ComplexMeasure.equivSignedMeasureₗ a = MeasureTheory.ComplexMeasure.equivSignedMeasure.toFun a
            @[simp]
            theorem MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply {α : Type u_1} {m : MeasurableSpace α} {R : Type u_2} [Semiring R] [Module R ] [ContinuousConstSMul R ] [ContinuousConstSMul R ] :
            ∀ (a : MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α), MeasureTheory.ComplexMeasure.equivSignedMeasureₗ.symm a = MeasureTheory.ComplexMeasure.equivSignedMeasure.invFun a

            The complex measures form a linear isomorphism to the type of pairs of signed measures.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For