English
There is a natural equivalence between ComplexMeasure α and SignedMeasure α × SignedMeasure α given by c ↦ (re c, im c) with inverse (s,t) ↦ s.toComplexMeasure t.
Русский
Существует естественная эквиваленция между ComplexMeasure α и парой SignedMeasure α × SignedMeasure α: c ↦ (re c, im c) с обратной стрелкой (s,t) ↦ s.toComplexMeasure t.
LaTeX
$$equivSignedMeasure : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α$$
Lean4
/-- The complex measures form an equivalence to the type of pairs of signed measures. -/
@[simps]
def equivSignedMeasure : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α
where
toFun c := ⟨ComplexMeasure.re c, ComplexMeasure.im c⟩
invFun := fun ⟨s, t⟩ => s.toComplexMeasure t
left_inv c := c.toComplexMeasure_to_signedMeasure
right_inv := fun ⟨s, t⟩ => Prod.ext (s.re_toComplexMeasure t) (s.im_toComplexMeasure t)
