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
f : StieltjesFunction
⊢ ∀ᵐ (x : ℝ), HasDerivAt (↑f) (ENNReal.toReal (rnDeriv (StieltjesFunction.measure f) volume x)) x
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
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
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
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
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
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
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
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)))
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
rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, ← nhds_left'_sup_nhds_right', tendsto_sup]
no goals
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)))
exact ⟨L4, L1⟩
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)
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)))
apply Tendsto.congr' _
  ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_right x)))
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)
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)
filter_upwards [self_mem_nhdsWithin]
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)
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)
rintro y (hxy : x < y)
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)
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)
simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc, Classical.not_not.1 h''x]
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)
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)
rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal]
no goals
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)
exact div_nonneg (sub_nonneg.2 (f.mono hxy.le)) (sub_pos.2 hxy).le
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)
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)))
apply Tendsto.congr' _
  ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_left x)))
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)
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)
filter_upwards [self_mem_nhdsWithin]
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)
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)
rintro y (hxy : y < x)
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)
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)
simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc]
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)
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)
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]
no goals
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)
exact div_nonneg (sub_nonneg.2 (f.mono.leftLim_le hxy.le)) (sub_pos.2 hxy).le
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)
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)))
apply tendsto_apply_add_mul_sq_div_sub (nhds_left'_le_nhds_ne x) L2
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)

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
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)
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
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)
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)
apply Tendsto.mono_left _ nhdsWithin_le_nhds
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)
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)
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)
no goals
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)
simpa using this
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
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
have : Ioo (x - 1) x ∈ 𝓝[<] x := by
  apply Ioo_mem_nhdsWithin_Iio; exact ⟨by linarith, le_refl _⟩
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
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
filter_upwards [this]
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
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
rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
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
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
rw [mem_Iio]
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
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
norm_num
no goals
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
nlinarith
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
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
apply Ioo_mem_nhdsWithin_Iio
no goals
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
exact ⟨by linarith, le_refl _⟩
no goals
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
linarith
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)

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)
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)))
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' L3 L2
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)
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)
filter_upwards [self_mem_nhdsWithin]
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)
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)
rintro y (hy : y < x)
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)
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)
refine' div_le_div_of_nonpos_of_le (by linarith) ((sub_le_sub_iff_right _).2 _)
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
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)
apply f.mono.le_leftLim
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
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
have : ↑0 < (x - y) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
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
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
norm_num
no goals
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
linarith
no goals
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
linarith
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)
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)
filter_upwards [self_mem_nhdsWithin]
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)
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)
rintro y (hy : y < x)
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
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)
refine' div_le_div_of_nonpos_of_le (by linarith) _
no goals
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
simpa only [sub_le_sub_iff_right] using f.mono.leftLim_le (le_refl y)
no goals
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
linarith