[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
⊢ ¬IntervalIntegrable g volume a b
[PROOFSTEP]
intro hgi
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
⊢ False
[PROOFSTEP]
obtain ⟨C, hC₀, s, hsl, hsub, hfd, hg⟩ :
  ∃ (C : ℝ) (_ : 0 ≤ C),
    ∃ s ∈ l,
      (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ [[a, b]]) ∧
        (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
          ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖ :=
  by
  rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩
  have h :
    ∀ᶠ x : ℝ × ℝ in l.prod l, ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]] :=
    (tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets
  rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩
  simp only [prod_subset_iff, mem_setOf_eq] at hs 
  exact
    ⟨C, C₀, s, hsl, fun x hx y hy z hz => (hs x hx y hy z hz).2, fun x hx y hy z hz => (hs x hx y hy z hz).1.1,
      fun x hx y hy z hz => (hs x hx y hy z hz).1.2⟩
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩
[GOAL]
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
C₀ : 0 ≤ C
hC : IsBigOWith C l (deriv f) g
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
have h :
  ∀ᶠ x : ℝ × ℝ in l.prod l, ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]] :=
  (tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets
[GOAL]
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
C₀ : 0 ≤ C
hC : IsBigOWith C l (deriv f) g
h :
  ∀ᶠ (x : ℝ × ℝ) in Filter.prod l l,
    ∀ (y : ℝ), y ∈ [[x.fst, x.snd]] → (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]]
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
C₀ : 0 ≤ C
hC : IsBigOWith C l (deriv f) g
h :
  ∀ᶠ (x : ℝ × ℝ) in Filter.prod l l,
    ∀ (y : ℝ), y ∈ [[x.fst, x.snd]] → (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]]
s : Set ℝ
hsl : s ∈ l
hs :
  s ×ˢ s ⊆
    {x |
      (fun x => ∀ (y : ℝ), y ∈ [[x.fst, x.snd]] → (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]]) x}
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
simp only [prod_subset_iff, mem_setOf_eq] at hs 
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
C₀ : 0 ≤ C
hC : IsBigOWith C l (deriv f) g
h :
  ∀ᶠ (x : ℝ × ℝ) in Filter.prod l l,
    ∀ (y : ℝ), y ∈ [[x.fst, x.snd]] → (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ [[a, b]]
s : Set ℝ
hsl : s ∈ l
hs :
  ∀ (x : ℝ),
    x ∈ s →
      ∀ (y : ℝ),
        y ∈ s → ∀ (y_1 : ℝ), y_1 ∈ [[x, y]] → (DifferentiableAt ℝ f y_1 ∧ ‖deriv f y_1‖ ≤ C * ‖g y_1‖) ∧ y_1 ∈ [[a, b]]
⊢ ∃ C x s,
    s ∈ l ∧
      (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]) ∧
        (∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z) ∧
          ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
[PROOFSTEP]
exact
  ⟨C, C₀, s, hsl, fun x hx y hy z hz => (hs x hx y hy z hz).2, fun x hx y hy z hz => (hs x hx y hy z hz).1.1,
    fun x hx y hy z hz => (hs x hx y hy z hz).1.2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
⊢ False
[PROOFSTEP]
replace hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
[GOAL]
case hgi
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
hgi : IntervalIntegrable g volume a b
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
⊢ IntervalIntegrable (fun x => C * ‖g x‖) volume a b
[PROOFSTEP]
convert hgi.norm.smul C using 1
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
⊢ False
[PROOFSTEP]
obtain ⟨c, hc, d, hd, hlt⟩ : ∃ c ∈ s, ∃ d ∈ s, (‖f c‖ + ∫ y in Ι a b, C * ‖g y‖) < ‖f d‖ :=
  by
  rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
  have : ∀ᶠ x in l, (‖f c‖ + ∫ y in Ι a b, C * ‖g y‖) < ‖f x‖ := hf.eventually (eventually_gt_atTop _)
  exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
⊢ ∃ c, c ∈ s ∧ ∃ d, d ∈ s ∧ ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
[PROOFSTEP]
rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
[GOAL]
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
⊢ ∃ c, c ∈ s ∧ ∃ d, d ∈ s ∧ ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
[PROOFSTEP]
have : ∀ᶠ x in l, (‖f c‖ + ∫ y in Ι a b, C * ‖g y‖) < ‖f x‖ := hf.eventually (eventually_gt_atTop _)
[GOAL]
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
this : ∀ᶠ (x : ℝ) in l, ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f x‖
⊢ ∃ c, c ∈ s ∧ ∃ d, d ∈ s ∧ ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
[PROOFSTEP]
exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → [[x, y]] ⊆ [[a, b]]
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
⊢ False
[PROOFSTEP]
specialize hsub c hc d hd
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hfd : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
⊢ False
[PROOFSTEP]
specialize hfd c hc d hd
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
⊢ False
[PROOFSTEP]
replace hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
[GOAL]
case hg
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hg : ∀ (x : ℝ), x ∈ s → ∀ (y : ℝ), y ∈ s → ∀ (z : ℝ), z ∈ [[x, y]] → ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
⊢ ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
⊢ False
[PROOFSTEP]
exact fun z hz => hg c hc d hd z ⟨hz.1.le, hz.2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
⊢ False
[PROOFSTEP]
have hg_ae : ∀ᵐ x ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖ := (ae_restrict_mem measurableSet_uIoc).mono hg
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
⊢ False
[PROOFSTEP]
have hsub' : Ι c d ⊆ Ι a b := uIoc_subset_uIoc_of_uIcc_subset_uIcc hsub
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ Ι a b
⊢ False
[PROOFSTEP]
have hfi : IntervalIntegrable (deriv f) volume c d :=
  (hgi.mono_set hsub).mono_fun' (aestronglyMeasurable_deriv _ _) hg_ae
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ Ι a b
hfi : IntervalIntegrable (deriv f) volume c d
⊢ False
[PROOFSTEP]
refine' hlt.not_le (sub_le_iff_le_add'.1 _)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : SecondCountableTopology E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : NeBot l
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntervalIntegrable (fun x => C * ‖g x‖) volume a b
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in Ι a b, C * ‖g y‖ < ‖f d‖
hsub : [[c, d]] ⊆ [[a, b]]
hfd : ∀ (z : ℝ), z ∈ [[c, d]] → DifferentiableAt ℝ f z
hg : ∀ (x : ℝ), x ∈ Ι c d → ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ Ι a b
hfi : IntervalIntegrable (deriv f) volume c d
⊢ ‖f d‖ - ‖f c‖ ≤ ∫ (y : ℝ) in Ι a b, C * ‖g y‖
[PROOFSTEP]
calc
  ‖f d‖ - ‖f c‖ ≤ ‖f d - f c‖ := norm_sub_norm_le _ _
  _ = ‖∫ x in c..d, deriv f x‖ := (congr_arg _ (integral_deriv_eq_sub hfd hfi).symm)
  _ = ‖∫ x in Ι c d, deriv f x‖ := (norm_integral_eq_norm_integral_Ioc _)
  _ ≤ ∫ x in Ι c d, ‖deriv f x‖ := (norm_integral_le_integral_norm _)
  _ ≤ ∫ x in Ι c d, C * ‖g x‖ := (set_integral_mono_on hfi.norm.def (hgi.def.mono_set hsub') measurableSet_uIoc hg)
  _ ≤ ∫ x in Ι a b, C * ‖g x‖ :=
    set_integral_mono_set hgi.def (ae_of_all _ fun x => mul_nonneg hC₀ (norm_nonneg _)) hsub'.eventuallyLE
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
⊢ ¬IntervalIntegrable g volume a b
[PROOFSTEP]
obtain ⟨l, hl, hl', hle, hmem⟩ : ∃ l : Filter ℝ, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ { c } ∈ l :=
  by
  cases' (min_lt_max.2 hne).lt_or_lt c with hlt hlt
  · refine' ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, _⟩
    rw [← Iic_diff_right]
    exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsWithin_Iic ⟨hlt, hc.2⟩) _
  · refine' ⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, _⟩
    rw [← Ici_diff_left]
    exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsWithin_Ici ⟨hc.1, hlt⟩) _
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
⊢ ∃ l, TendstoIxxClass Icc l l ∧ NeBot l ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
[PROOFSTEP]
cases' (min_lt_max.2 hne).lt_or_lt c with hlt hlt
[GOAL]
case inl
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ ∃ l, TendstoIxxClass Icc l l ∧ NeBot l ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
[PROOFSTEP]
refine' ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, _⟩
[GOAL]
case inl
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ [[a, b]] \ {c} ∈ 𝓝[Iio c] c
[PROOFSTEP]
rw [← Iic_diff_right]
[GOAL]
case inl
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ [[a, b]] \ {c} ∈ 𝓝[Iic c \ {c}] c
[PROOFSTEP]
exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsWithin_Iic ⟨hlt, hc.2⟩) _
[GOAL]
case inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ ∃ l, TendstoIxxClass Icc l l ∧ NeBot l ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
[PROOFSTEP]
refine' ⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, _⟩
[GOAL]
case inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ [[a, b]] \ {c} ∈ 𝓝[Ioi c] c
[PROOFSTEP]
rw [← Ici_diff_left]
[GOAL]
case inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ [[a, b]] \ {c} ∈ 𝓝[Ici c \ {c}] c
[PROOFSTEP]
exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsWithin_Ici ⟨hc.1, hlt⟩) _
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : NeBot l
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
⊢ ¬IntervalIntegrable g volume a b
[PROOFSTEP]
have : l ≤ 𝓝[[[a, b]] \ { c }] c := le_inf hle (le_principal_iff.2 hmem)
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : NeBot l
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
this : l ≤ 𝓝[[[a, b]] \ {c}] c
⊢ ¬IntervalIntegrable g volume a b
[PROOFSTEP]
exact
  not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter l (mem_of_superset hmem (diff_subset _ _))
    (h_deriv.filter_mono this) (h_infty.mono_left this) (hg.mono this)
[GOAL]
E : Type u_1
F : Type u_2
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
[PROOFSTEP]
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)
[GOAL]
E : Type u_1
F : Type u_2
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
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with x hx
[GOAL]
case h
E : Type u_1
F : Type u_2
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
[PROOFSTEP]
simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)
[GOAL]
E : Type u_1
F : Type u_2
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
[PROOFSTEP]
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
[GOAL]
E : Type u_1
F : Type u_2
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
[PROOFSTEP]
refine' tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsWithin_zero.comp _)
[GOAL]
E : Type u_1
F : Type u_2
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)
[PROOFSTEP]
rw [← sub_self c]
[GOAL]
E : Type u_1
F : Type u_2
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))
[PROOFSTEP]
exact ((hasDerivAt_id c).sub_const c).tendsto_punctured_nhds one_ne_zero
[GOAL]
E : Type u_1
F : Type u_2
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
[PROOFSTEP]
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
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b ↔ a = b ∨ ¬c ∈ [[a, b]]
[PROOFSTEP]
constructor
[GOAL]
case mp
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b → a = b ∨ ¬c ∈ [[a, b]]
[PROOFSTEP]
refine' fun h => or_iff_not_imp_left.2 fun hne hc => _
[GOAL]
case mp
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
h : IntervalIntegrable (fun x => (x - c)⁻¹) volume a b
hne : ¬a = b
hc : c ∈ [[a, b]]
⊢ False
[PROOFSTEP]
exact not_intervalIntegrable_of_sub_inv_isBigO_punctured (isBigO_refl _ _) hne hc h
[GOAL]
case mpr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
⊢ a = b ∨ ¬c ∈ [[a, b]] → IntervalIntegrable (fun x => (x - c)⁻¹) volume a b
[PROOFSTEP]
rintro (rfl | h₀)
[GOAL]
case mpr.inl
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a a
[PROOFSTEP]
exact IntervalIntegrable.refl
[GOAL]
case mpr.inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
h₀ : ¬c ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b
[PROOFSTEP]
refine' ((continuous_sub_right c).continuousOn.inv₀ _).intervalIntegrable
[GOAL]
case mpr.inr
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b c : ℝ
h₀ : ¬c ∈ [[a, b]]
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → x - c ≠ 0
[PROOFSTEP]
exact fun x hx => sub_ne_zero.2 <| ne_of_mem_of_not_mem hx h₀
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
inst✝ : NormedAddCommGroup F
a b : ℝ
⊢ IntervalIntegrable (fun x => x⁻¹) volume a b ↔ a = b ∨ ¬0 ∈ [[a, b]]
[PROOFSTEP]
simp only [← intervalIntegrable_sub_inv_iff, sub_zero]
