awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioo (min 0 1) (max 0 1)) s → HasDerivAt (fun (x : ℝ) ↦ -(x * log x - x)) ((-log) s) s
have hab : ∀ (hs : min 0 1 < s), s < max 0 1 → HasDerivAt (fun (x : ℝ) ↦ -(x * log x - x)) ((-log) s) s
Tactic: ⟨hs, _⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
hs : min 0 1 < s
right : s < max 0 1
⊢ HasDerivAt (fun (x : ℝ) ↦ -(x * log x - x)) ((-log) s) s
have hab : ∀ (hs : 0 < s), s < 1 → HasDerivAt (fun (x : ℝ) ↦ x - x * log x) (-log s) s
Tactic: norm_num at *
Cleared hypotheses: hs, right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioo (min 0 1) (max 0 1)) s → 0 ≤ (-log) s
have hab : ∀ (hs₁ : min 0 1 < s) (hs₂ : s < max 0 1), 0 ≤ (-log) s
Tactic: ⟨hs₁, hs₂⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
s : ℝ
hs₁ : min 0 1 < s
hs₂ : s < max 0 1
⊢ 0 ≤ (-log) s
have hab : ∀ (hs₁ : 0 < s) (hs₂ : s < 1), log s ≤ 0
Tactic: simp at *
Cleared hypotheses: hs₁, hs₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 1 x
have hbc : ContinuousOn log [[1, x]]
Tactic: apply ContinuousOn.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
⊢ ContinuousOn log [[1, x]]
have hbc : [[1, x]] ⊆ {0}ᶜ
Tactic: apply Real.continuousOn_log.mono
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b x : ℝ
hx : 0 < x
⊢ [[1, x]] ⊆ {0}ᶜ
have hx₁ : 0 ∉ [[1, x]]
Tactic: apply Set.notMem_uIcc_of_lt zero_lt_one at hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / (1 + HPow.hPow (β := ℕ) x 2)) μ a b
have hu : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 / (1 + HPow.hPow (β := ℕ) x 2)
Tactic: apply Continuous.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
x : ℝ
⊢ 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
have nlinarith : 1 + HPow.hPow (β := ℕ) x 2 = 0 → -1 + (0 - HPow.hPow (β := ℕ) x 2) + (1 + HPow.hPow (β := ℕ) x 2 - 0) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 / (1 + HPow.hPow (β := ℕ) x 2)
have funProp : ∀ (x : ℝ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
Tactic: fun_prop (discharger := intro; nlinarith)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
have pos : ∀ (t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤),
  IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
Tactic: by_cases t₀ : ∀ u : [[a, b]], meromorphicOrderAt f u ≠ ⊤
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
have neg : ∀ (t₀ : ¬∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤),
  IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
Tactic: by_cases t₀ : ∀ u : [[a, b]], meromorphicOrderAt f u ≠ ⊤
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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 : ℝ) ≠ ⊤
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
have 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
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := hf.extract_zeros_poles t₀
      ((MeromorphicOn.divisor f [[a, b]]).finiteSupport isCompact_uIcc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
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
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
have 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‖
Tactic: have h₄g := MeromorphicOn.extract_zeros_poles_log h₂g h₃g
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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‖
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
have pos : IntervalIntegrable
  (HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
    fun (x : ℝ) ↦ log ‖g x‖)
  volume a b
Tactic: rw [intervalIntegrable_congr_codiscreteWithin
      (h₄g.filter_mono (Filter.codiscreteWithin_mono Set.uIoc_subset_uIcc))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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‖
⊢ IntervalIntegrable
    (HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖)
    volume a b
have pos : IntervalIntegrable (ε := ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
  volume a b
Tactic: apply IntervalIntegrable.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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
⊢ IntervalIntegrable
    (HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖)
    volume a b
have pos₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖g x‖) volume a b
Tactic: apply IntervalIntegrable.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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‖
⊢ IntervalIntegrable (ε := ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
    volume a b
have pos : ∀ (i : ℝ),
  IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) i) : ℝ) * log ‖x - i‖) volume a b
Tactic: apply IntervalIntegrable.finsum
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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‖
i : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) i) : ℝ) * log ‖x - i‖) volume a b
have pos : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x - i‖) volume a b
Tactic: apply IntervalIntegrable.const_mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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‖
i : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x - i‖) volume a b
have pos : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x - i‖) volume (a - i + i) (b - i + i)
Tactic: rw [(by ring : a = ((a - i) + i)), (by ring : b = ((b - i) + i))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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‖
i : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x - i‖) volume (a - i + i) (b - i + i)
have apply : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x‖) volume (a - i) (b - i)
Tactic: apply IntervalIntegrable.comp_sub_right (f := (log ‖·‖)) _ i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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‖
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖g x‖) volume a b
have pos : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ log ‖g x‖) [[a, b]]
Tactic: apply ContinuousOn.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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‖
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ log ‖g x‖) [[a, b]]
have pos : ∀ x ∈ [[a, b]], ‖g x‖ ≠ 0
Tactic: apply h₁g.continuousOn.norm.log
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
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 : ℝ) ≠ ⊤
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
have t₁ : ¬∃ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
Tactic: rw [← hf.exists_meromorphicOrderAt_ne_top_iff_forall (isConnected_Icc inf_le_sup)] at t₀
Cleared hypotheses: t₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
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 : ℝ) ≠ ⊤
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
have t₁ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
Tactic: push Not at t₀
Cleared hypotheses: t₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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 : ℝ) = ⊤
⊢ (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
have apply : (codiscreteWithin [[a, b]]).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
Tactic: apply Filter.EventuallyEq.filter_mono _ (Filter.codiscreteWithin_mono Set.uIoc_subset_uIcc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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 : ℝ) = ⊤
⊢ (codiscreteWithin [[a, b]]).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
have h : ∀ (x : ℝ) (h₁x : MeromorphicNFAt f x) (h₂x : x ∈ [[a, b]]), log ‖f x‖ = 0 x
Tactic: filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin,
        Filter.self_mem_codiscreteWithin [[a, b]]] with x h₁x h₂x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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 : ℝ) = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
⊢ log ‖f x‖ = 0 x
have h : f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1
Tactic: simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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 : ℝ) = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
⊢ f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1
have h : f x = 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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 : ℝ) = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
⊢ f x = 0
have h : ∀ (hCon : ¬f x = 0), False
Tactic: by_contra hCon
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
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 : ℝ) = ⊤
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
have this : (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
Tactic: have : (log ‖f ·‖) =ᶠ[Filter.codiscreteWithin (Ι a b)] 0 := by
      apply Filter.EventuallyEq.filter_mono _ (Filter.codiscreteWithin_mono Set.uIoc_subset_uIcc)
      filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin,
        Filter.self_mem_codiscreteWithin [[a, b]]] with x h₁x h₂x
      simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]
      left
      by_contra hCon
      simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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 : ℝ) = ⊤
this : (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
have neg : IntervalIntegrable (ε := ℝ) 0 volume a b
Tactic: rw [intervalIntegrable_congr_codiscreteWithin this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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 : ℝ) = ⊤
this : (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
⊢ IntervalIntegrable (ε := ℝ) 0 volume a b
have neg : Real.zero✝ = 0 ∨ LT.lt (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
Tactic: apply Iff.mpr _root_.intervalIntegrable_const_iff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
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 : ℝ) = ⊤
this : (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
⊢ Real.zero✝ = 0 ∨ LT.lt (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
have neg : ¬Real.zero✝ = 0 → LT.lt (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log⁺ ‖f x‖) volume a b
have simp_rw : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) volume a b
Tactic: simp_rw [← half_mul_log_add_log_abs, mul_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) volume a b
have hf₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * log ‖f x‖) volume a b
Tactic: apply IntervalIntegrable.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
hf₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * log ‖f x‖) volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) volume a b
have hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * |log ‖f x‖|) volume a b
Tactic: apply IntervalIntegrable.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
a b : ℝ
f : ℝ → ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (log ∘ f) volume a b
have rw : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
Tactic: rw [(by aesop : log ∘ f = (log ‖f ·‖))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
have pos : ∀ (t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤),
  CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
Tactic: by_cases t₀ : ∀ u : (sphere c |R|), meromorphicOrderAt f u ≠ ⊤
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
pos :
  ∀ (t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤),
    CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
have neg : ∀ (t₀ : ¬∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤),
  CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
Tactic: by_cases t₀ : ∀ u : (sphere c |R|), meromorphicOrderAt f u ≠ ⊤