E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ ¬IntervalIntegrable f volume a b
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ¬IntervalIntegrable f volume a b
have A : ∀ᶠ x in 𝓝[≠] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x := by
  filter_upwards [self_mem_nhdsWithin] with x hx
  simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[{c}ᶜ] c) atTop
⊢ ¬IntervalIntegrable f volume a b
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ ¬IntervalIntegrable f volume a b
have B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[≠] c) atTop := by
  refine' tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsWithin_zero.comp _)
  rw [← sub_self c]
  exact ((hasDerivAt_id c).sub_const c).tendsto_punctured_nhds one_ne_zero
no goals
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[{c}ᶜ] c) atTop
⊢ ¬IntervalIntegrable f volume a b
exact not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured
  (A.mono fun x hx => hx.differentiableAt) B
  (hf.congr' (A.mono fun x hx => hx.deriv.symm) EventuallyEq.rfl) hne hc
case h
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
x : ℝ
hx : x ∈ {c}ᶜ
⊢ HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
filter_upwards [self_mem_nhdsWithin] with x hx
no goals
case h
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
x : ℝ
hx : x ∈ {c}ᶜ
⊢ HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x => x - c) (𝓝[{c}ᶜ] c) (𝓝[{0}ᶜ] 0)
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[{c}ᶜ] c) atTop
refine' tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsWithin_zero.comp _)
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x => x - c) (𝓝[{c}ᶜ] c) (𝓝[{c - c}ᶜ] (c - c))
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x => x - c) (𝓝[{c}ᶜ] c) (𝓝[{0}ᶜ] 0)
rw [← sub_self c]
no goals
E : Type ?u.29629
F : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[{c}ᶜ] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[{c}ᶜ] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x => x - c) (𝓝[{c}ᶜ] c) (𝓝[{c - c}ᶜ] (c - c))
exact ((hasDerivAt_id c).sub_const c).tendsto_punctured_nhds one_ne_zero