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)) + ↑ε
f : StieltjesFunction
a b : ℝ
⊢ ↑(StieltjesFunction.outer f) (Ioc a b) = ofReal (↑f b - ↑f a)
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 => _)
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)) + ↑ε
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)) + ↑ε
let δ := ε / 2
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)) + ↑ε
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)) + ↑ε
have δpos : 0 < (δ : ℝ≥0∞) := by simpa using εpos.ne'
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)) + ↑ε
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)) + ↑ε
rcases ENNReal.exists_pos_sum_of_countable δpos.ne' ℕ with ⟨ε', ε'0, hε⟩
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)) + ↑ε
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)) + ↑ε
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
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)) + ↑ε
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)) + ↑ε
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⟩
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)) + ↑ε
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)) + ↑ε
choose g hg using this
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)) + ↑ε
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)) + ↑ε
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
no goals
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)) + ↑ε
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]
f : StieltjesFunction
a b : ℝ
⊢ ↑(StieltjesFunction.outer f) (Ioc a b) ≤ length f (Ioc a b)
f : StieltjesFunction
a b : ℝ
⊢ ↑(StieltjesFunction.outer f) (Ioc a b) ≤ ofReal (↑f b - ↑f a)
rw [← f.length_Ioc]
no goals
f : StieltjesFunction
a b : ℝ
⊢ ↑(StieltjesFunction.outer f) (Ioc a b) ≤ length f (Ioc a b)
apply outer_le_length
no goals
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 < ↑δ
simpa using εpos.ne'
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'
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'
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
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'
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'
have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
no goals
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'
exact (((tendsto_order.1 A).2 _ B).and self_mem_nhdsWithin).exists
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
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
refine' ContinuousWithinAt.sub _ continuousWithinAt_const
no goals
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
exact (f.right_continuous a).mono Ioi_subset_Ici_self
no goals
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 < ↑δ
rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
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)
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)
intro i
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)
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)
have hl :=
  ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_ne_zero.2 (ε'0 i).ne')
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)
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)
conv at hl =>
  lhs
  rw [length]
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)
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)
simp only [iInf_lt_iff, exists_prop] at hl
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)
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)
rcases hl with ⟨p, q', spq, hq'⟩
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)
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)
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
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)
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)
rcases (((tendsto_order.1 this).2 _ hq').and self_mem_nhdsWithin).exists with ⟨q, hq, q'q⟩
no goals
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)
exact ⟨⟨p, q⟩, spq.trans (Ioc_subset_Ioo_right q'q), hq⟩
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'
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'
apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt
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'
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'
refine' ContinuousWithinAt.sub _ continuousWithinAt_const
no goals
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'
exact (f.right_continuous q').mono Ioi_subset_Ici_self
no goals
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))
rw [sub_add_sub_cancel]
no goals
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 ↑δ ≤ ↑δ
simp only [ENNReal.ofReal_coe_nnreal, le_rfl]
no goals
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)) + ↑δ
rw [ENNReal.tsum_add]
no goals
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)) + ↑ε
simp [add_assoc, ENNReal.add_halves]