α : Type ?u.451381
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
⊢ IsFiniteMeasure ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
α : Type ?u.451381
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
⊢ IsFiniteMeasure ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
haveI := isFiniteMeasure_withDensity_ofReal hfi.2
no goals
α : Type ?u.451381
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
⊢ IsFiniteMeasure ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
infer_instance
α : Type ?u.451381
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ IsFiniteMeasure ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
α : Type ?u.451381
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
⊢ IsFiniteMeasure ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
no goals
α : Type ?u.451381
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ IsFiniteMeasure ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
infer_instance
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
⊢ toJordanDecomposition s =
    JordanDecomposition.mk ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
      ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
      (_ :
        ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
          (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
⊢ toJordanDecomposition s =
    JordanDecomposition.mk ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
      ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
      (_ :
        ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
          (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
haveI := isFiniteMeasure_withDensity_ofReal hfi.2
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ toJordanDecomposition s =
    JordanDecomposition.mk ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
      ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
      (_ :
        ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
          (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
⊢ toJordanDecomposition s =
    JordanDecomposition.mk ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
      ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
      (_ :
        ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
          (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ s =
    JordanDecomposition.toSignedMeasure
      (JordanDecomposition.mk ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
        ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
        (_ :
          ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
            (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)))
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ toJordanDecomposition s =
    JordanDecomposition.mk ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
      ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
      (_ :
        ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
          (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
refine' toJordanDecomposition_eq _
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ t + withDensityᵥ μ f =
    toSignedMeasure ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ s =
    JordanDecomposition.toSignedMeasure
      (JordanDecomposition.mk ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x))
        ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
        (_ :
          ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
            (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)))
simp_rw [JordanDecomposition.toSignedMeasure, hadd]
case h
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
i : Set α
⊢ MeasurableSet i →
    ↑(t + withDensityᵥ μ f) i =
      ↑(toSignedMeasure ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) -
            toSignedMeasure ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)))
        i
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ t + withDensityᵥ μ f =
    toSignedMeasure ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x))
ext i
case h
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ ↑(t + withDensityᵥ μ f) i =
    ↑(toSignedMeasure ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) -
          toSignedMeasure ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)))
      i
case h
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
i : Set α
⊢ MeasurableSet i →
    ↑(t + withDensityᵥ μ f) i =
      ↑(toSignedMeasure ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) -
            toSignedMeasure ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)))
        i
intro hi
no goals
case h
α : Type u_1
β : Type ?u.451384
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ ↑(t + withDensityᵥ μ f) i =
    ↑(toSignedMeasure ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) -
          toSignedMeasure ((toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)))
      i
rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, add_apply, add_apply, ENNReal.toReal_add,
    ENNReal.toReal_add, add_sub_add_comm, ← toSignedMeasure_apply_measurable hi,
    ← toSignedMeasure_apply_measurable hi, ← VectorMeasure.sub_apply,
    ← JordanDecomposition.toSignedMeasure, toSignedMeasure_toJordanDecomposition,
    VectorMeasure.add_apply, ← toSignedMeasure_apply_measurable hi,
    ← toSignedMeasure_apply_measurable hi,
    withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part hfi,
    VectorMeasure.sub_apply] <;>
  exact (measure_lt_top _ _).ne