awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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‖
⊢ False
have hsub' : Ι c d ⊆ k
Tactic: have hsub' : Ι c d ⊆ k := Subset.trans Ioc_subset_Icc_self hsub
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
⊢ IntervalIntegrable (deriv f) volume c d
have rw : IntegrableOn (mα := Real.measurableSpace) (deriv f) (Ι c d) volume
Tactic: rw [intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
⊢ IntegrableOn (mα := Real.measurableSpace) (deriv f) (Ι c d) volume
have this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) (Ι c d) volume
Tactic: have : IntegrableOn (fun x ↦ C * ‖g x‖) (Ι c d) := IntegrableOn.mono hgi hsub' le_rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
⊢ False
have hfi : IntervalIntegrable (deriv f) volume c d
Tactic: have hfi : IntervalIntegrable (deriv f) volume c d := by
    rw [intervalIntegrable_iff]
    have : IntegrableOn (fun x ↦ C * ‖g x‖) (Ι c d) := IntegrableOn.mono hgi hsub' le_rfl
    exact Integrable.mono' this (aestronglyMeasurable_deriv _ _) hg_ae
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
⊢ False
have refine : ‖f d‖ - ‖f c‖ ≤ @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖
Tactic: refine hlt.not_ge (sub_le_iff_le_add'.1 ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
⊢ ‖f d‖ - ‖f c‖ ≤ @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
have 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
Tactic: filter_upwards [hd] with x hx using a.toContinuousLinearMap.differentiableAt.comp x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
⊢ ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x
have h₁ : ∀ (a : ℝ), DifferentiableAt ℝ f a → DifferentiableAt ℝ f' a
Tactic: filter_upwards [hd] with x hx using a.toContinuousLinearMap.differentiableAt.comp x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
⊢ ¬IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
have h'd : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
⊢ ¬IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
have h'f : 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'])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
have apply : deriv f' =O[l] deriv f
Tactic: apply IsBigO.trans _ hfg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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] deriv f
have rw : IsBigO (E := ℝ) (F := ℝ) l (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖
Tactic: rw [← isBigO_norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
⊢ IsBigO (E := ℝ) (F := ℝ) l (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖
have suffices : l.EventuallyEq (β := ℝ) (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
⊢ l.EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ ‖deriv f' x‖) fun (x : ℝ) ↦ ‖deriv f x‖
have h : ∀ (x : ℝ) (hx : DifferentiableAt ℝ f x), ‖deriv f' x‖ = ‖deriv f x‖
Tactic: filter_upwards [hd] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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)
have 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)
Tactic: rw [fderiv_comp_deriv x _ hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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)
⊢ deriv f' x = (a : (a : E) → UniformSpace.Completion E) (deriv f x)
have rw₁ : DifferentiableAt ℝ (F := UniformSpace.Completion E) (⇑a : (a : E) → UniformSpace.Completion E) (f x)
Tactic: rw [fderiv_comp_deriv x _ hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
⊢ 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)
have this : fderiv ℝ (⇑a : (a : E) → UniformSpace.Completion E) (f x) = a.toContinuousLinearMap
Tactic: have : fderiv ℝ a (f x) = a.toContinuousLinearMap := a.toContinuousLinearMap.fderiv
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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)
    ((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)
have 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)
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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‖ = ‖deriv f x‖
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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)
⊢ ‖deriv f' x‖ = ‖deriv f x‖
have h : norm (E := UniformSpace.Completion E)
    ((a : (a : E) → UniformSpace.Completion E) (deriv f x) : UniformSpace.Completion E) =
  ‖deriv f x‖
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
⊢ ¬IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
have h'fg : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
⊢ ¬IntervalIntegrable g volume a b
have rw : ¬IntegrableOn (mα := Real.measurableSpace) g [[a, b]] volume
Tactic: rw [intervalIntegrable_iff']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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 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 ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
have inl : ∀ (hlt : min a b < c), ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
Tactic: rcases (min_lt_max.2 hne).gt_or_lt c with hlt | hlt