awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
inr : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ r) volume 0 (-c)
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c

Tactic:
rw [IntervalIntegrable.iff_comp_neg, neg_zero]

Premises used: IntervalIntegrable.iff_comp_neg, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
linarith : -c < 0 → c - 0 + (-c - 0) = 0
⊢ 0 ≤ -c

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r) volume 0 (-c)

Tactic:
have m := (this (-c) (by linarith)).const_mul (Complex.exp (π * Complex.I * r))
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ι 0 (-c)) volume
linarith : -c < 0 → c - 0 + (-c - 0) = 0
⊢ 0 ≤ -c

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
linarith : -c < 0 → c - 0 + (-c - 0) = 0
⊢ 0 ≤ -c

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r) volume 0 (-c)
inr :
  ∀
    (m :
      IntegrableOn (ε := ℂ) (mα := measurableSpace)
        (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r) (Ioc 0 (-c)) volume),
    IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ r) (Ioc 0 (-c)) volume
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ r) volume 0 (-c)

Tactic:
rw [intervalIntegrable_iff, uIoc_of_le (by linarith : 0 ≤ -c)] at m ⊢

Premises used: intervalIntegrable_iff, Set.uIoc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
⊢ IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ r) (Ioc 0 (-c)) volume

Tactic:
m.congr_fun (fun x hx => ?_) measurableSet_Ioc

Premises used: measurableSet_Ioc, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
inr : ∀ (x : ℝ) (hx : x ∈ Ioc 0 (-c)), Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r = (↑(-x) : ℂ) ^ r
⊢ IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ r) (Ioc 0 (-c)) volume

Tactic:
refine m.congr_fun (fun x hx => ?_) measurableSet_Ioc

Premises used: measurableSet_Ioc, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
linarith : 0 < -x → 0 - -x + (0 - x) = 0
⊢ -x ≤ 0

Tactic:
linarith [hx.1]

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
⊢ -x ≤ 0

Tactic:
have : -x ≤ 0 := by linarith [hx.1]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this_1 : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
this : -x ≤ 0
inr :
  (↑x : ℂ) ^ r * Complex.exp ((↑π : ℂ) * Complex.I * r) = (-(↑(-x) : ℂ)) ^ r * Complex.exp ((↑π : ℂ) * Complex.I * r)
⊢ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r = (↑(-x) : ℂ) ^ r

Tactic:
rw [Complex.ofReal_cpow_of_nonpos this, mul_comm]

Premises used: Complex.ofReal_cpow_of_nonpos, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this_1 : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
this : -x ≤ 0
⊢ (↑x : ℂ) ^ r * Complex.exp ((↑π : ℂ) * Complex.I * r) = (-(↑(-x) : ℂ)) ^ r * Complex.exp ((↑π : ℂ) * Complex.I * r)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s : ℂ
t : ℝ
ht : 0 < t
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume ↔ -1 < s.re

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s : ℂ
t : ℝ
ht : 0 < t
refine_1 :
  ∀ (h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume),
    -1 < s.re
refine_2 :
  ∀ (h : -1 < s.re),
    IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume ↔ -1 < s.re

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : -1 < s.re
refine_2 : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) volume 0 t
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume

Tactic:
rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]

Premises used: LT.lt.le, intervalIntegrable_iff_integrableOn_Ioo_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : -1 < s.re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) volume 0 t

Tactic:
intervalIntegrable_cpow' h (a := 0) (b := t)

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : -1 < s.re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) volume 0 t

Tactic:
exact intervalIntegrable_cpow' h (a := 0) (b := t)

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
apply : EqOn (β := ℝ) (fun (a : ℝ) ↦ ‖(↑a : ℂ) ^ s‖) (fun (a : ℝ) ↦ a ^ s.re) (Ioo 0 t)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (a : ℝ) ↦ a ^ s.re) (Ioo 0 t) volume

Tactic:
apply (integrableOn_congr_fun _ measurableSet_Ioo).1 h.norm

Premises used: MeasureTheory.integrableOn_congr_fun, measurableSet_Ioo, Iff.mp, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
a : ℝ
ha : a ∈ Ioo 0 t
⊢ Eq (α := ℝ) ((fun (a : ℝ) ↦ ‖(↑a : ℂ) ^ s‖) a) ((fun (a : ℝ) ↦ a ^ s.re) a)

Tactic:
simp [Complex.norm_cpow_eq_rpow_re_of_pos ha.1]

Premises used: And.left, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (a : ℝ) ↦ a ^ s.re) (Ioo 0 t) volume

Tactic:
have B : IntegrableOn (fun a ↦ a ^ s.re) (Ioo 0 t) := by
    apply (integrableOn_congr_fun _ measurableSet_Ioo).1 h.norm
    intro a ha
    simp [Complex.norm_cpow_eq_rpow_re_of_pos ha.1]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
B : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (a : ℝ) ↦ a ^ s.re) (Ioo 0 t) volume
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ (B : -1 < s.re), -1 < s.re
⊢ -1 < s.re

Tactic:
rwa [integrableOn_Ioo_rpow_iff ht] at B

Premises used: intervalIntegral.integrableOn_Ioo_rpow_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x) μ a b

Tactic:
continuous_id.intervalIntegrable a b

Premises used: Continuous.intervalIntegrable, continuous_id
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b c : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ c) μ a b

Tactic:
continuous_const.intervalIntegrable a b

Premises used: continuous_const, Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
h : ∀ x ∈ [[a, b]], f x ≠ 0
hf : ContinuousOn f [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / f x) μ a b

Tactic:
(continuousOn_const.div hf h).intervalIntegrable

Premises used: continuousOn_const, ContinuousOn.div, ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
h : ∀ x ∈ [[a, b]], f x ≠ 0
hf : ContinuousOn f [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (f x)⁻¹) μ a b

Tactic:
simpa only [one_div] using intervalIntegrable_one_div h hf

Premises used: one_div, intervalIntegral.intervalIntegrable_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable sin μ a b

Tactic:
continuous_sin.intervalIntegrable a b

Premises used: Real.continuous_sin, Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable cos μ a b

Tactic:
continuous_cos.intervalIntegrable a b

Premises used: Continuous.intervalIntegrable, Real.continuous_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable rexp μ a b

Tactic:
continuous_exp.intervalIntegrable a b

Premises used: Continuous.intervalIntegrable, Real.continuous_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
f : ℝ → ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
hf : ContinuousOn f [[a, b]]
h : ∀ x ∈ [[a, b]], f x ≠ 0
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (f x)) μ a b

Tactic:
(ContinuousOn.log hf h).intervalIntegrable

Premises used: ContinuousOn.log, ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
h : 0 ∉ [[a, b]]
⊢ IntervalIntegrable log μ a b

Tactic:
IntervalIntegrable.log continuousOn_id fun _ hx => ne_of_mem_of_not_mem hx h

Premises used: IntervalIntegrable.log, ne_of_mem_of_not_mem, continuousOn_id
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
apply : ∀ (x : ℝ), 0 < x → IntervalIntegrable log volume 0 x
⊢ IntervalIntegrable log volume a b

Tactic:
apply intervalIntegrable_of_even (log_neg_eq_log · |>.symm)

Premises used: Real.log_neg_eq_log, intervalIntegrable_of_even, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
hab : IntervalIntegrable log volume 0 1
hbc : IntervalIntegrable log volume 1 x
⊢ IntervalIntegrable log volume 0 x

Tactic:
apply IntervalIntegrable.trans (b := 1)

Premises used: IntervalIntegrable.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
hab : IntervalIntegrable (- -log) volume 0 1
⊢ IntervalIntegrable log volume 0 1

Tactic:
rw [← neg_neg log]

Premises used: neg_neg, Real.log
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
hab : IntervalIntegrable (-log) volume 0 1
⊢ IntervalIntegrable (- -log) volume 0 1

Tactic:
apply IntervalIntegrable.neg

Premises used: IntervalIntegrable.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
hab : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ -(x * log x - x)) [[0, 1]]
hab₁ :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo (min 0 1) (max 0 1)) x → HasDerivAt (fun (x : ℝ) ↦ -(x * log x - x)) ((-log) x) x
hab₂ : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo (min 0 1) (max 0 1)) x → 0 ≤ (-log) x
⊢ IntervalIntegrable (-log) volume 0 1

Tactic:
apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))

Premises used: intervalIntegral.intervalIntegrable_deriv_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ -(x * log x - x)) [[0, 1]]

Tactic:
(continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg

Premises used: ContinuousOn.neg, Real.continuous_mul_log, Continuous.continuousOn, ContinuousOn.sub, continuous_id
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ -(x * log x - x)) [[0, 1]]

Tactic:
exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg

Premises used: ContinuousOn.neg, Real.continuous_mul_log, Continuous.continuousOn, ContinuousOn.sub, continuous_id
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
hab : ∀ (hs : min 0 1 < s), s < max 0 1 → HasDerivAt (fun (x : ℝ) ↦ -(x * log x - x)) ((-log) s) s
⊢ Membership.mem (γ := Set ℝ) (Ioo (min 0 1) (max 0 1)) s → HasDerivAt (fun (x : ℝ) ↦ -(x * log x - x)) ((-log) s) s

Tactic:
⟨hs, _⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
hs : min 0 1 < s
right : s < max 0 1
hab : ∀ (hs : 0 < s), s < 1 → HasDerivAt (fun (x : ℝ) ↦ x - x * log x) (-log s) s
⊢ HasDerivAt (fun (x : ℝ) ↦ -(x * log x - x)) ((-log) s) s

Tactic:
norm_num at *
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
hs : 0 < s
right : s < 1
⊢ HasDerivAt (fun (x : ℝ) ↦ x - x * log x) (-log s) s

Tactic:
simpa using (hasDerivAt_id s).sub (hasDerivAt_mul_log hs.ne.symm)

Premises used: Real.hasDerivAt_mul_log, HasDerivAt.sub, Ne.symm, hasDerivAt_id, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
hab : ∀ (hs₁ : min 0 1 < s) (hs₂ : s < max 0 1), 0 ≤ (-log) s
⊢ Membership.mem (γ := Set ℝ) (Ioo (min 0 1) (max 0 1)) s → 0 ≤ (-log) s

Tactic:
⟨hs₁, hs₂⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
hs₁ : min 0 1 < s
hs₂ : s < max 0 1
hab : ∀ (hs₁ : 0 < s) (hs₂ : s < 1), log s ≤ 0
⊢ 0 ≤ (-log) s

Tactic:
simp at *
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
hs₁ : 0 < s
hs₂ : s < 1
⊢ log s ≤ 0

Tactic:
(log_nonpos_iff hs₁.le).mpr hs₂.le

Premises used: Iff.mpr, LT.lt.le, Real.log_nonpos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
hs₁ : 0 < s
hs₂ : s < 1
⊢ log s ≤ 0

Tactic:
exact (log_nonpos_iff hs₁.le).mpr hs₂.le

Premises used: Iff.mpr, LT.lt.le, Real.log_nonpos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
hbc : ContinuousOn log [[1, x]]
⊢ IntervalIntegrable log volume 1 x

Tactic:
apply ContinuousOn.intervalIntegrable

Premises used: ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
hbc : [[1, x]] ⊆ {0}ᶜ
⊢ ContinuousOn log [[1, x]]

Tactic:
apply Real.continuousOn_log.mono

Premises used: Real.continuousOn_log, ContinuousOn.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx : 0 < x
⊢ 0 ∉ [[1, x]]

Tactic:
apply Set.notMem_uIcc_of_lt zero_lt_one at hx

Premises used: Set.notMem_uIcc_of_lt, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b x : ℝ
hx_1 : 0 < x
hx : 0 ∉ [[1, x]]
⊢ [[1, x]] ⊆ {0}ᶜ

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
hu : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 / (1 + HPow.hPow (β := ℕ) x 2)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / (1 + HPow.hPow (β := ℕ) x 2)) μ a b

Tactic:
apply Continuous.intervalIntegrable

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
x : ℝ
nlinarith : 1 + HPow.hPow (β := ℕ) x 2 = 0 → -1 + (0 - HPow.hPow (β := ℕ) x 2) + (1 + HPow.hPow (β := ℕ) x 2 - 0) = 0
⊢ 1 + HPow.hPow (β := ℕ) x 2 ≠ 0

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
funProp : ∀ (x : ℝ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 / (1 + HPow.hPow (β := ℕ) x 2)

Tactic:
fun_prop (discharger := intro; nlinarith)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (1 + HPow.hPow (β := ℕ) x 2)⁻¹) μ a b

Tactic:
simp [← one_div, intervalIntegrable_one_div_one_add_sq]

Premises used: intervalIntegral.intervalIntegrable_one_div_one_add_sq, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
pos :
  ∀ (t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤),
    IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
neg :
  ∀ (t₀ : ¬∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤),
    IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b

Tactic:
by_cases t₀ : ∀ u : [[a, b]], meromorphicOrderAt f u ≠ ⊤
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
pos :
  ∀ (g : ℝ → E) (h₁g : AnalyticOnNhd ℝ g [[a, b]]) (h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0)
    (h₃g :
      f =ᶠ[codiscreteWithin [[a, b]]]
        HSMul.hSMul (α := ℝ → ℝ)
          (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ))
          g),
    IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := hf.extract_zeros_poles t₀
      ((MeromorphicOn.divisor f [[a, b]]).finiteSupport isCompact_uIcc)

Premises used: Function.locallyFinsuppWithin.finiteSupport, isCompact_uIcc, MeromorphicOn.divisor, MeromorphicOn.extract_zeros_poles, Set.uIcc
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
⊢ (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖

Tactic:
have h₄g := MeromorphicOn.extract_zeros_poles_log h₂g h₃g
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
pos :
  IntervalIntegrable
    (HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖)
    volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b

Tactic:
rw [intervalIntegrable_congr_codiscreteWithin
      (h₄g.filter_mono (Filter.codiscreteWithin_mono Set.uIoc_subset_uIcc))]

Premises used: Filter.codiscreteWithin_mono, Filter.EventuallyEq.filter_mono, Set.uIoc_subset_uIcc, intervalIntegrable_congr_codiscreteWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
pos :
  IntervalIntegrable (ε := ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
    volume a b
pos₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖g x‖) volume a b
⊢ IntervalIntegrable
    (HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖)
    volume a b

Tactic:
apply IntervalIntegrable.add

Premises used: IntervalIntegrable.add