awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (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 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ 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 ⊆ k
hfi : IntervalIntegrable (deriv f) volume c d
d₁ :
  LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι c d)) fun (x : ℝ) ↦ C * ‖g x‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (x : ℝ) ↦ C * ‖g x‖)
⊢ ‖f d‖ - ‖f c‖ ≤ @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖

Tactic:
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_uIoc _
    _ ≤ ∫ x in Ι c d, ‖deriv f x‖ := norm_integral_le_integral_norm _
    _ ≤ ∫ x in Ι c d, C * ‖g x‖ :=
      setIntegral_mono_on hfi.norm.def' (hgi.mono_set hsub') measurableSet_uIoc hg
    _ ≤ ∫ x in k, C * ‖g x‖ := by
      apply setIntegral_mono_set hgi
        (ae_of_all _ fun x => mul_nonneg hC₀ (norm_nonneg _)) hsub'.eventuallyLE

Premises used: intervalIntegral.integral_deriv_eq_sub, Set.uIoc, measurableSet_uIoc, congr_arg, IntervalIntegrable.norm, MeasureTheory.IntegrableOn.mono_set, norm_sub_norm_le, IntervalIntegrable.def', intervalIntegral.norm_integral_eq_norm_integral_uIoc, Eq.symm, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ f' x

Tactic:
a.toContinuousLinearMap.differentiableAt.comp x hx

Premises used: ContinuousLinearMap.differentiableAt, DifferentiableAt.comp, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ DifferentiableAt ℝ f x) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ DifferentiableAt ℝ f' x) x} x}
      a
h₁ h₂ : ∀ (x : ℝ) (hx : DifferentiableAt ℝ f x), DifferentiableAt ℝ f' x
⊢ ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x

Tactic:
filter_upwards [hd] with x hx using a.toContinuousLinearMap.differentiableAt.comp x hx
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
⊢ ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x

Tactic:
have h'd : ∀ᶠ x in l, DifferentiableAt ℝ f' x := by
    filter_upwards [hd] with x hx using a.toContinuousLinearMap.differentiableAt.comp x hx
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
x : ℝ
⊢ ‖f x‖ = ‖f' x‖

Tactic:
simp [f']
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop

Tactic:
have h'f : Tendsto (fun x => ‖f' x‖) l atTop := hf.congr (fun x ↦ by simp [f'])
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
apply : deriv f' =O[l] deriv f
⊢ deriv f' =O[l] g

Tactic:
apply IsBigO.trans _ hfg

Premises used: Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
rw : IsBigO (E := ℝ) (F := ℝ) l (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖
⊢ deriv f' =O[l] deriv f

Tactic:
rw [← isBigO_norm_norm]

Premises used: Asymptotics.isBigO_norm_norm
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
this : l.EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖
⊢ IsBigO (E := ℝ) (F := ℝ) l (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖

Tactic:
this.isBigO

Premises used: Filter.EventuallyEq.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
this : l.EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖
⊢ IsBigO (E := ℝ) (F := ℝ) l (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖

Tactic:
exact this.isBigO

Premises used: Filter.EventuallyEq.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
suffices : l.EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖
⊢ IsBigO (E := ℝ) (F := ℝ) l (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖

Tactic:
suffices (fun x ↦ ‖deriv f' x‖) =ᶠ[l] (fun x ↦ ‖deriv f x‖) by exact this.isBigO
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
h : ∀ (x : ℝ) (hx : DifferentiableAt ℝ f x), ‖deriv f' x‖ = ‖deriv f x‖
⊢ l.EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖

Tactic:
filter_upwards [hd] with x hx
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
rw :
  Eq (α := UniformSpace.Completion E)
    ((fderiv ℝ (⇑a : (a : E) → UniformSpace.Completion E) (f x) : (a : E) → UniformSpace.Completion E) (deriv f x) :
      UniformSpace.Completion E)
    ((a : (a : E) → UniformSpace.Completion E) (deriv f x) : UniformSpace.Completion E)
rw₁ : DifferentiableAt ℝ (F := UniformSpace.Completion E) (⇑a : (a : E) → UniformSpace.Completion E) (f x)
⊢ deriv f' x = (a : (a : E) → UniformSpace.Completion E) (deriv f x)

Tactic:
rw [fderiv_comp_deriv x _ hx]

Premises used: fderiv_comp_deriv
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ 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 : (a : E) → UniformSpace.Completion E) (f x) = a.toContinuousLinearMap

Tactic:
have : fderiv ℝ a (f x) = a.toContinuousLinearMap := a.toContinuousLinearMap.fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ 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 : (a : E) → UniformSpace.Completion E) (f x) = a.toContinuousLinearMap
simp :
  Eq (α := UniformSpace.Completion E)
    ((a.toContinuousLinearMap : (a : E) → UniformSpace.Completion E) (deriv f x) : UniformSpace.Completion E)
    ((a : (a : E) → UniformSpace.Completion E) (deriv f x) : UniformSpace.Completion E)
⊢ Eq (α := UniformSpace.Completion E)
    ((fderiv ℝ (⇑a : (a : E) → UniformSpace.Completion E) (f x) : (a : E) → UniformSpace.Completion E) (deriv f x) :
      UniformSpace.Completion E)
    ((a : (a : E) → UniformSpace.Completion E) (deriv f x) : UniformSpace.Completion E)

Tactic:
simp only [this]
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ 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 : (a : E) → UniformSpace.Completion E) (f x) = a.toContinuousLinearMap
⊢ Eq (α := UniformSpace.Completion E)
    ((a.toContinuousLinearMap : (a : E) → UniformSpace.Completion E) (deriv f x) : UniformSpace.Completion E)
    ((a : (a : E) → UniformSpace.Completion E) (deriv f x) : UniformSpace.Completion E)

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (F := UniformSpace.Completion E) (⇑a : (a : E) → UniformSpace.Completion E) (f x)

Tactic:
a.toContinuousLinearMap.differentiableAt

Premises used: ContinuousLinearMap.differentiableAt, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (F := UniformSpace.Completion E) (⇑a : (a : E) → UniformSpace.Completion E) (f x)

Tactic:
exact a.toContinuousLinearMap.differentiableAt

Premises used: ContinuousLinearMap.differentiableAt, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
x : ℝ
hx : DifferentiableAt ℝ f x
⊢ deriv f' x = (a : (a : E) → UniformSpace.Completion E) (deriv f x)

Tactic:
have : deriv f' x = a (deriv f x) := by
      rw [fderiv_comp_deriv x _ hx]
      · have : fderiv ℝ a (f x) = a.toContinuousLinearMap := a.toContinuousLinearMap.fderiv
        simp only [this]
        rfl
      · exact a.toContinuousLinearMap.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ 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 : (a : E) → UniformSpace.Completion E) (deriv f x)
h :
  norm (E := UniformSpace.Completion E)
      ((a : (a : E) → UniformSpace.Completion E) (deriv f x) : UniformSpace.Completion E) =
    ‖deriv f x‖
⊢ ‖deriv f' x‖ = ‖deriv f x‖

Tactic:
simp only [this]
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ 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 : (a : E) → UniformSpace.Completion E) (deriv f x)
⊢ norm (E := UniformSpace.Completion E)
      ((a : (a : E) → UniformSpace.Completion E) (deriv f x) : UniformSpace.Completion E) =
    ‖deriv f x‖

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ f
h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
h'f : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f' x‖) l atTop
⊢ deriv f' =O[l] g

Tactic:
have h'fg : deriv f' =O[l] g := by
    apply IsBigO.trans _ hfg
    rw [← isBigO_norm_norm]
    suffices (fun x ↦ ‖deriv f' x‖) =ᶠ[l] (fun x ↦ ‖deriv f x‖) by exact this.isBigO
    filter_upwards [hd] with x hx
    have : deriv f' x = a (deriv f x) := by
      rw [fderiv_comp_deriv x _ hx]
      · have : fderiv ℝ a (f x) = a.toContinuousLinearMap := a.toContinuousLinearMap.fderiv
        simp only [this]
        rfl
      · exact a.toContinuousLinearMap.differentiableAt
    simp only [this]
    simp
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ 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 (mα := MeasureSpace.toMeasurableSpace) g k volume

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

Premises used: not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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 : (a : E) → UniformSpace.Completion E) ∘ 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 (mα := MeasureSpace.toMeasurableSpace) g k volume

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

Premises used: not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : 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
rw : ¬IntegrableOn (mα := Real.measurableSpace) g [[a, b]] volume
⊢ ¬IntervalIntegrable g volume a b

Tactic:
rw [intervalIntegrable_iff']

Premises used: intervalIntegrable_iff'