[GOAL]
f g : StieltjesFunction
h : ∀ (x : ℝ), ↑f x = ↑g x
⊢ f = g
[PROOFSTEP]
exact (StieltjesFunction.mk.injEq ..).mpr (funext (by exact h))
[GOAL]
f g : StieltjesFunction
h : ∀ (x : ℝ), ↑f x = ↑g x
⊢ ∀ (x : ℝ), ↑f x = ↑g x
[PROOFSTEP]
exact h
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
⊢ rightLim (↑f) x = ↑f x
[PROOFSTEP]
rw [← f.mono.continuousWithinAt_Ioi_iff_rightLim_eq, continuousWithinAt_Ioi_iff_Ici]
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
⊢ ContinuousWithinAt (↑f) (Ici x) x
[PROOFSTEP]
exact f.right_continuous' x
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
⊢ ⨅ (r : ↑(Ioi x)), ↑f ↑r = ↑f x
[PROOFSTEP]
suffices Function.rightLim f x = ⨅ r : Ioi x, f r by rw [← this, f.rightLim_eq]
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
this : rightLim (↑f) x = ⨅ (r : ↑(Ioi x)), ↑f ↑r
⊢ ⨅ (r : ↑(Ioi x)), ↑f ↑r = ↑f x
[PROOFSTEP]
rw [← this, f.rightLim_eq]
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
⊢ rightLim (↑f) x = ⨅ (r : ↑(Ioi x)), ↑f ↑r
[PROOFSTEP]
rw [f.mono.rightLim_eq_sInf, sInf_image']
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
⊢ 𝓝[Ioi x] x ≠ ⊥
[PROOFSTEP]
rw [← neBot_iff]
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
⊢ NeBot (𝓝[Ioi x] x)
[PROOFSTEP]
infer_instance
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
⊢ ⨅ (r : { r' // x < ↑r' }), ↑f ↑↑r = ↑f x
[PROOFSTEP]
rw [← iInf_Ioi_eq f x]
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
⊢ ⨅ (r : { r' // x < ↑r' }), ↑f ↑↑r = ⨅ (r : ↑(Ioi x)), ↑f ↑r
[PROOFSTEP]
refine' (Real.iInf_Ioi_eq_iInf_rat_gt _ _ f.mono).symm
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
⊢ BddBelow (↑f '' Ioi x)
[PROOFSTEP]
refine' ⟨f x, fun y => _⟩
[GOAL]
f✝ f : StieltjesFunction
x y : ℝ
⊢ y ∈ ↑f '' Ioi x → ↑f x ≤ y
[PROOFSTEP]
rintro ⟨y, hy_mem, rfl⟩
[GOAL]
case intro.intro
f✝ f : StieltjesFunction
x y : ℝ
hy_mem : y ∈ Ioi x
⊢ ↑f x ≤ ↑f y
[PROOFSTEP]
exact f.mono (le_of_lt hy_mem)
[GOAL]
f✝ : StieltjesFunction
f : ℝ → ℝ
hf : Monotone f
⊢ ∀ (x : ℝ), ContinuousWithinAt (rightLim f) (Ici x) x
[PROOFSTEP]
intro x s hs
[GOAL]
f✝ : StieltjesFunction
f : ℝ → ℝ
hf : Monotone f
x : ℝ
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
⊢ s ∈ map (rightLim f) (𝓝[Ici x] x)
[PROOFSTEP]
obtain ⟨l, u, hlu, lus⟩ : ∃ l u : ℝ, rightLim f x ∈ Ioo l u ∧ Ioo l u ⊆ s := mem_nhds_iff_exists_Ioo_subset.1 hs
[GOAL]
case intro.intro.intro
f✝ : StieltjesFunction
f : ℝ → ℝ
hf : Monotone f
x : ℝ
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
⊢ s ∈ map (rightLim f) (𝓝[Ici x] x)
[PROOFSTEP]
obtain ⟨y, xy, h'y⟩ : ∃ (y : ℝ), x < y ∧ Ioc x y ⊆ f ⁻¹' Ioo l u :=
  mem_nhdsWithin_Ioi_iff_exists_Ioc_subset.1 (hf.tendsto_rightLim x (Ioo_mem_nhds hlu.1 hlu.2))
[GOAL]
case intro.intro.intro.intro.intro
f✝ : StieltjesFunction
f : ℝ → ℝ
hf : Monotone f
x : ℝ
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y : ℝ
xy : x < y
h'y : Ioc x y ⊆ f ⁻¹' Ioo l u
⊢ s ∈ map (rightLim f) (𝓝[Ici x] x)
[PROOFSTEP]
change ∀ᶠ y in 𝓝[≥] x, rightLim f y ∈ s
[GOAL]
case intro.intro.intro.intro.intro
f✝ : StieltjesFunction
f : ℝ → ℝ
hf : Monotone f
x : ℝ
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y : ℝ
xy : x < y
h'y : Ioc x y ⊆ f ⁻¹' Ioo l u
⊢ ∀ᶠ (y : ℝ) in 𝓝[Ici x] x, rightLim f y ∈ s
[PROOFSTEP]
filter_upwards [Ico_mem_nhdsWithin_Ici ⟨le_refl x, xy⟩] with z hz
[GOAL]
case h
f✝ : StieltjesFunction
f : ℝ → ℝ
hf : Monotone f
x : ℝ
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y : ℝ
xy : x < y
h'y : Ioc x y ⊆ f ⁻¹' Ioo l u
z : ℝ
hz : z ∈ Ico x y
⊢ rightLim f z ∈ s
[PROOFSTEP]
apply lus
[GOAL]
case h.a
f✝ : StieltjesFunction
f : ℝ → ℝ
hf : Monotone f
x : ℝ
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y : ℝ
xy : x < y
h'y : Ioc x y ⊆ f ⁻¹' Ioo l u
z : ℝ
hz : z ∈ Ico x y
⊢ rightLim f z ∈ Ioo l u
[PROOFSTEP]
refine' ⟨hlu.1.trans_le (hf.rightLim hz.1), _⟩
[GOAL]
case h.a
f✝ : StieltjesFunction
f : ℝ → ℝ
hf : Monotone f
x : ℝ
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y : ℝ
xy : x < y
h'y : Ioc x y ⊆ f ⁻¹' Ioo l u
z : ℝ
hz : z ∈ Ico x y
⊢ rightLim f z < u
[PROOFSTEP]
obtain ⟨a, za, ay⟩ : ∃ a : ℝ, z < a ∧ a < y := exists_between hz.2
[GOAL]
case h.a.intro.intro
f✝ : StieltjesFunction
f : ℝ → ℝ
hf : Monotone f
x : ℝ
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y : ℝ
xy : x < y
h'y : Ioc x y ⊆ f ⁻¹' Ioo l u
z : ℝ
hz : z ∈ Ico x y
a : ℝ
za : z < a
ay : a < y
⊢ rightLim f z < u
[PROOFSTEP]
calc
  rightLim f z ≤ f a := hf.rightLim_le za
  _ < u := (h'y ⟨hz.1.trans_lt za, ay.le⟩).2
[GOAL]
f✝ f : StieltjesFunction
⊢ Set.Countable {x | leftLim (↑f) x ≠ ↑f x}
[PROOFSTEP]
refine Countable.mono ?_ f.mono.countable_not_continuousAt
[GOAL]
f✝ f : StieltjesFunction
⊢ {x | leftLim (↑f) x ≠ ↑f x} ⊆ {x | ¬ContinuousAt (↑f) x}
[PROOFSTEP]
intro x hx h'x
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
hx : x ∈ {x | leftLim (↑f) x ≠ ↑f x}
h'x : ContinuousAt (↑f) x
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
f✝ f : StieltjesFunction
x : ℝ
hx : x ∈ {x | leftLim (↑f) x ≠ ↑f x}
h'x : ContinuousAt (↑f) x
⊢ leftLim (↑f) x = ↑f x
[PROOFSTEP]
exact tendsto_nhds_unique (f.mono.tendsto_leftLim x) (h'x.tendsto.mono_left nhdsWithin_le_nhds)
[GOAL]
f : StieltjesFunction
⊢ ⨅ (_ : ∅ ⊆ Ioc 0 0), ofReal (↑f 0 - ↑f 0) ≤ 0
[PROOFSTEP]
simp
[GOAL]
f : StieltjesFunction
a b : ℝ
⊢ length f (Ioc a b) = ofReal (↑f b - ↑f a)
[PROOFSTEP]
refine'
  le_antisymm (iInf_le_of_le a <| iInf₂_le b Subset.rfl)
    (le_iInf fun a' => le_iInf fun b' => le_iInf fun h => ENNReal.coe_le_coe.2 _)
[GOAL]
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
[PROOFSTEP]
cases' le_or_lt b a with ab ab
[GOAL]
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
[PROOFSTEP]
rw [Real.toNNReal_of_nonpos (sub_nonpos.2 (f.mono ab))]
[GOAL]
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ 0 ≤ Real.toNNReal (↑f b' - ↑f a')
[PROOFSTEP]
apply zero_le
[GOAL]
case inr
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
[PROOFSTEP]
cases' (Ioc_subset_Ioc_iff ab).1 h with h₁ h₂
[GOAL]
case inr.intro
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
h₁ : b ≤ b'
h₂ : a' ≤ a
⊢ Real.toNNReal (↑f b - ↑f a) ≤ Real.toNNReal (↑f b' - ↑f a')
[PROOFSTEP]
exact Real.toNNReal_le_toNNReal (sub_le_sub (f.mono h₁) (f.mono h₂))
[GOAL]
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
suffices
  ∀ (s : Finset ℕ) (b),
    Icc a b ⊆ (⋃ i ∈ (s : Set ℕ), Ioo (c i) (d i)) → (ofReal (f b - f a) : ℝ≥0∞) ≤ ∑ i in s, ofReal (f (d i) - f (c i))
  by
  rcases isCompact_Icc.elim_finite_subcover_image (fun (i : ℕ) (_ : i ∈ univ) => @isOpen_Ioo _ _ _ _ (c i) (d i))
      (by simpa using ss) with
    ⟨s, _, hf, hs⟩
  have e : ⋃ i ∈ (hf.toFinset : Set ℕ), Ioo (c i) (d i) = ⋃ i ∈ s, Ioo (c i) (d i) := by
    simp only [ext_iff, exists_prop, Finset.set_biUnion_coe, mem_iUnion, forall_const, iff_self_iff,
      Finite.mem_toFinset]
  rw [ENNReal.tsum_eq_iSup_sum]
  refine' le_trans _ (le_iSup _ hf.toFinset)
  exact this hf.toFinset _ (by simpa only [e])
[GOAL]
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
rcases isCompact_Icc.elim_finite_subcover_image (fun (i : ℕ) (_ : i ∈ univ) => @isOpen_Ioo _ _ _ _ (c i) (d i))
    (by simpa using ss) with
  ⟨s, _, hf, hs⟩
[GOAL]
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
⊢ Icc ?m.97098 ?m.97099 ⊆ ⋃ (i : ℕ) (_ : i ∈ univ), Ioo (c i) (d i)
[PROOFSTEP]
simpa using ss
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
have e : ⋃ i ∈ (hf.toFinset : Set ℕ), Ioo (c i) (d i) = ⋃ i ∈ s, Ioo (c i) (d i) := by
  simp only [ext_iff, exists_prop, Finset.set_biUnion_coe, mem_iUnion, forall_const, iff_self_iff, Finite.mem_toFinset]
[GOAL]
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
[PROOFSTEP]
simp only [ext_iff, exists_prop, Finset.set_biUnion_coe, mem_iUnion, forall_const, iff_self_iff, Finite.mem_toFinset]
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : ⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
rw [ENNReal.tsum_eq_iSup_sum]
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : ⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ⨆ (s : Finset ℕ), ∑ a in s, ofReal (↑f (d a) - ↑f (c a))
[PROOFSTEP]
refine' le_trans _ (le_iSup _ hf.toFinset)
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : ⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ a in Finite.toFinset hf, ofReal (↑f (d a) - ↑f (c a))
[PROOFSTEP]
exact this hf.toFinset _ (by simpa only [e])
[GOAL]
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : Set.Finite s
hs : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
e : ⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i) = ⋃ (i : ℕ) (_ : i ∈ s), Ioo (c i) (d i)
⊢ Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑(Finite.toFinset hf)), Ioo (c i) (d i)
[PROOFSTEP]
simpa only [e]
[GOAL]
f : StieltjesFunction
a b : ℝ
c d : ℕ → ℝ
ss : Icc a b ⊆ ⋃ (i : ℕ), Ioo (c i) (d i)
⊢ ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
clear ss b
[GOAL]
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
⊢ ∀ (s : Finset ℕ) (b : ℝ),
    Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
refine' fun s => Finset.strongInductionOn s fun s IH b cv => _
[GOAL]
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
cases' le_total b a with ab ab
[GOAL]
case inl
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : b ≤ a
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
rw [ENNReal.ofReal_eq_zero.2 (sub_nonpos.2 (f.mono ab))]
[GOAL]
case inl
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : b ≤ a
⊢ 0 ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
exact zero_le _
[GOAL]
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
have := cv ⟨ab, le_rfl⟩
[GOAL]
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
this : b ∈ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
simp only [Finset.mem_coe, gt_iff_lt, not_lt, ge_iff_le, mem_iUnion, mem_Ioo, exists_and_left, exists_prop] at this 
[GOAL]
case inr
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
this : ∃ i, c i < b ∧ i ∈ s ∧ b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
rcases this with ⟨i, cb, is, bd⟩
[GOAL]
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
cv : Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑s), Ioo (c i) (d i)
ab : a ≤ b
i : ℕ
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in s, ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
rw [← Finset.insert_erase is] at cv ⊢
[GOAL]
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ ⋃ (i_1 : ℕ) (_ : i_1 ∈ ↑(insert i (Finset.erase s i))), Ioo (c i_1) (d i_1)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in insert i (Finset.erase s i), ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
rw [Finset.coe_insert, biUnion_insert] at cv 
[GOAL]
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i in insert i (Finset.erase s i), ofReal (↑f (d i) - ↑f (c i))
[PROOFSTEP]
rw [Finset.sum_insert (Finset.not_mem_erase _ _)]
[GOAL]
case inr.intro.intro.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ∑ x in Finset.erase s i, ofReal (↑f (d x) - ↑f (c x))
[PROOFSTEP]
refine' le_trans _ (add_le_add_left (IH _ (Finset.erase_ssubset is) (c i) _) _)
[GOAL]
case inr.intro.intro.intro.refine'_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ofReal (↑f (c i) - ↑f a)
[PROOFSTEP]
refine' le_trans (ENNReal.ofReal_le_ofReal _) ENNReal.ofReal_add_le
[GOAL]
case inr.intro.intro.intro.refine'_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ↑f b - ↑f a ≤ ↑f (d i) - ↑f (c i) + (↑f (c i) - ↑f a)
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
case inr.intro.intro.intro.refine'_1
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ ↑f b - ↑f a ≤ ↑f (d i) - ↑f a
[PROOFSTEP]
exact sub_le_sub_right (f.mono bd.le) _
[GOAL]
case inr.intro.intro.intro.refine'_2
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
⊢ Icc a (c i) ⊆ ⋃ (i_1 : ℕ) (_ : i_1 ∈ ↑(Finset.erase s i)), Ioo (c i_1) (d i_1)
[PROOFSTEP]
rintro x ⟨h₁, h₂⟩
[GOAL]
case inr.intro.intro.intro.refine'_2.intro
f : StieltjesFunction
a : ℝ
c d : ℕ → ℝ
s✝ s : Finset ℕ
IH :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (b : ℝ),
        Icc a b ⊆ ⋃ (i : ℕ) (_ : i ∈ ↑t), Ioo (c i) (d i) →
          ofReal (↑f b - ↑f a) ≤ ∑ i in t, ofReal (↑f (d i) - ↑f (c i))
b : ℝ
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Ioo (c i) (d i) ∪ ⋃ (x : ℕ) (_ : x ∈ ↑(Finset.erase s i)), Ioo (c x) (d x)
cb : c i < b
is : i ∈ s
bd : b < d i
x : ℝ
h₁ : a ≤ x
h₂ : x ≤ c i
⊢ x ∈ ⋃ (i_1 : ℕ) (_ : i_1 ∈ ↑(Finset.erase s i)), Ioo (c i_1) (d i_1)
[PROOFSTEP]
refine' (cv ⟨h₁, le_trans h₂ (le_of_lt cb)⟩).resolve_left (mt And.left (not_lt_of_le h₂))
[GOAL]
f : StieltjesFunction
a b : ℝ
⊢ ↑(StieltjesFunction.outer f) (Ioc a b) = ofReal (↑f b - ↑f a)
[PROOFSTEP]
refine'
  le_antisymm
    (by
      rw [← f.length_Ioc]
      apply outer_le_length)
    (le_iInf₂ fun s hs => ENNReal.le_of_forall_pos_le_add fun ε εpos h => _)
[GOAL]
f : StieltjesFunction
a b : ℝ
⊢ ↑(StieltjesFunction.outer f) (Ioc a b) ≤ ofReal (↑f b - ↑f a)
[PROOFSTEP]
rw [← f.length_Ioc]
[GOAL]
f : StieltjesFunction
a b : ℝ
⊢ ↑(StieltjesFunction.outer f) (Ioc a b) ≤ length f (Ioc a b)
[PROOFSTEP]
apply outer_le_length
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), length f (s i) + ↑ε
[PROOFSTEP]
let δ := ε / 2
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), length f (s i) + ↑ε
[PROOFSTEP]
have δpos : 0 < (δ : ℝ≥0∞) := by simpa using εpos.ne'
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
⊢ 0 < ↑δ
[PROOFSTEP]
simpa using εpos.ne'
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), length f (s i) + ↑ε
[PROOFSTEP]
rcases ENNReal.exists_pos_sum_of_countable δpos.ne' ℕ with ⟨ε', ε'0, hε⟩
[GOAL]
case intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), length f (s i) + ↑ε
[PROOFSTEP]
obtain ⟨a', ha', aa'⟩ : ∃ a', f a' - f a < δ ∧ a < a' :=
  by
  have A : ContinuousWithinAt (fun r => f r - f a) (Ioi a) a :=
    by
    refine' ContinuousWithinAt.sub _ continuousWithinAt_const
    exact (f.right_continuous a).mono Ioi_subset_Ici_self
  have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
  exact (((tendsto_order.1 A).2 _ B).and self_mem_nhdsWithin).exists
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
⊢ ∃ a', ↑f a' - ↑f a < ↑δ ∧ a < a'
[PROOFSTEP]
have A : ContinuousWithinAt (fun r => f r - f a) (Ioi a) a :=
  by
  refine' ContinuousWithinAt.sub _ continuousWithinAt_const
  exact (f.right_continuous a).mono Ioi_subset_Ici_self
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
⊢ ContinuousWithinAt (fun r => ↑f r - ↑f a) (Ioi a) a
[PROOFSTEP]
refine' ContinuousWithinAt.sub _ continuousWithinAt_const
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
⊢ ContinuousWithinAt (fun r => ↑f r) (Ioi a) a
[PROOFSTEP]
exact (f.right_continuous a).mono Ioi_subset_Ici_self
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
A : ContinuousWithinAt (fun r => ↑f r - ↑f a) (Ioi a) a
⊢ ∃ a', ↑f a' - ↑f a < ↑δ ∧ a < a'
[PROOFSTEP]
have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
A : ContinuousWithinAt (fun r => ↑f r - ↑f a) (Ioi a) a
⊢ ↑f a - ↑f a < ↑δ
[PROOFSTEP]
rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
A : ContinuousWithinAt (fun r => ↑f r - ↑f a) (Ioi a) a
B : ↑f a - ↑f a < ↑δ
⊢ ∃ a', ↑f a' - ↑f a < ↑δ ∧ a < a'
[PROOFSTEP]
exact (((tendsto_order.1 A).2 _ B).and self_mem_nhdsWithin).exists
[GOAL]
case intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), length f (s i) + ↑ε
[PROOFSTEP]
have : ∀ i, ∃ p : ℝ × ℝ, s i ⊆ Ioo p.1 p.2 ∧ (ofReal (f p.2 - f p.1) : ℝ≥0∞) < f.length (s i) + ε' i :=
  by
  intro i
  have hl := ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_ne_zero.2 (ε'0 i).ne')
  conv at hl =>
    lhs
    rw [length]
  simp only [iInf_lt_iff, exists_prop] at hl 
  rcases hl with ⟨p, q', spq, hq'⟩
  have : ContinuousWithinAt (fun r => ofReal (f r - f p)) (Ioi q') q' :=
    by
    apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt
    refine' ContinuousWithinAt.sub _ continuousWithinAt_const
    exact (f.right_continuous q').mono Ioi_subset_Ici_self
  rcases(((tendsto_order.1 this).2 _ hq').and self_mem_nhdsWithin).exists with ⟨q, hq, q'q⟩
  exact ⟨⟨p, q⟩, spq.trans (Ioc_subset_Ioo_right q'q), hq⟩
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
⊢ ∀ (i : ℕ), ∃ p, s i ⊆ Ioo p.fst p.snd ∧ ofReal (↑f p.snd - ↑f p.fst) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
intro i
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
⊢ ∃ p, s i ⊆ Ioo p.fst p.snd ∧ ofReal (↑f p.snd - ↑f p.fst) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
have hl := ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_ne_zero.2 (ε'0 i).ne')
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
hl : length f (s i) < length f (s i) + ↑(ε' i)
⊢ ∃ p, s i ⊆ Ioo p.fst p.snd ∧ ofReal (↑f p.snd - ↑f p.fst) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
conv at hl =>
  lhs
  rw [length]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
hl : length f (s i) < length f (s i) + ↑(ε' i)
| length f (s i) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
  lhs
  rw [length]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
hl : length f (s i) < length f (s i) + ↑(ε' i)
| length f (s i) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
  lhs
  rw [length]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
hl : length f (s i) < length f (s i) + ↑(ε' i)
| length f (s i) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
lhs
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
hl : length f (s i) < length f (s i) + ↑(ε' i)
| length f (s i)
[PROOFSTEP]
rw [length]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
hl : ⨅ (a : ℝ) (b : ℝ) (_ : s i ⊆ Ioc a b), ofReal (↑f b - ↑f a) < length f (s i) + ↑(ε' i)
⊢ ∃ p, s i ⊆ Ioo p.fst p.snd ∧ ofReal (↑f p.snd - ↑f p.fst) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
simp only [iInf_lt_iff, exists_prop] at hl 
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
hl : ∃ i_1 i_2, s i ⊆ Ioc i_1 i_2 ∧ ofReal (↑f i_2 - ↑f i_1) < length f (s i) + ↑(ε' i)
⊢ ∃ p, s i ⊆ Ioo p.fst p.snd ∧ ofReal (↑f p.snd - ↑f p.fst) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
rcases hl with ⟨p, q', spq, hq'⟩
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < length f (s i) + ↑(ε' i)
⊢ ∃ p, s i ⊆ Ioo p.fst p.snd ∧ ofReal (↑f p.snd - ↑f p.fst) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
have : ContinuousWithinAt (fun r => ofReal (f r - f p)) (Ioi q') q' :=
  by
  apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt
  refine' ContinuousWithinAt.sub _ continuousWithinAt_const
  exact (f.right_continuous q').mono Ioi_subset_Ici_self
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < length f (s i) + ↑(ε' i)
⊢ ContinuousWithinAt (fun r => ofReal (↑f r - ↑f p)) (Ioi q') q'
[PROOFSTEP]
apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < length f (s i) + ↑(ε' i)
⊢ ContinuousWithinAt (fun r => ↑f r - ↑f p) (Ioi q') q'
[PROOFSTEP]
refine' ContinuousWithinAt.sub _ continuousWithinAt_const
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < length f (s i) + ↑(ε' i)
⊢ ContinuousWithinAt (fun r => ↑f r) (Ioi q') q'
[PROOFSTEP]
exact (f.right_continuous q').mono Ioi_subset_Ici_self
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < length f (s i) + ↑(ε' i)
this : ContinuousWithinAt (fun r => ofReal (↑f r - ↑f p)) (Ioi q') q'
⊢ ∃ p, s i ⊆ Ioo p.fst p.snd ∧ ofReal (↑f p.snd - ↑f p.fst) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
rcases(((tendsto_order.1 this).2 _ hq').and self_mem_nhdsWithin).exists with ⟨q, hq, q'q⟩
[GOAL]
case intro.intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
i : ℕ
p q' : ℝ
spq : s i ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < length f (s i) + ↑(ε' i)
this : ContinuousWithinAt (fun r => ofReal (↑f r - ↑f p)) (Ioi q') q'
q : ℝ
hq : ofReal (↑f q - ↑f p) < length f (s i) + ↑(ε' i)
q'q : q' < q
⊢ ∃ p, s i ⊆ Ioo p.fst p.snd ∧ ofReal (↑f p.snd - ↑f p.fst) < length f (s i) + ↑(ε' i)
[PROOFSTEP]
exact ⟨⟨p, q⟩, spq.trans (Ioc_subset_Ioo_right q'q), hq⟩
[GOAL]
case intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : ∀ (i : ℕ), ∃ p, s i ⊆ Ioo p.fst p.snd ∧ ofReal (↑f p.snd - ↑f p.fst) < length f (s i) + ↑(ε' i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), length f (s i) + ↑ε
[PROOFSTEP]
choose g hg using this
[GOAL]
case intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
g : ℕ → ℝ × ℝ
hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).fst (g i).snd ∧ ofReal (↑f (g i).snd - ↑f (g i).fst) < length f (s i) + ↑(ε' i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), length f (s i) + ↑ε
[PROOFSTEP]
have I_subset : Icc a' b ⊆ ⋃ i, Ioo (g i).1 (g i).2 :=
  calc
    Icc a' b ⊆ Ioc a b := fun x hx => ⟨aa'.trans_le hx.1, hx.2⟩
    _ ⊆ ⋃ i, s i := hs
    _ ⊆ ⋃ i, Ioo (g i).1 (g i).2 := iUnion_mono fun i => (hg i).1
[GOAL]
case intro.intro.intro.intro
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
g : ℕ → ℝ × ℝ
hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).fst (g i).snd ∧ ofReal (↑f (g i).snd - ↑f (g i).fst) < length f (s i) + ↑(ε' i)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Ioo (g i).fst (g i).snd
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), length f (s i) + ↑ε
[PROOFSTEP]
calc
  ofReal (f b - f a) = ofReal (f b - f a' + (f a' - f a)) := by rw [sub_add_sub_cancel]
  _ ≤ ofReal (f b - f a') + ofReal (f a' - f a) := ENNReal.ofReal_add_le
  _ ≤ ∑' i, ofReal (f (g i).2 - f (g i).1) + ofReal δ :=
    (add_le_add (f.length_subadditive_Icc_Ioo I_subset) (ENNReal.ofReal_le_ofReal ha'.le))
  _ ≤ ∑' i, (f.length (s i) + ε' i) + δ :=
    (add_le_add (ENNReal.tsum_le_tsum fun i => (hg i).2.le) (by simp only [ENNReal.ofReal_coe_nnreal, le_rfl]))
  _ = ∑' i, f.length (s i) + ∑' i, (ε' i : ℝ≥0∞) + δ := by rw [ENNReal.tsum_add]
  _ ≤ ∑' i, f.length (s i) + δ + δ := (add_le_add (add_le_add le_rfl hε.le) le_rfl)
  _ = ∑' i : ℕ, f.length (s i) + ε := by simp [add_assoc, ENNReal.add_halves]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
g : ℕ → ℝ × ℝ
hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).fst (g i).snd ∧ ofReal (↑f (g i).snd - ↑f (g i).fst) < length f (s i) + ↑(ε' i)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Ioo (g i).fst (g i).snd
⊢ ofReal (↑f b - ↑f a) = ofReal (↑f b - ↑f a' + (↑f a' - ↑f a))
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
g : ℕ → ℝ × ℝ
hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).fst (g i).snd ∧ ofReal (↑f (g i).snd - ↑f (g i).fst) < length f (s i) + ↑(ε' i)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Ioo (g i).fst (g i).snd
⊢ ofReal ↑δ ≤ ↑δ
[PROOFSTEP]
simp only [ENNReal.ofReal_coe_nnreal, le_rfl]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
g : ℕ → ℝ × ℝ
hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).fst (g i).snd ∧ ofReal (↑f (g i).snd - ↑f (g i).fst) < length f (s i) + ↑(ε' i)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Ioo (g i).fst (g i).snd
⊢ ∑' (i : ℕ), (length f (s i) + ↑(ε' i)) + ↑δ = ∑' (i : ℕ), length f (s i) + ∑' (i : ℕ), ↑(ε' i) + ↑δ
[PROOFSTEP]
rw [ENNReal.tsum_add]
[GOAL]
f : StieltjesFunction
a b : ℝ
s : ℕ → Set ℝ
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), length f (s i) < ⊤
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : ℝ
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
g : ℕ → ℝ × ℝ
hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).fst (g i).snd ∧ ofReal (↑f (g i).snd - ↑f (g i).fst) < length f (s i) + ↑(ε' i)
I_subset : Icc a' b ⊆ ⋃ (i : ℕ), Ioo (g i).fst (g i).snd
⊢ ∑' (i : ℕ), length f (s i) + ↑δ + ↑δ = ∑' (i : ℕ), length f (s i) + ↑ε
[PROOFSTEP]
simp [add_assoc, ENNReal.add_halves]
[GOAL]
f : StieltjesFunction
c : ℝ
⊢ MeasurableSet (Ioi c)
[PROOFSTEP]
refine OuterMeasure.ofFunction_caratheodory fun t => ?_
[GOAL]
f : StieltjesFunction
c : ℝ
t : Set ℝ
⊢ length f (t ∩ Ioi c) + length f (t \ Ioi c) ≤ length f t
[PROOFSTEP]
refine' le_iInf fun a => le_iInf fun b => le_iInf fun h => _
[GOAL]
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
⊢ length f (t ∩ Ioi c) + length f (t \ Ioi c) ≤ ofReal (↑f b - ↑f a)
[PROOFSTEP]
refine'
  le_trans (add_le_add (f.length_mono <| inter_subset_inter_left _ h) (f.length_mono <| diff_subset_diff_left h)) _
[GOAL]
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
[PROOFSTEP]
cases' le_total a c with hac hac
[GOAL]
case inl
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : a ≤ c
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
[PROOFSTEP]
cases' le_total b c with hbc hbc
[GOAL]
case inr
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : c ≤ a
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
[PROOFSTEP]
cases' le_total b c with hbc hbc
[GOAL]
case inl.inl
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : a ≤ c
hbc : b ≤ c
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
[PROOFSTEP]
simp only [Ioc_inter_Ioi, f.length_Ioc, hac, _root_.sup_eq_max, hbc, le_refl, Ioc_eq_empty, max_eq_right, min_eq_left,
  Ioc_diff_Ioi, f.length_empty, zero_add, not_lt]
[GOAL]
case inl.inr
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : a ≤ c
hbc : c ≤ b
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
[PROOFSTEP]
simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right, _root_.sup_eq_max, ← ENNReal.ofReal_add,
  f.mono hac, f.mono hbc, sub_nonneg, sub_add_sub_cancel, le_refl, max_eq_right]
[GOAL]
case inr.inl
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : c ≤ a
hbc : b ≤ c
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
[PROOFSTEP]
simp only [hbc, le_refl, Ioc_eq_empty, Ioc_inter_Ioi, min_eq_left, Ioc_diff_Ioi, f.length_empty, zero_add, or_true_iff,
  le_sup_iff, f.length_Ioc, not_lt]
[GOAL]
case inr.inr
f : StieltjesFunction
c : ℝ
t : Set ℝ
a b : ℝ
h : t ⊆ Ioc a b
hac : c ≤ a
hbc : c ≤ b
⊢ length f (Ioc a b ∩ Ioi c) + length f (Ioc a b \ Ioi c) ≤ ofReal (↑f b - ↑f a)
[PROOFSTEP]
simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right, _root_.sup_eq_max, le_refl, Ioc_eq_empty,
  add_zero, max_eq_left, f.length_empty, not_lt]
[GOAL]
f : StieltjesFunction
⊢ OuterMeasure.trim (StieltjesFunction.outer f) = StieltjesFunction.outer f
[PROOFSTEP]
refine' le_antisymm (fun s => _) (OuterMeasure.le_trim _)
[GOAL]
f : StieltjesFunction
s : Set ℝ
⊢ ↑(OuterMeasure.trim (StieltjesFunction.outer f)) s ≤ ↑(StieltjesFunction.outer f) s
[PROOFSTEP]
rw [OuterMeasure.trim_eq_iInf]
[GOAL]
f : StieltjesFunction
s : Set ℝ
⊢ ⨅ (t : Set ℝ) (_ : s ⊆ t) (_ : MeasurableSet t), ↑(StieltjesFunction.outer f) t ≤ ↑(StieltjesFunction.outer f) s
[PROOFSTEP]
refine' le_iInf fun t => le_iInf fun ht => ENNReal.le_of_forall_pos_le_add fun ε ε0 h => _
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
⊢ ⨅ (t : Set ℝ) (_ : s ⊆ t) (_ : MeasurableSet t), ↑(StieltjesFunction.outer f) t ≤ ∑' (i : ℕ), length f (t i) + ↑ε
[PROOFSTEP]
rcases ENNReal.exists_pos_sum_of_countable (ENNReal.coe_pos.2 ε0).ne' ℕ with ⟨ε', ε'0, hε⟩
[GOAL]
case intro.intro
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ ⨅ (t : Set ℝ) (_ : s ⊆ t) (_ : MeasurableSet t), ↑(StieltjesFunction.outer f) t ≤ ∑' (i : ℕ), length f (t i) + ↑ε
[PROOFSTEP]
refine' le_trans _ (add_le_add_left (le_of_lt hε) _)
[GOAL]
case intro.intro
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ ⨅ (t : Set ℝ) (_ : s ⊆ t) (_ : MeasurableSet t), ↑(StieltjesFunction.outer f) t ≤
    ∑' (i : ℕ), length f (t i) + ∑' (i : ℕ), ↑(ε' i)
[PROOFSTEP]
rw [← ENNReal.tsum_add]
[GOAL]
case intro.intro
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ ⨅ (t : Set ℝ) (_ : s ⊆ t) (_ : MeasurableSet t), ↑(StieltjesFunction.outer f) t ≤
    ∑' (a : ℕ), (length f (t a) + ↑(ε' a))
[PROOFSTEP]
choose g hg using
  show ∀ i, ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ f.outer s ≤ f.length (t i) + ofReal (ε' i)
    by
    intro i
    have hl := ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_pos.2 (ε'0 i)).ne'
    conv at hl =>
      lhs
      rw [length]
    simp only [iInf_lt_iff] at hl 
    rcases hl with ⟨a, b, h₁, h₂⟩
    rw [← f.outer_Ioc] at h₂ 
    exact ⟨_, h₁, measurableSet_Ioc, le_of_lt <| by simpa using h₂⟩
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ ∀ (i : ℕ), ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ ↑(StieltjesFunction.outer f) s ≤ length f (t i) + ofReal ↑(ε' i)
[PROOFSTEP]
intro i
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ ↑(StieltjesFunction.outer f) s ≤ length f (t i) + ofReal ↑(ε' i)
[PROOFSTEP]
have hl := ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_pos.2 (ε'0 i)).ne'
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hl : length f (t i) < length f (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ ↑(StieltjesFunction.outer f) s ≤ length f (t i) + ofReal ↑(ε' i)
[PROOFSTEP]
conv at hl =>
  lhs
  rw [length]
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hl : length f (t i) < length f (t i) + ↑(ε' i)
| length f (t i) < length f (t i) + ↑(ε' i)
[PROOFSTEP]
  lhs
  rw [length]
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hl : length f (t i) < length f (t i) + ↑(ε' i)
| length f (t i) < length f (t i) + ↑(ε' i)
[PROOFSTEP]
  lhs
  rw [length]
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hl : length f (t i) < length f (t i) + ↑(ε' i)
| length f (t i) < length f (t i) + ↑(ε' i)
[PROOFSTEP]
lhs
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hl : length f (t i) < length f (t i) + ↑(ε' i)
| length f (t i)
[PROOFSTEP]
rw [length]
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hl : ⨅ (a : ℝ) (b : ℝ) (_ : t i ⊆ Ioc a b), ofReal (↑f b - ↑f a) < length f (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ ↑(StieltjesFunction.outer f) s ≤ length f (t i) + ofReal ↑(ε' i)
[PROOFSTEP]
simp only [iInf_lt_iff] at hl 
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hl : ∃ i_1 i_2 i_3, ofReal (↑f i_2 - ↑f i_1) < length f (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ ↑(StieltjesFunction.outer f) s ≤ length f (t i) + ofReal ↑(ε' i)
[PROOFSTEP]
rcases hl with ⟨a, b, h₁, h₂⟩
[GOAL]
case intro.intro.intro
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
a b : ℝ
h₁ : t i ⊆ Ioc a b
h₂ : ofReal (↑f b - ↑f a) < length f (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ ↑(StieltjesFunction.outer f) s ≤ length f (t i) + ofReal ↑(ε' i)
[PROOFSTEP]
rw [← f.outer_Ioc] at h₂ 
[GOAL]
case intro.intro.intro
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
a b : ℝ
h₁ : t i ⊆ Ioc a b
h₂ : ↑(StieltjesFunction.outer f) (Ioc a b) < length f (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ ↑(StieltjesFunction.outer f) s ≤ length f (t i) + ofReal ↑(ε' i)
[PROOFSTEP]
exact ⟨_, h₁, measurableSet_Ioc, le_of_lt <| by simpa using h₂⟩
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
a b : ℝ
h₁ : t i ⊆ Ioc a b
h₂ : ↑(StieltjesFunction.outer f) (Ioc a b) < length f (t i) + ↑(ε' i)
⊢ ↑(StieltjesFunction.outer f) (Ioc a b) < length f (t i) + ofReal ↑(ε' i)
[PROOFSTEP]
simpa using h₂
[GOAL]
case intro.intro
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
g : ℕ → Set ℝ
hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ ↑(StieltjesFunction.outer f) (g i) ≤ length f (t i) + ofReal ↑(ε' i)
⊢ ⨅ (t : Set ℝ) (_ : s ⊆ t) (_ : MeasurableSet t), ↑(StieltjesFunction.outer f) t ≤
    ∑' (a : ℕ), (length f (t a) + ↑(ε' a))
[PROOFSTEP]
simp only [ofReal_coe_nnreal] at hg 
[GOAL]
case intro.intro
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
g : ℕ → Set ℝ
hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ ↑(StieltjesFunction.outer f) (g i) ≤ length f (t i) + ↑(ε' i)
⊢ ⨅ (t : Set ℝ) (_ : s ⊆ t) (_ : MeasurableSet t), ↑(StieltjesFunction.outer f) t ≤
    ∑' (a : ℕ), (length f (t a) + ↑(ε' a))
[PROOFSTEP]
apply iInf_le_of_le (iUnion g) _
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
g : ℕ → Set ℝ
hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ ↑(StieltjesFunction.outer f) (g i) ≤ length f (t i) + ↑(ε' i)
⊢ ⨅ (_ : s ⊆ iUnion g) (_ : MeasurableSet (iUnion g)), ↑(StieltjesFunction.outer f) (iUnion g) ≤
    ∑' (a : ℕ), (length f (t a) + ↑(ε' a))
[PROOFSTEP]
apply iInf_le_of_le (ht.trans <| iUnion_mono fun i => (hg i).1) _
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
g : ℕ → Set ℝ
hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ ↑(StieltjesFunction.outer f) (g i) ≤ length f (t i) + ↑(ε' i)
⊢ ⨅ (_ : MeasurableSet (iUnion g)), ↑(StieltjesFunction.outer f) (iUnion g) ≤ ∑' (a : ℕ), (length f (t a) + ↑(ε' a))
[PROOFSTEP]
apply iInf_le_of_le (MeasurableSet.iUnion fun i => (hg i).2.1) _
[GOAL]
f : StieltjesFunction
s : Set ℝ
t : ℕ → Set ℝ
ht : s ⊆ ⋃ (i : ℕ), t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), length f (t i) < ⊤
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
g : ℕ → Set ℝ
hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ ↑(StieltjesFunction.outer f) (g i) ≤ length f (t i) + ↑(ε' i)
⊢ ↑(StieltjesFunction.outer f) (iUnion g) ≤ ∑' (a : ℕ), (length f (t a) + ↑(ε' a))
[PROOFSTEP]
exact le_trans (f.outer.iUnion _) (ENNReal.tsum_le_tsum fun i => (hg i).2.2)
[GOAL]
f : StieltjesFunction
⊢ borel ℝ ≤ OuterMeasure.caratheodory (StieltjesFunction.outer f)
[PROOFSTEP]
rw [borel_eq_generateFrom_Ioi]
[GOAL]
f : StieltjesFunction
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ OuterMeasure.caratheodory (StieltjesFunction.outer f)
[PROOFSTEP]
refine' MeasurableSpace.generateFrom_le _
[GOAL]
f : StieltjesFunction
⊢ ∀ (t : Set ℝ), t ∈ range Ioi → MeasurableSet t
[PROOFSTEP]
simp (config := { contextual := true }) [f.measurableSet_Ioi]
[GOAL]
f : StieltjesFunction
a b : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Ioc a b) = ofReal (↑f b - ↑f a)
[PROOFSTEP]
rw [StieltjesFunction.measure]
[GOAL]
f : StieltjesFunction
a b : ℝ
⊢ ↑↑{ toOuterMeasure := StieltjesFunction.outer f,
            m_iUnion :=
              (_ :
                ∀ (_s : ℕ → Set ℝ),
                  (∀ (i : ℕ), MeasurableSet (_s i)) →
                    Pairwise (Disjoint on _s) →
                      ↑(StieltjesFunction.outer f) (⋃ (i : ℕ), _s i) = ∑' (i : ℕ), ↑(StieltjesFunction.outer f) (_s i)),
            trimmed := (_ : OuterMeasure.trim (StieltjesFunction.outer f) = StieltjesFunction.outer f) }
      (Ioc a b) =
    ofReal (↑f b - ↑f a)
[PROOFSTEP]
exact f.outer_Ioc a b
[GOAL]
f : StieltjesFunction
a : ℝ
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
[PROOFSTEP]
obtain ⟨u, u_mono, u_lt_a, u_lim⟩ : ∃ u : ℕ → ℝ, StrictMono u ∧ (∀ n : ℕ, u n < a) ∧ Tendsto u atTop (𝓝 a) :=
  exists_seq_strictMono_tendsto a
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
[PROOFSTEP]
have A : { a } = ⋂ n, Ioc (u n) a :=
  by
  refine' Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => _
  simp at hx 
  have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
  simp [le_antisymm this (hx 0).2]
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
⊢ {a} = ⋂ (n : ℕ), Ioc (u n) a
[PROOFSTEP]
refine' Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => _
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : x ∈ {a}
⊢ x ∈ ⋂ (n : ℕ), Ioc (u n) a
[PROOFSTEP]
simp [mem_singleton_iff.1 hx, u_lt_a]
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : x ∈ ⋂ (n : ℕ), Ioc (u n) a
⊢ x ∈ {a}
[PROOFSTEP]
simp at hx 
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
⊢ x ∈ {a}
[PROOFSTEP]
have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
x : ℝ
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
this : a ≤ x
⊢ x ∈ {a}
[PROOFSTEP]
simp [le_antisymm this (hx 0).2]
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
[PROOFSTEP]
have L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure { a })) :=
  by
  rw [A]
  refine' tendsto_measure_iInter (fun n => measurableSet_Ioc) (fun m n hmn => _) _
  · exact Ioc_subset_Ioc (u_mono.monotone hmn) le_rfl
  · exact ⟨0, by simpa only [measure_Ioc] using ENNReal.ofReal_ne_top⟩
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
[PROOFSTEP]
rw [A]
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop
    (𝓝 (↑↑(StieltjesFunction.measure f) (⋂ (n : ℕ), Ioc (u n) a)))
[PROOFSTEP]
refine' tendsto_measure_iInter (fun n => measurableSet_Ioc) (fun m n hmn => _) _
[GOAL]
case refine'_1
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
m n : ℕ
hmn : m ≤ n
⊢ Ioc (u n) a ≤ Ioc (u m) a
[PROOFSTEP]
exact Ioc_subset_Ioc (u_mono.monotone hmn) le_rfl
[GOAL]
case refine'_2
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ ∃ i, ↑↑(StieltjesFunction.measure f) (Ioc (u i) a) ≠ ⊤
[PROOFSTEP]
exact ⟨0, by simpa only [measure_Ioc] using ENNReal.ofReal_ne_top⟩
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
⊢ ↑↑(StieltjesFunction.measure f) (Ioc (u 0) a) ≠ ⊤
[PROOFSTEP]
simpa only [measure_Ioc] using ENNReal.ofReal_ne_top
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
[PROOFSTEP]
have L2 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (ofReal (f a - leftLim f a))) :=
  by
  simp only [measure_Ioc]
  have : Tendsto (fun n => f (u n)) atTop (𝓝 (leftLim f a)) :=
    by
    apply (f.mono.tendsto_leftLim a).comp
    exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim (eventually_of_forall fun n => u_lt_a n)
  exact ENNReal.continuous_ofReal.continuousAt.tendsto.comp (tendsto_const_nhds.sub this)
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
[PROOFSTEP]
simp only [measure_Ioc]
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => ofReal (↑f a - ↑f (u n))) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
[PROOFSTEP]
have : Tendsto (fun n => f (u n)) atTop (𝓝 (leftLim f a)) :=
  by
  apply (f.mono.tendsto_leftLim a).comp
  exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim (eventually_of_forall fun n => u_lt_a n)
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => ↑f (u n)) atTop (𝓝 (leftLim (↑f) a))
[PROOFSTEP]
apply (f.mono.tendsto_leftLim a).comp
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
⊢ Tendsto (fun n => u n) atTop (𝓝[Iio a] a)
[PROOFSTEP]
exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim (eventually_of_forall fun n => u_lt_a n)
[GOAL]
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
this : Tendsto (fun n => ↑f (u n)) atTop (𝓝 (leftLim (↑f) a))
⊢ Tendsto (fun n => ofReal (↑f a - ↑f (u n))) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
[PROOFSTEP]
exact ENNReal.continuous_ofReal.continuousAt.tendsto.comp (tendsto_const_nhds.sub this)
[GOAL]
case intro.intro.intro
f : StieltjesFunction
a : ℝ
u : ℕ → ℝ
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n < a
u_lim : Tendsto u atTop (𝓝 a)
A : {a} = ⋂ (n : ℕ), Ioc (u n) a
L1 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (↑↑(StieltjesFunction.measure f) {a}))
L2 : Tendsto (fun n => ↑↑(StieltjesFunction.measure f) (Ioc (u n) a)) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))
⊢ ↑↑(StieltjesFunction.measure f) {a} = ofReal (↑f a - leftLim (↑f) a)
[PROOFSTEP]
exact tendsto_nhds_unique L1 L2
[GOAL]
f : StieltjesFunction
a b : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
[PROOFSTEP]
rcases le_or_lt a b with (hab | hab)
[GOAL]
case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
[PROOFSTEP]
have A : Disjoint { a } (Ioc a b) := by simp
[GOAL]
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
⊢ Disjoint {a} (Ioc a b)
[PROOFSTEP]
simp
[GOAL]
case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
A : Disjoint {a} (Ioc a b)
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
[PROOFSTEP]
simp [← Icc_union_Ioc_eq_Icc le_rfl hab, -singleton_union, ← ENNReal.ofReal_add, f.mono.leftLim_le,
  measure_union A measurableSet_Ioc, f.mono hab]
[GOAL]
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ ↑↑(StieltjesFunction.measure f) (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
[PROOFSTEP]
simp only [hab, measure_empty, Icc_eq_empty, not_le]
[GOAL]
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ 0 = ofReal (↑f b - leftLim (↑f) a)
[PROOFSTEP]
symm
[GOAL]
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ ofReal (↑f b - leftLim (↑f) a) = 0
[PROOFSTEP]
simp [ENNReal.ofReal_eq_zero, f.mono.le_leftLim hab]
[GOAL]
f : StieltjesFunction
a b : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
[PROOFSTEP]
rcases le_or_lt b a with (hab | hab)
[GOAL]
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
[PROOFSTEP]
simp only [hab, measure_empty, Ioo_eq_empty, not_lt]
[GOAL]
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f) b - ↑f a)
[PROOFSTEP]
symm
[GOAL]
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ofReal (leftLim (↑f) b - ↑f a) = 0
[PROOFSTEP]
simp [ENNReal.ofReal_eq_zero, f.mono.leftLim_le hab]
[GOAL]
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ ↑↑(StieltjesFunction.measure f) (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
[PROOFSTEP]
have A : Disjoint (Ioo a b) { b } := by simp
[GOAL]
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ Disjoint (Ioo a b) {b}
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
have D : f b - f a = f b - leftLim f b + (leftLim f b - f a) := by abel
[GOAL]
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)
[PROOFSTEP]
abel
[GOAL]
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)
[PROOFSTEP]
abel
[GOAL]
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)
[PROOFSTEP]
have := f.measure_Ioc a b
[GOAL]
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)
[PROOFSTEP]
simp only [← Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton, measure_union A (measurableSet_singleton b),
  Icc_self] at this 
[GOAL]
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)
[PROOFSTEP]
rw [D, ENNReal.ofReal_add, add_comm] at this 
[GOAL]
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)
[PROOFSTEP]
simpa only [ENNReal.add_right_inj ENNReal.ofReal_ne_top]
[GOAL]
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
[PROOFSTEP]
simp only [f.mono.leftLim_le le_rfl, sub_nonneg]
[GOAL]
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
[PROOFSTEP]
simp only [f.mono.le_leftLim hab, sub_nonneg]
[GOAL]
f : StieltjesFunction
a b : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)
[PROOFSTEP]
rcases le_or_lt b a with (hab | hab)
[GOAL]
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ↑↑(StieltjesFunction.measure f) (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)
[PROOFSTEP]
simp only [hab, measure_empty, Ico_eq_empty, not_lt]
[GOAL]
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f) b - leftLim (↑f) a)
[PROOFSTEP]
symm
[GOAL]
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ofReal (leftLim (↑f) b - leftLim (↑f) a) = 0
[PROOFSTEP]
simp [ENNReal.ofReal_eq_zero, f.mono.leftLim hab]
[GOAL]
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ ↑↑(StieltjesFunction.measure f) (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)
[PROOFSTEP]
have A : Disjoint { a } (Ioo a b) := by simp
[GOAL]
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ Disjoint {a} (Ioo a b)
[PROOFSTEP]
simp
[GOAL]
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint {a} (Ioo a b)
⊢ ↑↑(StieltjesFunction.measure f) (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)
[PROOFSTEP]
simp [← Icc_union_Ioo_eq_Ico le_rfl hab, -singleton_union, hab.ne, f.mono.leftLim_le, measure_union A measurableSet_Ioo,
  f.mono.le_leftLim hab, ← ENNReal.ofReal_add]
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Iic x) = ofReal (↑f x - l)
[PROOFSTEP]
refine' tendsto_nhds_unique (tendsto_measure_Ioc_atBot _ _) _
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ↑↑(StieltjesFunction.measure f) (Ioc x_1 x)) atBot (𝓝 (ofReal (↑f x - l)))
[PROOFSTEP]
simp_rw [measure_Ioc]
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (↑f x - ↑f x_1)) atBot (𝓝 (ofReal (↑f x - l)))
[PROOFSTEP]
exact ENNReal.tendsto_ofReal (Tendsto.const_sub _ hf)
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Ici x) = ofReal (l - leftLim (↑f) x)
[PROOFSTEP]
refine' tendsto_nhds_unique (tendsto_measure_Ico_atTop _ _) _
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ↑↑(StieltjesFunction.measure f) (Ico x x_1)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))
[PROOFSTEP]
simp_rw [measure_Ico]
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (leftLim (↑f) x_1 - leftLim (↑f) x)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))
[PROOFSTEP]
refine' ENNReal.tendsto_ofReal (Tendsto.sub_const _ _)
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x => leftLim (↑f) x) atTop (𝓝 l)
[PROOFSTEP]
have h_le1 : ∀ x, f (x - 1) ≤ leftLim f x := fun x => Monotone.le_leftLim f.mono (sub_one_lt x)
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
⊢ Tendsto (fun x => leftLim (↑f) x) atTop (𝓝 l)
[PROOFSTEP]
have h_le2 : ∀ x, leftLim f x ≤ f x := fun x => Monotone.leftLim_le f.mono le_rfl
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (fun x => leftLim (↑f) x) atTop (𝓝 l)
[PROOFSTEP]
refine' tendsto_of_tendsto_of_tendsto_of_le_of_le (hf.comp _) hf h_le1 h_le2
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (fun i => i - 1) atTop atTop
[PROOFSTEP]
rw [tendsto_atTop_atTop]
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a - 1
[PROOFSTEP]
exact fun y => ⟨y + 1, fun z hyz => by rwa [le_sub_iff_add_le]⟩
[GOAL]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
y z : ℝ
hyz : y + 1 ≤ z
⊢ y ≤ z - 1
[PROOFSTEP]
rwa [le_sub_iff_add_le]
[GOAL]
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ ↑↑(StieltjesFunction.measure f) univ = ofReal (u - l)
[PROOFSTEP]
refine' tendsto_nhds_unique (tendsto_measure_Iic_atTop _) _
[GOAL]
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => ↑↑(StieltjesFunction.measure f) (Iic x)) atTop (𝓝 (ofReal (u - l)))
[PROOFSTEP]
simp_rw [measure_Iic f hfl]
[GOAL]
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => ofReal (↑f x - l)) atTop (𝓝 (ofReal (u - l)))
[PROOFSTEP]
exact ENNReal.tendsto_ofReal (Tendsto.sub_const hfu _)
[GOAL]
f : StieltjesFunction
x : ℝ
⊢ x - 1 < x
[PROOFSTEP]
linarith
[GOAL]
f : StieltjesFunction
x : ℝ
⊢ x < x + 1
[PROOFSTEP]
linarith
[GOAL]
f : StieltjesFunction
x : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Ioo (x - 1) (x + 1)) < ⊤
[PROOFSTEP]
simp
[GOAL]
f g : StieltjesFunction
l : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case h
f g : StieltjesFunction
l : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
⊢ ↑f x = ↑g x
[PROOFSTEP]
have hf := measure_Iic f hfl x
[GOAL]
case h
f g : StieltjesFunction
l : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ↑↑(StieltjesFunction.measure f) (Iic x) = ofReal (↑f x - l)
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [hfg, measure_Iic g hgl x, ENNReal.ofReal_eq_ofReal_iff, eq_comm] at hf 
[GOAL]
case h
f g : StieltjesFunction
l : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ↑f x - l = ↑g x - l
⊢ ↑f x = ↑g x
[PROOFSTEP]
simpa using hf
[GOAL]
case h.hp
f g : StieltjesFunction
l : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ 0 ≤ ↑g x - l
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
case h.hp
f g : StieltjesFunction
l : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ l ≤ ↑g x
[PROOFSTEP]
exact Monotone.le_of_tendsto g.mono hgl x
[GOAL]
case h.hq
f g : StieltjesFunction
l : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ 0 ≤ ↑f x - l
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
case h.hq
f g : StieltjesFunction
l : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : ℝ
hf : ofReal (↑g x - l) = ofReal (↑f x - l)
⊢ l ≤ ↑f x
[PROOFSTEP]
exact Monotone.le_of_tendsto f.mono hfl x
[GOAL]
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case h
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
⊢ ↑f x = ↑g x
[PROOFSTEP]
cases le_total x y with
| inl hxy =>
  have hf := measure_Ioc f x y
  rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf 
  · simpa using hf
  · rw [sub_nonneg]
    exact g.mono hxy
  · rw [sub_nonneg]
    exact f.mono hxy
| inr hxy =>
  have hf := measure_Ioc f y x
  rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf 
  · simpa using hf
  · rw [sub_nonneg]
    exact g.mono hxy
  · rw [sub_nonneg]
    exact f.mono hxy
[GOAL]
case h
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
x✝ : x ≤ y ∨ y ≤ x
⊢ ↑f x = ↑g x
[PROOFSTEP]
cases le_total x y with
| inl hxy =>
  have hf := measure_Ioc f x y
  rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf 
  · simpa using hf
  · rw [sub_nonneg]
    exact g.mono hxy
  · rw [sub_nonneg]
    exact f.mono hxy
| inr hxy =>
  have hf := measure_Ioc f y x
  rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf 
  · simpa using hf
  · rw [sub_nonneg]
    exact g.mono hxy
  · rw [sub_nonneg]
    exact f.mono hxy
[GOAL]
case h.inl
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
⊢ ↑f x = ↑g x
[PROOFSTEP]

| inl hxy =>
  have hf := measure_Ioc f x y
  rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf 
  · simpa using hf
  · rw [sub_nonneg]
    exact g.mono hxy
  · rw [sub_nonneg]
    exact f.mono hxy
[GOAL]
case h.inl
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
⊢ ↑f x = ↑g x
[PROOFSTEP]
have hf := measure_Ioc f x y
[GOAL]
case h.inl
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ↑↑(StieltjesFunction.measure f) (Ioc x y) = ofReal (↑f y - ↑f x)
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf 
[GOAL]
case h.inl
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ↑g y - ↑f x = ↑g y - ↑g x
⊢ ↑f x = ↑g x
[PROOFSTEP]
simpa using hf
[GOAL]
case h.inl.hp
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ 0 ≤ ↑g y - ↑g x
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
case h.inl.hp
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ ↑g x ≤ ↑g y
[PROOFSTEP]
exact g.mono hxy
[GOAL]
case h.inl.hq
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ 0 ≤ ↑f y - ↑f x
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
case h.inl.hq
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ ↑f x ≤ ↑f y
[PROOFSTEP]
exact f.mono hxy
[GOAL]
case h.inr
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
⊢ ↑f x = ↑g x
[PROOFSTEP]

| inr hxy =>
  have hf := measure_Ioc f y x
  rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf 
  · simpa using hf
  · rw [sub_nonneg]
    exact g.mono hxy
  · rw [sub_nonneg]
    exact f.mono hxy
[GOAL]
case h.inr
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
⊢ ↑f x = ↑g x
[PROOFSTEP]
have hf := measure_Ioc f y x
[GOAL]
case h.inr
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ↑↑(StieltjesFunction.measure f) (Ioc y x) = ofReal (↑f x - ↑f y)
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf 
[GOAL]
case h.inr
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ↑f x - ↑g y = ↑g x - ↑g y
⊢ ↑f x = ↑g x
[PROOFSTEP]
simpa using hf
[GOAL]
case h.inr.hp
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ 0 ≤ ↑g x - ↑g y
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
case h.inr.hp
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ ↑g y ≤ ↑g x
[PROOFSTEP]
exact g.mono hxy
[GOAL]
case h.inr.hq
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ 0 ≤ ↑f x - ↑f y
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
case h.inr.hq
f g : StieltjesFunction
y : ℝ
hfg : StieltjesFunction.measure f = StieltjesFunction.measure g
hy : ↑f y = ↑g y
x : ℝ
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ ↑f y ≤ ↑f x
[PROOFSTEP]
exact f.mono hxy
