[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
[PROOFSTEP]
have L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1) :=
  by
  have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) :=
    by
    apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
    exact ((tendsto_id.sub_const x).const_mul c).const_add 1
  simp only [_root_.sub_self, add_zero, mul_zero] at this 
  apply Tendsto.congr' (Eventually.filter_mono hl _) this
  filter_upwards [self_mem_nhdsWithin] with y hy
  field_simp [sub_ne_zero.2 hy]
  ring
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
[PROOFSTEP]
have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) :=
  by
  apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
  exact ((tendsto_id.sub_const x).const_mul c).const_add 1
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))
[PROOFSTEP]
apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y => 1 + c * (y - x)) (𝓝 x) (𝓝 (1 + c * (x - x)))
[PROOFSTEP]
exact ((tendsto_id.sub_const x).const_mul c).const_add 1
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))
⊢ Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
[PROOFSTEP]
simp only [_root_.sub_self, add_zero, mul_zero] at this 
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
⊢ Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
[PROOFSTEP]
apply Tendsto.congr' (Eventually.filter_mono hl _) this
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[{x}ᶜ] x, 1 + c * (x_1 - x) = (x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with y hy
[GOAL]
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
y : ℝ
hy : y ∈ {x}ᶜ
⊢ 1 + c * (y - x) = (y + c * (y - x) ^ 2 - x) / (y - x)
[PROOFSTEP]
field_simp [sub_ne_zero.2 hy]
[GOAL]
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
y : ℝ
hy : y ∈ {x}ᶜ
⊢ (1 + c * (y - x)) * (y - x) = y + c * (y - x) ^ 2 - x
[PROOFSTEP]
ring
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
[PROOFSTEP]
have Z := (hf.comp h').mul L
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 (a * 1))
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
[PROOFSTEP]
rw [mul_one] at Z 
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
[PROOFSTEP]
apply Tendsto.congr' _ Z
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 *
        ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) =ᶠ[l]
    fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)
[PROOFSTEP]
have : ∀ᶠ y in l, y + c * (y - x) ^ 2 ≠ x := by apply Tendsto.mono_right h' hl self_mem_nhdsWithin
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x
[PROOFSTEP]
apply Tendsto.mono_right h' hl self_mem_nhdsWithin
[GOAL]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
this : ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x
⊢ (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 *
        ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) =ᶠ[l]
    fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)
[PROOFSTEP]
filter_upwards [this] with y hy
[GOAL]
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
this : ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x
y : ℝ
hy : y + c * (y - x) ^ 2 ≠ x
⊢ ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) y * ((y + c * (y - x) ^ 2 - x) / (y - x)) =
    (f (y + c * (y - x) ^ 2) - d) / (y - x)
[PROOFSTEP]
field_simp [sub_ne_zero.2 hy]
[GOAL]
f : StieltjesFunction
⊢ ∀ᵐ (x : ℝ), HasDerivAt (↑f) (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)) x
[PROOFSTEP]
filter_upwards [VitaliFamily.ae_tendsto_rnDeriv (vitaliFamily (volume : Measure ℝ) 1) f.measure,
  rnDeriv_lt_top f.measure volume, f.countable_leftLim_ne.ae_not_mem volume] with x hx h'x h''x
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
⊢ HasDerivAt (↑f) (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)) x
[PROOFSTEP]
have L1 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (rnDeriv f.measure volume x).toReal) :=
  by
  apply Tendsto.congr' _ ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_right x)))
  filter_upwards [self_mem_nhdsWithin]
  rintro y (hxy : x < y)
  simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc, Classical.not_not.1 h''x]
  rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal]
  exact div_nonneg (sub_nonneg.2 (f.mono hxy.le)) (sub_pos.2 hxy).le
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
⊢ Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
[PROOFSTEP]
apply Tendsto.congr' _ ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_right x)))
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
⊢ (ENNReal.toReal ∘ (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) ∘ fun y => Icc x y) =ᶠ[𝓝[Ioi x] x]
    fun y => (↑f y - ↑f x) / (y - x)
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
⊢ ∀ (a : ℝ),
    a ∈ Ioi x →
      (ENNReal.toReal ∘ (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) ∘ fun y => Icc x y) a =
        (↑f a - ↑f x) / (a - x)
[PROOFSTEP]
rintro y (hxy : x < y)
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
y : ℝ
hxy : x < y
⊢ (ENNReal.toReal ∘ (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) ∘ fun y => Icc x y) y =
    (↑f y - ↑f x) / (y - x)
[PROOFSTEP]
simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc, Classical.not_not.1 h''x]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
y : ℝ
hxy : x < y
⊢ ENNReal.toReal (ENNReal.ofReal (↑f y - ↑f x) / ENNReal.ofReal (y - x)) = (↑f y - ↑f x) / (y - x)
[PROOFSTEP]
rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
y : ℝ
hxy : x < y
⊢ 0 ≤ (↑f y - ↑f x) / (y - x)
[PROOFSTEP]
exact div_nonneg (sub_nonneg.2 (f.mono hxy.le)) (sub_pos.2 hxy).le
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ HasDerivAt (↑f) (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)) x
[PROOFSTEP]
have L2 : Tendsto (fun y => (leftLim f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (rnDeriv f.measure volume x).toReal) :=
  by
  apply Tendsto.congr' _ ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_left x)))
  filter_upwards [self_mem_nhdsWithin]
  rintro y (hxy : y < x)
  simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc]
  rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal, ← neg_neg (y - x), div_neg, neg_div', neg_sub,
    neg_sub]
  exact div_nonneg (sub_nonneg.2 (f.mono.leftLim_le hxy.le)) (sub_pos.2 hxy).le
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
[PROOFSTEP]
apply Tendsto.congr' _ ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_left x)))
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ (ENNReal.toReal ∘ (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) ∘ fun y => Icc y x) =ᶠ[𝓝[Iio x] x]
    fun y => (leftLim (↑f) y - ↑f x) / (y - x)
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ ∀ (a : ℝ),
    a ∈ Iio x →
      (ENNReal.toReal ∘ (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) ∘ fun y => Icc y x) a =
        (leftLim (↑f) a - ↑f x) / (a - x)
[PROOFSTEP]
rintro y (hxy : y < x)
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hxy : y < x
⊢ (ENNReal.toReal ∘ (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) ∘ fun y => Icc y x) y =
    (leftLim (↑f) y - ↑f x) / (y - x)
[PROOFSTEP]
simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hxy : y < x
⊢ ENNReal.toReal (ENNReal.ofReal (↑f x - leftLim (↑f) y) / ENNReal.ofReal (x - y)) = (leftLim (↑f) y - ↑f x) / (y - x)
[PROOFSTEP]
rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal, ← neg_neg (y - x), div_neg, neg_div', neg_sub,
  neg_sub]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hxy : y < x
⊢ 0 ≤ (↑f x - leftLim (↑f) y) / (x - y)
[PROOFSTEP]
exact div_nonneg (sub_nonneg.2 (f.mono.leftLim_le hxy.le)) (sub_pos.2 hxy).le
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ HasDerivAt (↑f) (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)) x
[PROOFSTEP]
have L3 :
  Tendsto (fun y => (leftLim f (y + 1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv f.measure volume x).toReal) :=
  by
  apply tendsto_apply_add_mul_sq_div_sub (nhds_left'_le_nhds_ne x) L2
  apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
  · apply Tendsto.mono_left _ nhdsWithin_le_nhds
    have : Tendsto (fun y : ℝ => y + ↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + ↑1 * (x - x) ^ 2)) :=
      tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul ↑1)
    simpa using this
  · have : Ioo (x - 1) x ∈ 𝓝[<] x := by apply Ioo_mem_nhdsWithin_Iio; exact ⟨by linarith, le_refl _⟩
    filter_upwards [this]
    rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
    rw [mem_Iio]
    norm_num;
    nlinarith
      -- Deduce the correct limit on the left, by sandwiching.
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
[PROOFSTEP]
apply tendsto_apply_add_mul_sq_div_sub (nhds_left'_le_nhds_ne x) L2
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ Tendsto (fun y => y + ↑1 * (y - x) ^ 2) (𝓝[Iio x] x) (𝓝[Iio x] x)
[PROOFSTEP]
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
[GOAL]
case h1
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ Tendsto (fun y => y + ↑1 * (y - x) ^ 2) (𝓝[Iio x] x) (𝓝 x)
[PROOFSTEP]
apply Tendsto.mono_left _ nhdsWithin_le_nhds
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ Tendsto (fun y => y + ↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)
[PROOFSTEP]
have : Tendsto (fun y : ℝ => y + ↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + ↑1 * (x - x) ^ 2)) :=
  tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul ↑1)
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
this : Tendsto (fun y => y + 1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + 1 * (x - x) ^ 2))
⊢ Tendsto (fun y => y + ↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)
[PROOFSTEP]
simpa using this
[GOAL]
case h2
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[Iio x] x, x_1 + ↑1 * (x_1 - x) ^ 2 ∈ Iio x
[PROOFSTEP]
have : Ioo (x - 1) x ∈ 𝓝[<] x := by apply Ioo_mem_nhdsWithin_Iio; exact ⟨by linarith, le_refl _⟩
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ Ioo (x - 1) x ∈ 𝓝[Iio x] x
[PROOFSTEP]
apply Ioo_mem_nhdsWithin_Iio
[GOAL]
case H
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ x ∈ Ioc (x - 1) x
[PROOFSTEP]
exact ⟨by linarith, le_refl _⟩
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ x - 1 < x
[PROOFSTEP]
linarith
[GOAL]
case h2
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[Iio x] x, x_1 + ↑1 * (x_1 - x) ^ 2 ∈ Iio x
[PROOFSTEP]
filter_upwards [this]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
⊢ ∀ (a : ℝ), a ∈ Ioo (x - 1) x → a + ↑1 * (a - x) ^ 2 ∈ Iio x
[PROOFSTEP]
rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
[GOAL]
case h.intro
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
y : ℝ
hy : x - 1 < y
h'y : y < x
⊢ y + ↑1 * (y - x) ^ 2 ∈ Iio x
[PROOFSTEP]
rw [mem_Iio]
[GOAL]
case h.intro
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
y : ℝ
hy : x - 1 < y
h'y : y < x
⊢ y + ↑1 * (y - x) ^ 2 < x
[PROOFSTEP]
norm_num
[GOAL]
case h.intro
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
y : ℝ
hy : x - 1 < y
h'y : y < x
⊢ y + (y - x) ^ 2 < x
[PROOFSTEP]
nlinarith
  -- Deduce the correct limit on the left, by sandwiching.
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ HasDerivAt (↑f) (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)) x
[PROOFSTEP]
have L4 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (rnDeriv f.measure volume x).toReal) :=
  by
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' L3 L2
  · filter_upwards [self_mem_nhdsWithin]
    rintro y (hy : y < x)
    refine' div_le_div_of_nonpos_of_le (by linarith) ((sub_le_sub_iff_right _).2 _)
    apply f.mono.le_leftLim
    have : ↑0 < (x - y) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
    norm_num; linarith
  · filter_upwards [self_mem_nhdsWithin]
    rintro y (hy : y < x)
    refine' div_le_div_of_nonpos_of_le (by linarith) _
    simpa only [sub_le_sub_iff_right] using
      f.mono.leftLim_le
        (le_refl y)
          -- prove the result by splitting into left and right limits.
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
[PROOFSTEP]
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' L3 L2
[GOAL]
case hgf
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ ∀ᶠ (b : ℝ) in 𝓝[Iio x] x, (leftLim (↑f) (b + ↑1 * (b - x) ^ 2) - ↑f x) / (b - x) ≤ (↑f b - ↑f x) / (b - x)
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ ∀ (a : ℝ), a ∈ Iio x → (leftLim (↑f) (a + ↑1 * (a - x) ^ 2) - ↑f x) / (a - x) ≤ (↑f a - ↑f x) / (a - x)
[PROOFSTEP]
rintro y (hy : y < x)
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hy : y < x
⊢ (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x) ≤ (↑f y - ↑f x) / (y - x)
[PROOFSTEP]
refine' div_le_div_of_nonpos_of_le (by linarith) ((sub_le_sub_iff_right _).2 _)
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hy : y < x
⊢ y - x ≤ 0
[PROOFSTEP]
linarith
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hy : y < x
⊢ ↑f y ≤ leftLim (↑f) (y + ↑1 * (y - x) ^ 2)
[PROOFSTEP]
apply f.mono.le_leftLim
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hy : y < x
⊢ y < y + ↑1 * (y - x) ^ 2
[PROOFSTEP]
have : ↑0 < (x - y) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hy : y < x
this : 0 < (x - y) ^ 2
⊢ y < y + ↑1 * (y - x) ^ 2
[PROOFSTEP]
norm_num
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hy : y < x
this : 0 < (x - y) ^ 2
⊢ 0 < (y - x) ^ 2
[PROOFSTEP]
linarith
[GOAL]
case hfh
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ ∀ᶠ (b : ℝ) in 𝓝[Iio x] x, (↑f b - ↑f x) / (b - x) ≤ (leftLim (↑f) b - ↑f x) / (b - x)
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ ∀ (a : ℝ), a ∈ Iio x → (↑f a - ↑f x) / (a - x) ≤ (leftLim (↑f) a - ↑f x) / (a - x)
[PROOFSTEP]
rintro y (hy : y < x)
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hy : y < x
⊢ (↑f y - ↑f x) / (y - x) ≤ (leftLim (↑f) y - ↑f x) / (y - x)
[PROOFSTEP]
refine' div_le_div_of_nonpos_of_le (by linarith) _
[GOAL]
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hy : y < x
⊢ y - x ≤ 0
[PROOFSTEP]
linarith
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
y : ℝ
hy : y < x
⊢ leftLim (↑f) y - ↑f x ≤ ↑f y - ↑f x
[PROOFSTEP]
simpa only [sub_le_sub_iff_right] using
  f.mono.leftLim_le
    (le_refl y)
      -- prove the result by splitting into left and right limits.
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L4 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ HasDerivAt (↑f) (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)) x
[PROOFSTEP]
rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, ← nhds_left'_sup_nhds_right', tendsto_sup]
[GOAL]
case h
f : StieltjesFunction
x : ℝ
hx :
  Tendsto (fun a => ↑↑(StieltjesFunction.measure f) a / ↑↑volume a) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
    (𝓝 (rnDeriv (StieltjesFunction.measure f) volume x))
h'x : rnDeriv (StieltjesFunction.measure f) volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L2 :
  Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L3 :
  Tendsto (fun y => (leftLim (↑f) (y + ↑1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
L4 :
  Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
⊢ Tendsto (fun b => (↑f b - ↑f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x))) ∧
    Tendsto (fun b => (↑f b - ↑f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)))
[PROOFSTEP]
exact ⟨L4, L1⟩
[GOAL]
f : ℝ → ℝ
hf : Monotone f
⊢ ∀ᵐ (x : ℝ), HasDerivAt f (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
[PROOFSTEP]
filter_upwards [hf.stieltjesFunction.ae_hasDerivAt, hf.countable_not_continuousAt.ae_not_mem volume] with x hx h'x
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑(stieltjesFunction hf))
    (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
h'x : ¬¬ContinuousAt f x
⊢ HasDerivAt f (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
[PROOFSTEP]
have A : hf.stieltjesFunction x = f x :=
  by
  rw [Classical.not_not, hf.continuousAt_iff_leftLim_eq_rightLim] at h'x 
  apply le_antisymm _ (hf.le_rightLim (le_refl _))
  rw [← h'x]
  exact hf.leftLim_le (le_refl _)
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑(stieltjesFunction hf))
    (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
h'x : ¬¬ContinuousAt f x
⊢ ↑(stieltjesFunction hf) x = f x
[PROOFSTEP]
rw [Classical.not_not, hf.continuousAt_iff_leftLim_eq_rightLim] at h'x 
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑(stieltjesFunction hf))
    (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
h'x : leftLim f x = rightLim f x
⊢ ↑(stieltjesFunction hf) x = f x
[PROOFSTEP]
apply le_antisymm _ (hf.le_rightLim (le_refl _))
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑(stieltjesFunction hf))
    (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
h'x : leftLim f x = rightLim f x
⊢ rightLim f x ≤ f x
[PROOFSTEP]
rw [← h'x]
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑(stieltjesFunction hf))
    (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
h'x : leftLim f x = rightLim f x
⊢ leftLim f x ≤ f x
[PROOFSTEP]
exact hf.leftLim_le (le_refl _)
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  HasDerivAt (↑(stieltjesFunction hf))
    (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ HasDerivAt f (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
[PROOFSTEP]
rw [hasDerivAt_iff_tendsto_slope, (nhds_left'_sup_nhds_right' x).symm, tendsto_sup, slope_fun_def_field, A] at hx 
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ HasDerivAt f (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
[PROOFSTEP]
have L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
  -- limit of a helper function, with a small shift compared to `g`
  have :
    Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
      (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) :=
    by
    apply tendsto_apply_add_mul_sq_div_sub (nhds_right'_le_nhds_ne x) hx.2
    apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
    · apply Tendsto.mono_left _ nhdsWithin_le_nhds
      have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
        tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
      simpa using this
    · have : Ioo x (x + 1) ∈ 𝓝[>] x := by apply Ioo_mem_nhdsWithin_Ioi; exact ⟨le_refl _, by linarith⟩
      filter_upwards [this]
      rintro y ⟨hy : x < y, h'y : y < x + 1⟩
      rw [mem_Ioi]
      norm_num;
      nlinarith
        -- apply the sandwiching argument, with the helper function and `g`
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
  · filter_upwards [self_mem_nhdsWithin]
    rintro y (hy : x < y)
    have : ↑0 < (y - x) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
    apply div_le_div_of_le_of_nonneg _ (sub_pos.2 hy).le
    exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by norm_num; linarith))
  · filter_upwards [self_mem_nhdsWithin]
    rintro y (hy : x < y)
    apply div_le_div_of_le_of_nonneg _ (sub_pos.2 hy).le
    exact
      (sub_le_sub_iff_right _).2
        (hf.le_rightLim (le_refl y))
          -- prove differentiability on the left, by sandwiching with values of `g`
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
[PROOFSTEP]
have :
  Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) :=
  by
  apply tendsto_apply_add_mul_sq_div_sub (nhds_right'_le_nhds_ne x) hx.2
  apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
  · apply Tendsto.mono_left _ nhdsWithin_le_nhds
    have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
      tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
    simpa using this
  · have : Ioo x (x + 1) ∈ 𝓝[>] x := by apply Ioo_mem_nhdsWithin_Ioi; exact ⟨le_refl _, by linarith⟩
    filter_upwards [this]
    rintro y ⟨hy : x < y, h'y : y < x + 1⟩
    rw [mem_Ioi]
    norm_num;
    nlinarith
      -- apply the sandwiching argument, with the helper function and `g`
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
[PROOFSTEP]
apply tendsto_apply_add_mul_sq_div_sub (nhds_right'_le_nhds_ne x) hx.2
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ Tendsto (fun y => y + -↑1 * (y - x) ^ 2) (𝓝[Ioi x] x) (𝓝[Ioi x] x)
[PROOFSTEP]
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
[GOAL]
case h1
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ Tendsto (fun y => y + -↑1 * (y - x) ^ 2) (𝓝[Ioi x] x) (𝓝 x)
[PROOFSTEP]
apply Tendsto.mono_left _ nhdsWithin_le_nhds
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ Tendsto (fun y => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)
[PROOFSTEP]
have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
  tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this : Tendsto (fun y => y + -1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -1 * (x - x) ^ 2))
⊢ Tendsto (fun y => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)
[PROOFSTEP]
simpa using this
[GOAL]
case h2
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[Ioi x] x, x_1 + -↑1 * (x_1 - x) ^ 2 ∈ Ioi x
[PROOFSTEP]
have : Ioo x (x + 1) ∈ 𝓝[>] x := by apply Ioo_mem_nhdsWithin_Ioi; exact ⟨le_refl _, by linarith⟩
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ Ioo x (x + 1) ∈ 𝓝[Ioi x] x
[PROOFSTEP]
apply Ioo_mem_nhdsWithin_Ioi
[GOAL]
case H
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ x ∈ Ico x (x + 1)
[PROOFSTEP]
exact ⟨le_refl _, by linarith⟩
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
⊢ x < x + 1
[PROOFSTEP]
linarith
[GOAL]
case h2
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this : Ioo x (x + 1) ∈ 𝓝[Ioi x] x
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[Ioi x] x, x_1 + -↑1 * (x_1 - x) ^ 2 ∈ Ioi x
[PROOFSTEP]
filter_upwards [this]
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this : Ioo x (x + 1) ∈ 𝓝[Ioi x] x
⊢ ∀ (a : ℝ), a ∈ Ioo x (x + 1) → a + -↑1 * (a - x) ^ 2 ∈ Ioi x
[PROOFSTEP]
rintro y ⟨hy : x < y, h'y : y < x + 1⟩
[GOAL]
case h.intro
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this : Ioo x (x + 1) ∈ 𝓝[Ioi x] x
y : ℝ
hy : x < y
h'y : y < x + 1
⊢ y + -↑1 * (y - x) ^ 2 ∈ Ioi x
[PROOFSTEP]
rw [mem_Ioi]
[GOAL]
case h.intro
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this : Ioo x (x + 1) ∈ 𝓝[Ioi x] x
y : ℝ
hy : x < y
h'y : y < x + 1
⊢ x < y + -↑1 * (y - x) ^ 2
[PROOFSTEP]
norm_num
[GOAL]
case h.intro
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this : Ioo x (x + 1) ∈ 𝓝[Ioi x] x
y : ℝ
hy : x < y
h'y : y < x + 1
⊢ x + (y - x) ^ 2 < y
[PROOFSTEP]
nlinarith
  -- apply the sandwiching argument, with the helper function and `g`
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
[PROOFSTEP]
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
[GOAL]
case hgf
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioi x] x, (↑(stieltjesFunction hf) (b + -↑1 * (b - x) ^ 2) - f x) / (b - x) ≤ (f b - f x) / (b - x)
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin]
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ ∀ (a : ℝ), a ∈ Ioi x → (↑(stieltjesFunction hf) (a + -↑1 * (a - x) ^ 2) - f x) / (a - x) ≤ (f a - f x) / (a - x)
[PROOFSTEP]
rintro y (hy : x < y)
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : x < y
⊢ (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)
[PROOFSTEP]
have : ↑0 < (y - x) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this✝ :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : x < y
this : 0 < (y - x) ^ 2
⊢ (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)
[PROOFSTEP]
apply div_le_div_of_le_of_nonneg _ (sub_pos.2 hy).le
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this✝ :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : x < y
this : 0 < (y - x) ^ 2
⊢ ↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x ≤ f y - f x
[PROOFSTEP]
exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by norm_num; linarith))
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this✝ :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : x < y
this : 0 < (y - x) ^ 2
⊢ y + -↑1 * (y - x) ^ 2 < y
[PROOFSTEP]
norm_num
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this✝ :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : x < y
this : 0 < (y - x) ^ 2
⊢ 0 < (y - x) ^ 2
[PROOFSTEP]
linarith
[GOAL]
case hfh
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioi x] x, (f b - f x) / (b - x) ≤ (↑(stieltjesFunction hf) b - f x) / (b - x)
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin]
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ ∀ (a : ℝ), a ∈ Ioi x → (f a - f x) / (a - x) ≤ (↑(stieltjesFunction hf) a - f x) / (a - x)
[PROOFSTEP]
rintro y (hy : x < y)
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : x < y
⊢ (f y - f x) / (y - x) ≤ (↑(stieltjesFunction hf) y - f x) / (y - x)
[PROOFSTEP]
apply div_le_div_of_le_of_nonneg _ (sub_pos.2 hy).le
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : x < y
⊢ f y - f x ≤ ↑(stieltjesFunction hf) y - f x
[PROOFSTEP]
exact
  (sub_le_sub_iff_right _).2
    (hf.le_rightLim (le_refl y))
      -- prove differentiability on the left, by sandwiching with values of `g`
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ HasDerivAt f (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
[PROOFSTEP]
have L2 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[<] x) (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
  -- limit of a helper function, with a small shift compared to `g`
  have :
    Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
      (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) :=
    by
    apply tendsto_apply_add_mul_sq_div_sub (nhds_left'_le_nhds_ne x) hx.1
    apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
    · apply Tendsto.mono_left _ nhdsWithin_le_nhds
      have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
        tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
      simpa using this
    · have : Ioo (x - 1) x ∈ 𝓝[<] x := by apply Ioo_mem_nhdsWithin_Iio; exact ⟨by linarith, le_refl _⟩
      filter_upwards [this]
      rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
      rw [mem_Iio]
      norm_num;
      nlinarith
        -- apply the sandwiching argument, with `g` and the helper function
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hx.1 this
  · filter_upwards [self_mem_nhdsWithin]
    rintro y (hy : y < x)
    apply div_le_div_of_nonpos_of_le (sub_neg.2 hy).le
    exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl _))
  · filter_upwards [self_mem_nhdsWithin]
    rintro y (hy : y < x)
    have : ↑0 < (y - x) ^ 2 := sq_pos_of_neg (sub_neg.2 hy)
    apply div_le_div_of_nonpos_of_le (sub_neg.2 hy).le
    exact
      (sub_le_sub_iff_right _).2
        (hf.rightLim_le (by norm_num; linarith))
          -- conclude global differentiability
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
[PROOFSTEP]
have :
  Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) :=
  by
  apply tendsto_apply_add_mul_sq_div_sub (nhds_left'_le_nhds_ne x) hx.1
  apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
  · apply Tendsto.mono_left _ nhdsWithin_le_nhds
    have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
      tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
    simpa using this
  · have : Ioo (x - 1) x ∈ 𝓝[<] x := by apply Ioo_mem_nhdsWithin_Iio; exact ⟨by linarith, le_refl _⟩
    filter_upwards [this]
    rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
    rw [mem_Iio]
    norm_num;
    nlinarith
      -- apply the sandwiching argument, with `g` and the helper function
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
[PROOFSTEP]
apply tendsto_apply_add_mul_sq_div_sub (nhds_left'_le_nhds_ne x) hx.1
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ Tendsto (fun y => y + -↑1 * (y - x) ^ 2) (𝓝[Iio x] x) (𝓝[Iio x] x)
[PROOFSTEP]
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
[GOAL]
case h1
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ Tendsto (fun y => y + -↑1 * (y - x) ^ 2) (𝓝[Iio x] x) (𝓝 x)
[PROOFSTEP]
apply Tendsto.mono_left _ nhdsWithin_le_nhds
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ Tendsto (fun y => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)
[PROOFSTEP]
have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
  tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this : Tendsto (fun y => y + -1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -1 * (x - x) ^ 2))
⊢ Tendsto (fun y => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)
[PROOFSTEP]
simpa using this
[GOAL]
case h2
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[Iio x] x, x_1 + -↑1 * (x_1 - x) ^ 2 ∈ Iio x
[PROOFSTEP]
have : Ioo (x - 1) x ∈ 𝓝[<] x := by apply Ioo_mem_nhdsWithin_Iio; exact ⟨by linarith, le_refl _⟩
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ Ioo (x - 1) x ∈ 𝓝[Iio x] x
[PROOFSTEP]
apply Ioo_mem_nhdsWithin_Iio
[GOAL]
case H
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ x ∈ Ioc (x - 1) x
[PROOFSTEP]
exact ⟨by linarith, le_refl _⟩
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ x - 1 < x
[PROOFSTEP]
linarith
[GOAL]
case h2
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[Iio x] x, x_1 + -↑1 * (x_1 - x) ^ 2 ∈ Iio x
[PROOFSTEP]
filter_upwards [this]
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
⊢ ∀ (a : ℝ), a ∈ Ioo (x - 1) x → a + -↑1 * (a - x) ^ 2 ∈ Iio x
[PROOFSTEP]
rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
[GOAL]
case h.intro
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
y : ℝ
hy : x - 1 < y
h'y : y < x
⊢ y + -↑1 * (y - x) ^ 2 ∈ Iio x
[PROOFSTEP]
rw [mem_Iio]
[GOAL]
case h.intro
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
y : ℝ
hy : x - 1 < y
h'y : y < x
⊢ y + -↑1 * (y - x) ^ 2 < x
[PROOFSTEP]
norm_num
[GOAL]
case h.intro
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this : Ioo (x - 1) x ∈ 𝓝[Iio x] x
y : ℝ
hy : x - 1 < y
h'y : y < x
⊢ y < x + (y - x) ^ 2
[PROOFSTEP]
nlinarith
  -- apply the sandwiching argument, with `g` and the helper function
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
[PROOFSTEP]
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hx.1 this
[GOAL]
case hgf
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ ∀ᶠ (b : ℝ) in 𝓝[Iio x] x, (↑(stieltjesFunction hf) b - f x) / (b - x) ≤ (f b - f x) / (b - x)
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin]
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ ∀ (a : ℝ), a ∈ Iio x → (↑(stieltjesFunction hf) a - f x) / (a - x) ≤ (f a - f x) / (a - x)
[PROOFSTEP]
rintro y (hy : y < x)
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : y < x
⊢ (↑(stieltjesFunction hf) y - f x) / (y - x) ≤ (f y - f x) / (y - x)
[PROOFSTEP]
apply div_le_div_of_nonpos_of_le (sub_neg.2 hy).le
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : y < x
⊢ f y - f x ≤ ↑(stieltjesFunction hf) y - f x
[PROOFSTEP]
exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl _))
[GOAL]
case hfh
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ ∀ᶠ (b : ℝ) in 𝓝[Iio x] x, (f b - f x) / (b - x) ≤ (↑(stieltjesFunction hf) (b + -↑1 * (b - x) ^ 2) - f x) / (b - x)
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin]
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ ∀ (a : ℝ), a ∈ Iio x → (f a - f x) / (a - x) ≤ (↑(stieltjesFunction hf) (a + -↑1 * (a - x) ^ 2) - f x) / (a - x)
[PROOFSTEP]
rintro y (hy : y < x)
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : y < x
⊢ (f y - f x) / (y - x) ≤ (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)
[PROOFSTEP]
have : ↑0 < (y - x) ^ 2 := sq_pos_of_neg (sub_neg.2 hy)
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this✝ :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : y < x
this : 0 < (y - x) ^ 2
⊢ (f y - f x) / (y - x) ≤ (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)
[PROOFSTEP]
apply div_le_div_of_nonpos_of_le (sub_neg.2 hy).le
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this✝ :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : y < x
this : 0 < (y - x) ^ 2
⊢ ↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x ≤ f y - f x
[PROOFSTEP]
exact
  (sub_le_sub_iff_right _).2
    (hf.rightLim_le (by norm_num; linarith))
      -- conclude global differentiability
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this✝ :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : y < x
this : 0 < (y - x) ^ 2
⊢ y + -↑1 * (y - x) ^ 2 < y
[PROOFSTEP]
norm_num
[GOAL]
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
this✝ :
  Tendsto (fun y => (↑(stieltjesFunction hf) (y + -↑1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
y : ℝ
hy : y < x
this : 0 < (y - x) ^ 2
⊢ 0 < (y - x) ^ 2
[PROOFSTEP]
linarith
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
L2 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ HasDerivAt f (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
[PROOFSTEP]
rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, (nhds_left'_sup_nhds_right' x).symm, tendsto_sup]
[GOAL]
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (↑(stieltjesFunction hf) b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
h'x : ¬¬ContinuousAt f x
A : ↑(stieltjesFunction hf) x = f x
L1 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Ioi x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
L2 :
  Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[Iio x] x)
    (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
⊢ Tendsto (fun b => (f b - f x) / (b - x)) (𝓝[Iio x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x))) ∧
    Tendsto (fun b => (f b - f x) / (b - x)) (𝓝[Ioi x] x)
      (𝓝 (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)))
[PROOFSTEP]
exact ⟨L2, L1⟩
[GOAL]
f : ℝ → ℝ
hf : Monotone f
⊢ ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
[PROOFSTEP]
filter_upwards [hf.ae_hasDerivAt] with x hx using hx.differentiableAt
[GOAL]
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
[PROOFSTEP]
apply ae_of_mem_of_ae_of_mem_inter_Ioo
[GOAL]
case h
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
⊢ ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
[PROOFSTEP]
intro a b as bs _
[GOAL]
case h
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
⊢ ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
[PROOFSTEP]
obtain ⟨g, hg, gf⟩ : ∃ g : ℝ → ℝ, Monotone g ∧ EqOn f g (s ∩ Icc a b) :=
  (hf.mono (inter_subset_left s (Icc a b))).exists_monotone_extension
    (hf.map_bddBelow (inter_subset_left _ _) ⟨a, fun x hx => hx.2.1, as⟩)
    (hf.map_bddAbove (inter_subset_left _ _) ⟨b, fun x hx => hx.2.2, bs⟩)
[GOAL]
case h.intro.intro
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
⊢ ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
[PROOFSTEP]
filter_upwards [hg.ae_differentiableAt] with x hx
[GOAL]
case h
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
⊢ x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
[PROOFSTEP]
intro h'x
[GOAL]
case h
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
⊢ DifferentiableWithinAt ℝ f s x
[PROOFSTEP]
apply hx.differentiableWithinAt.congr_of_eventuallyEq _ (gf ⟨h'x.1, h'x.2.1.le, h'x.2.2.le⟩)
[GOAL]
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
⊢ f =ᶠ[𝓝[s] x] g
[PROOFSTEP]
have : Ioo a b ∈ 𝓝[s] x := nhdsWithin_le_nhds (Ioo_mem_nhds h'x.2.1 h'x.2.2)
[GOAL]
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
this : Ioo a b ∈ 𝓝[s] x
⊢ f =ᶠ[𝓝[s] x] g
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin, this] with y hy h'y
[GOAL]
case h
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
this : Ioo a b ∈ 𝓝[s] x
y : ℝ
hy : y ∈ s
h'y : y ∈ Ioo a b
⊢ f y = g y
[PROOFSTEP]
exact gf ⟨hy, h'y.1.le, h'y.2.le⟩
[GOAL]
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume s, DifferentiableWithinAt ℝ f s x
[PROOFSTEP]
rw [ae_restrict_iff' hs]
[GOAL]
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
[PROOFSTEP]
exact hf.ae_differentiableWithinAt_of_mem
