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
f : ℝ → ℝ
hf : Monotone f
⊢ ∀ᵐ (x : ℝ), HasDerivAt f (ENNReal.toReal (rnDeriv (StieltjesFunction.measure (stieltjesFunction hf)) volume x)) x
filter_upwards [hf.stieltjesFunction.ae_hasDerivAt,
  hf.countable_not_continuousAt.ae_not_mem volume] with x hx h'x
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
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
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 _)
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
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
rw [hasDerivAt_iff_tendsto_slope, (nhds_left'_sup_nhds_right' x).symm, tendsto_sup,
  slope_fun_def_field, A] at hx
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)))
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
rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, (nhds_left'_sup_nhds_right' x).symm,
  tendsto_sup]
no goals
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)))
exact ⟨L2, L1⟩
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
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
rw [Classical.not_not, hf.continuousAt_iff_leftLim_eq_rightLim] at h'x
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
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
apply le_antisymm _ (hf.le_rightLim (le_refl _))
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
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
rw [← h'x]
no goals
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
exact hf.leftLim_le (le_refl _)
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)

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)
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)))
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
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)
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)))
apply tendsto_apply_add_mul_sq_div_sub (nhds_right'_le_nhds_ne x) hx.2
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)

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
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)
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
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)
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)
apply Tendsto.mono_left _ nhdsWithin_le_nhds
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)
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)
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 : ℝ → ℝ
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)
simpa using this
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
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
have : Ioo x (x + 1) ∈ 𝓝[>] x := by
  apply Ioo_mem_nhdsWithin_Ioi; exact ⟨le_refl _, by linarith⟩
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
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
filter_upwards [this]
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
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
rintro y ⟨hy : x < y, h'y : y < x + 1⟩
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
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
rw [mem_Ioi]
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
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
norm_num
no goals
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
nlinarith
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)
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
apply Ioo_mem_nhdsWithin_Ioi
no goals
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)
exact ⟨le_refl _, by linarith⟩
no goals
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
linarith
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)
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)
filter_upwards [self_mem_nhdsWithin]
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)
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)
rintro y (hy : x < y)
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)
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)
have : ↑0 < (y - x) ^ 2 := sq_pos_of_pos (sub_pos.2 hy)
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
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)
apply div_le_div_of_le_of_nonneg _ (sub_pos.2 hy).le
no goals
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
exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by norm_num; linarith))
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
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
norm_num
no goals
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
linarith
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)
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)
filter_upwards [self_mem_nhdsWithin]
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)
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)
rintro y (hy : x < y)
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
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)
apply div_le_div_of_le_of_nonneg _ (sub_pos.2 hy).le
no goals
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
exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl y))
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)

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)
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)))
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hx.1 this
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)
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)))
apply tendsto_apply_add_mul_sq_div_sub (nhds_left'_le_nhds_ne x) hx.1
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)

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
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)
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
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)
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)
apply Tendsto.mono_left _ nhdsWithin_le_nhds
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)
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)
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 : ℝ → ℝ
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)
simpa using this
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
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
have : Ioo (x - 1) x ∈ 𝓝[<] x := by
  apply Ioo_mem_nhdsWithin_Iio; exact ⟨by linarith, le_refl _⟩
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
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
filter_upwards [this]
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
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
rintro y ⟨hy : x - 1 < y, h'y : y < x⟩
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
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
rw [mem_Iio]
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
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
norm_num
no goals
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
nlinarith
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
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
apply Ioo_mem_nhdsWithin_Iio
no goals
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
exact ⟨by linarith, le_refl _⟩
no goals
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
linarith
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)
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)
filter_upwards [self_mem_nhdsWithin]
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)
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)
rintro y (hy : y < x)
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
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)
apply div_le_div_of_nonpos_of_le (sub_neg.2 hy).le
no goals
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
exact (sub_le_sub_iff_right _).2 (hf.le_rightLim (le_refl _))
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)
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)
filter_upwards [self_mem_nhdsWithin]
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)
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)
rintro y (hy : y < x)
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)
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)
have : ↑0 < (y - x) ^ 2 := sq_pos_of_neg (sub_neg.2 hy)
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
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)
apply div_le_div_of_nonpos_of_le (sub_neg.2 hy).le
no goals
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
exact (sub_le_sub_iff_right _).2 (hf.rightLim_le (by norm_num; linarith))
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
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
norm_num
no goals
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
linarith