case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
f : StieltjesFunction
a b : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
rcases le_or_lt b a with (hab | hab)
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f) b - ↑f a)
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
simp only [hab, measure_empty, Ioo_eq_empty, not_lt]
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ofReal (leftLim (↑f) b - ↑f a) = 0
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f) b - ↑f a)
symm
no goals
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ofReal (leftLim (↑f) b - ↑f a) = 0
simp [ENNReal.ofReal_eq_zero, f.mono.leftLim_le hab]
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
have A : Disjoint (Ioo a b) {b} := by simp
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
have D : f b - f a = f b - leftLim f b + (leftLim f b - f a) := by abel
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : ↑↑(StieltjesFunction.measure f) (Ioc a b) = ofReal (↑f b - ↑f a)
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
have := f.measure_Ioc a b
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : ↑↑(StieltjesFunction.measure f) (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) = ofReal (↑f b - ↑f a)
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : ↑↑(StieltjesFunction.measure f) (Ioc a b) = ofReal (↑f b - ↑f a)
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
simp only [← Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton,
  measure_union A (measurableSet_singleton b), Icc_self] at this
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this :
  ofReal (↑f b - leftLim (↑f) b) + ↑↑(StieltjesFunction.measure f) (Ioo a b) =
    ofReal (↑f b - leftLim (↑f) b) + ofReal (leftLim (↑f) b - ↑f a)
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

case inr.hp
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this :
  ↑↑(StieltjesFunction.measure f) (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) =
    ofReal (↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a))
⊢ 0 ≤ ↑f b - leftLim (↑f) b

case inr.hq
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this :
  ↑↑(StieltjesFunction.measure f) (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) =
    ofReal (↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a))
⊢ 0 ≤ leftLim (↑f) b - ↑f a
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this : ↑↑(StieltjesFunction.measure f) (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) = ofReal (↑f b - ↑f a)
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
rw [D, ENNReal.ofReal_add, add_comm] at this
no goals
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ Disjoint (Ioo a b) {b}
simp
no goals
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
⊢ ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
abel
no goals
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this :
  ofReal (↑f b - leftLim (↑f) b) + ↑↑(StieltjesFunction.measure f) (Ioo a b) =
    ofReal (↑f b - leftLim (↑f) b) + ofReal (leftLim (↑f) b - ↑f a)
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
simpa only [ENNReal.add_right_inj ENNReal.ofReal_ne_top]
no goals
case inr.hp
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this :
  ↑↑(StieltjesFunction.measure f) (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) =
    ofReal (↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a))
⊢ 0 ≤ ↑f b - leftLim (↑f) b
simp only [f.mono.leftLim_le le_rfl, sub_nonneg]
no goals
case inr.hq
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint (Ioo a b) {b}
D : ↑f b - ↑f a = ↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a)
this :
  ↑↑(StieltjesFunction.measure f) (Ioo a b) + ofReal (↑f b - leftLim (↑f) b) =
    ofReal (↑f b - leftLim (↑f) b + (leftLim (↑f) b - ↑f a))
⊢ 0 ≤ leftLim (↑f) b - ↑f a
simp only [f.mono.le_leftLim hab, sub_nonneg]