[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
⊢ (fun i => { re := ↑s i, im := ↑t i }) ∅ = 0
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
⊢ { re := ↑s ∅, im := ↑t ∅ } = 0
[PROOFSTEP]
rw [s.empty, t.empty]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
⊢ { re := 0, im := 0 } = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
hi : ¬MeasurableSet i
⊢ (fun i => { re := ↑s i, im := ↑t i }) i = 0
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
hi : ¬MeasurableSet i
⊢ { re := ↑s i, im := ↑t i } = 0
[PROOFSTEP]
rw [s.not_measurable hi, t.not_measurable hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s t : SignedMeasure α
i : Set α
hi : ¬MeasurableSet i
⊢ { re := 0, im := 0 } = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
c d : ComplexMeasure α
⊢ Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ c + Equiv.toFun src✝ d
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
⊢ ∀ (r : R) (x : ComplexMeasure α),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (c d : ComplexMeasure α), Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ (c + d)) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' := (_ : ∀ (c d : ComplexMeasure α), Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ (c + d)) }
          x
[PROOFSTEP]
intro r c
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
r : R
c : ComplexMeasure α
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' := (_ : ∀ (c d : ComplexMeasure α), Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ (c + d)) }
      (r • c) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (c d : ComplexMeasure α), Equiv.toFun src✝ (c + d) = Equiv.toFun src✝ (c + d)) }
        c
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
r : R
c : ComplexMeasure α
⊢ (mapRange (r • c) (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
      mapRange (r • c) (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im) =
    (r • mapRange c (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
      r • mapRange c (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im)
[PROOFSTEP]
ext
[GOAL]
case h₁.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
r : R
c : ComplexMeasure α
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange (r • c) (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
            mapRange (r • c) (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im).fst
      i✝ =
    ↑(r • mapRange c (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
            r • mapRange c (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im).fst
      i✝
[PROOFSTEP]
simp [Complex.smul_re]
[GOAL]
case h₂.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
src✝ : ComplexMeasure α ≃ SignedMeasure α × SignedMeasure α := equivSignedMeasure
r : R
c : ComplexMeasure α
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange (r • c) (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
            mapRange (r • c) (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im).snd
      i✝ =
    ↑(r • mapRange c (LinearMap.toAddMonoidHom Complex.reLm) Complex.continuous_re,
            r • mapRange c (LinearMap.toAddMonoidHom Complex.imLm) Complex.continuous_im).snd
      i✝
[PROOFSTEP]
simp [Complex.smul_im]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ c ≪ᵥ μ ↔ ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ c ≪ᵥ μ → ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ → c ≪ᵥ μ
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
[PROOFSTEP]
constructor
[GOAL]
case mp.left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ ↑re c ≪ᵥ μ
[PROOFSTEP]
intro i hi
[GOAL]
case mp.left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑(↑re c) i = 0
[PROOFSTEP]
simp [h hi]
[GOAL]
case mp.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ ↑im c ≪ᵥ μ
[PROOFSTEP]
intro i hi
[GOAL]
case mp.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑(↑im c) i = 0
[PROOFSTEP]
simp [h hi]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
⊢ c ≪ᵥ μ
[PROOFSTEP]
intro i hi
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑c i = 0
[PROOFSTEP]
rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).im = 0
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).re = 0
[PROOFSTEP]
exacts [by simp, h.2 hi, h.1 hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ↑re c ≪ᵥ μ ∧ ↑im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0
[PROOFSTEP]
simp
