-- Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter
    {f : ℝ → E} {g : ℝ → F}
    {k : Set ℝ} (l : Filter ℝ) [NeBot l] [TendstoIxxClass Icc l l]
    (hl : k ∈ l) (hd : ∀ᶠ x in l, DifferentiableAt ℝ f x) (hf : Tendsto (fun x => ‖f x‖) l atTop)
    (hfg : deriv f =O[l] g) : ¬IntegrableOn g k

Proof state:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x => ‖f' x‖) l atTop
this : (fun x => ‖deriv f' x‖) =ᶠ[l] fun x => ‖deriv f x‖
⊢ (fun x => ‖deriv f' x‖) =O[l] fun x => ‖deriv f x‖

Tactic:
exact this.isBigO

Result:
no goals

Proof state:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
⊢ ¬IntegrableOn g k volume

Tactic:
have h'f : Tendsto (fun x => ‖f' x‖) l atTop := hf.congr (fun x ↦ by simp [f'])

Result:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x => ‖f' x‖) l atTop
⊢ ¬IntegrableOn g k volume

Proof state:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
⊢ ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x

Tactic:
filter_upwards [hd] with x hx using a.toContinuousLinearMap.differentiableAt.comp x hx

Result:
no goals

Proof state:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
⊢ ¬IntegrableOn g k volume

Tactic:
let f' := a ∘ f

Result:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
⊢ ¬IntegrableOn g k volume

Proof state:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x => ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ (fderiv ℝ (⇑a) (f x)) (deriv f x) = a (deriv f x)

Tactic:
have : fderiv ℝ a (f x) = a.toContinuousLinearMap := a.toContinuousLinearMap.fderiv

Result:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x => ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
this : fderiv ℝ (⇑a) (f x) = a.toContinuousLinearMap
⊢ (fderiv ℝ (⇑a) (f x)) (deriv f x) = a (deriv f x)

Proof state:
case h
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x => ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
this : deriv f' x = a (deriv f x)
⊢ ‖a (deriv f x)‖ = ‖deriv f x‖

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x => ‖f' x‖) l atTop
h'fg : deriv f' =O[l] g
⊢ ¬IntegrableOn g k volume

Tactic:
exact not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux l hl h'd h'f h'fg

Result:
no goals

Proof state:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (fun x => ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (⇑a) (f x)

Tactic:
exact a.toContinuousLinearMap.differentiableAt

Result:
no goals