awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
hbc : BddAbove (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)
⊢ HPow.hPow (β := ℕ) ‖log x‖ 2 ≤ sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)

Tactic:
refine le_csSup ?_ (by grind)

Premises used: le_csSup
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ BddAbove (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)

Tactic:
grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]

Premises used: IsCompact.bddAbove, IsCompact.image_of_continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
h₃ :
  sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) ≤
    HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
⊢ p * sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) ≤
    pbound * HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) ≤
    HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ pbound * HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1 = ε

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))
sSup_nonneg' : LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
hcont : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) s
hcont' : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s)) 1
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
_ : p * HPow.hPow (β := ℕ) ‖log x‖ 2 ≤ p * sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)
_₁ :
  p * sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) ≤
    pbound * HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
_₂ : pbound * HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1 = ε
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ ε

Tactic:
calc
    _ ≤ p * ‖log x‖ ^ 2 := Real.norm_inv_mul_rpow_sub_one_sub_log_le hp₁ (hs hx) hx'
    _ ≤ p * sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
          gcongr
          refine le_csSup ?_ (by grind)
          grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
    _ ≤ pbound * (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1) := by gcongr; grind
    _ = ε := by grind

Premises used: Norm.norm, Real.norm_inv_mul_rpow_sub_one_sub_log_le, Real.log, HPow.hPow, HAdd.hAdd, Set.image, OfNat.ofNat, SupSet.sSup
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
x : ℝ
hx : 0 < x
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
a : ℂ
hfn : ∀ (i : ι), f i ≠ 0
hf : HasSum (fun (i : ι) ↦ log (f i)) a
⊢ ∀ (x : Finset ι), Eq (α := ℂ) (∏ b ∈ x, (cexp ∘ fun (i : ι) ↦ log (f i)) b) (∏ b ∈ x, f b)

Tactic:
simp [exp_log, hfn]

Premises used: Complex.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable (α := ℂ) fun (i : ι) ↦ log (f i)
pos : ∀ (hfn : ∃ (n : ι), f n = 0), Multipliable f
neg : ∀ (hfn : ∀ (n : ι), f n ≠ 0), Multipliable f
⊢ Multipliable f

Tactic:
by_cases! hfn : ∃ n, f n = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable (α := ℂ) fun (i : ι) ↦ log (f i)
hfn : ∃ (n : ι), f n = 0
⊢ Multipliable f

Tactic:
multipliable_of_exists_eq_zero hfn

Premises used: multipliable_of_exists_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable (α := ℂ) fun (i : ι) ↦ log (f i)
hfn : ∃ (n : ι), f n = 0
⊢ Multipliable f

Tactic:
exact multipliable_of_exists_eq_zero hfn

Premises used: multipliable_of_exists_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable (α := ℂ) fun (i : ι) ↦ log (f i)
hfn : ∀ (n : ι), f n ≠ 0
⊢ Multipliable f

Tactic:
⟨_, hasProd_of_hasSum_log hfn hf.hasSum⟩

Premises used: Multipliable, Summable.hasSum, Exists.intro, Complex.hasProd_of_hasSum_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable (α := ℂ) fun (i : ι) ↦ log (f i)
hfn : ∀ (n : ι), f n ≠ 0
⊢ Multipliable f

Tactic:
exact ⟨_, hasProd_of_hasSum_log hfn hf.hasSum⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hfn : ∀ (i : ι), f i ≠ 0
hf : Summable (α := ℂ) fun (i : ι) ↦ log (f i)
⊢ cexp (∑' (i : ι), log (f i)) = ∏' (i : ι), f i

Tactic:
(hasProd_of_hasSum_log hfn hf.hasSum).tprod_eq.symm

Premises used: HasProd.tprod_eq, Summable.hasSum, Complex.hasProd_of_hasSum_log, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable f
apply : ∀ᶠ (i : ι) in cofinite, ‖log (1 + f i)‖ ≤ 3 / 2 * ‖f i‖
⊢ Summable (α := ℂ) fun (i : ι) ↦ log (1 + f i)

Tactic:
apply (hf.norm.mul_left (3 / 2)).of_norm_bounded_eventually

Premises used: HDiv.hDiv, Summable.mul_left, Summable.norm, Summable.of_norm_bounded_eventually, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable f
i : ι
hi : ‖f i‖ ≤ 1 / 2
⊢ ‖log (1 + f i)‖ ≤ 3 / 2 * ‖f i‖

Tactic:
norm_log_one_add_half_le_self hi

Premises used: Complex.norm_log_one_add_half_le_self
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable f
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ ‖f a‖ ≤ 1 / 2) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ ‖log (1 + f i)‖ ≤ 3 / 2 * ‖f i‖) x} x}
      a
h₁ h₂ : ∀ (i : ι) (hi : ‖f i‖ ≤ 1 / 2), ‖log (1 + f i)‖ ≤ 3 / 2 * ‖f i‖
⊢ ∀ᶠ (i : ι) in cofinite, ‖log (1 + f i)‖ ≤ 3 / 2 * ‖f i‖

Tactic:
filter_upwards [hf.norm.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi
    using norm_log_one_add_half_le_self hi

Premises used: Filter.Tendsto.eventually_le_const, Summable.tendsto_cofinite_zero, one_half_pos, Summable.norm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable f
⊢ Multipliable (α := ℂ) fun (i : ι) ↦ 1 + f i

Tactic:
multipliable_of_summable_log (summable_log_one_add_of_summable hf)

Premises used: Complex.multipliable_of_summable_log, Complex.summable_log_one_add_of_summable
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
a : ℝ
hfn : ∀ (i : ι), 0 < f i
hf : HasSum (fun (i : ι) ↦ log (f i)) a
⊢ ∀ (x : Finset ι), Eq (α := ℝ) (∏ b ∈ x, (rexp ∘ fun (i : ι) ↦ log (f i)) b) (∏ b ∈ x, f b)

Tactic:
simp [exp_log, hfn]

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ (i : ι), 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
⊢ Multipliable f

Tactic:
⟨_, hasProd_of_hasSum_log hfn hf.hasSum⟩

Premises used: Multipliable, Summable.hasSum, Exists.intro, Real.hasProd_of_hasSum_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
apply : EventuallyEq (β := ℝ) cofinite (fun (i : ι) ↦ log (f i)) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
⊢ Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)

Tactic:
apply hf.congr_cofinite

Premises used: Summable.congr_cofinite
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
i : ι
hi : 0 < f i
⊢ log (f i) = log (if 0 < f i then f i else 1)

Tactic:
simp [hi]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ 0 < f i) x} x →
          Membership.mem (γ := Set ι)
            {x : ι |
              (fun (x : ι) ↦
                  Eq (α := ℝ) ((fun (i : ι) ↦ log (f i)) x) ((fun (i : ι) ↦ log (if 0 < f i then f i else 1)) x))
                x}
            x}
      a
h₁ h₂ : ∀ (i : ι) (hi : 0 < f i), log (f i) = log (if 0 < f i then f i else 1)
⊢ EventuallyEq (β := ℝ) cofinite (fun (i : ι) ↦ log (f i)) fun (i : ι) ↦ log (if 0 < f i then f i else 1)

Tactic:
filter_upwards [hfn] with i hi using by simp [hi]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
⊢ Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)

Tactic:
have : Summable fun i ↦ log (if 0 < f i then f i else 1) := by
    apply hf.congr_cofinite
    filter_upwards [hfn] with i hi using by simp [hi]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1

Tactic:
multipliable_of_summable_log (fun i ↦ ?_) this

Premises used: Real.multipliable_of_summable_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
refine : ∀ (i : ι), 0 < if 0 < f i then f i else 1
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1

Tactic:
refine multipliable_of_summable_log (fun i ↦ ?_) this

Premises used: Real.multipliable_of_summable_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
i : ι
pos : ∀ (h : 0 < f i), 0 < f i
neg : ∀ (h : ¬0 < f i), LT.lt (α := ℝ) 0 1
⊢ 0 < if 0 < f i then f i else 1

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
i : ι
h : 0 < f i
⊢ 0 < f i

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
i : ι
h : ¬0 < f i
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1

Tactic:
have : Multipliable fun i ↦ if 0 < f i then f i else 1 := by
    refine multipliable_of_summable_log (fun i ↦ ?_) this
    split_ifs with h <;> simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this_1 : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
this : Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1
⊢ Multipliable f

Tactic:
this.congr_cofinite₀ (fun i ↦ ?_) ?_

Premises used: Multipliable.congr_cofinite₀
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this_1 : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
this : Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1
refine_1 : ∀ (i : ι), (if 0 < f i then f i else 1) ≠ 0
refine_2 : ∀ᶠ (a : ι) in cofinite, (if 0 < f a then f a else 1) = f a
⊢ Multipliable f

Tactic:
refine this.congr_cofinite₀ (fun i ↦ ?_) ?_

Premises used: Multipliable.congr_cofinite₀
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this_1 : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
this : Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1
i : ι
pos : ∀ (h : 0 < f i), f i ≠ 0
neg : ∀ (h : ¬0 < f i), Ne (α := ℝ) 1 0
⊢ (if 0 < f i then f i else 1) ≠ 0

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this_1 : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
this : Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1
i : ι
h : 0 < f i
⊢ f i ≠ 0

Tactic:
simp [h, ne_of_gt]

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this_1 : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
this : Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1
i : ι
h : ¬0 < f i
⊢ Ne (α := ℝ) 1 0

Tactic:
simp [h, ne_of_gt]

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this_1 : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
this : Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1
i : ι
hi : 0 < f i
⊢ (if 0 < f i then f i else 1) = f i

Tactic:
simp [hi]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
this_1 : Summable (α := ℝ) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
this : Multipliable (α := ℝ) fun (i : ι) ↦ if 0 < f i then f i else 1
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ 0 < f i) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ (if 0 < f a then f a else 1) = f a) x} x}
      a
h₁ h₂ : ∀ (i : ι) (hi : 0 < f i), (if 0 < f i then f i else 1) = f i
⊢ ∀ᶠ (a : ι) in cofinite, (if 0 < f a then f a else 1) = f a

Tactic:
filter_upwards [hfn] with i hi using by simp [hi]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ (i : ι), 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
⊢ rexp (∑' (i : ι), log (f i)) = ∏' (i : ι), f i

Tactic:
(hasProd_of_hasSum_log hfn hf.hasSum).tprod_eq.symm

Premises used: HasProd.tprod_eq, Summable.hasSum, Eq.symm, Real.hasProd_of_hasSum_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
rw : Summable (α := ℂ) fun (x : ι) ↦ (↑(log (1 + f x)) : ℂ)
⊢ Summable (α := ℝ) fun (i : ι) ↦ log (1 + f i)

Tactic:
rw [← summable_ofReal]

Premises used: Complex.summable_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
apply :
  EventuallyEq (β := ℂ) cofinite (fun (i : ι) ↦ Complex.log (1 + (↑(f i) : ℂ))) fun (x : ι) ↦ (↑(log (1 + f x)) : ℂ)
⊢ Summable (α := ℂ) fun (x : ι) ↦ (↑(log (1 + f x)) : ℂ)

Tactic:
apply (Complex.summable_log_one_add_of_summable (summable_ofReal.mpr hf)).congr_cofinite

Premises used: Iff.mpr, Complex.summable_ofReal, Summable.congr_cofinite, Complex.summable_log_one_add_of_summable
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
h : ∀ (i : ι) (hi : -1 ≤ f i), Complex.log (1 + (↑(f i) : ℂ)) = (↑(log (1 + f i)) : ℂ)
⊢ EventuallyEq (β := ℂ) cofinite (fun (i : ι) ↦ Complex.log (1 + (↑(f i) : ℂ))) fun (x : ι) ↦ (↑(log (1 + f x)) : ℂ)

Tactic:
filter_upwards [hf.tendsto_cofinite_zero.eventually_const_le neg_one_lt_zero] with i hi

Premises used: Filter.Tendsto.eventually_const_le, Summable.tendsto_cofinite_zero, neg_one_lt_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
i : ι
hi : -1 ≤ f i
h : 0 ≤ 1 + f i
⊢ Complex.log (1 + (↑(f i) : ℂ)) = (↑(log (1 + f i)) : ℂ)

Tactic:
rw [ofReal_log, ofReal_add, ofReal_one]

Premises used: Complex.ofReal_log, Complex.ofReal_add, Complex.ofReal_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
i : ι
hi : -1 ≤ f i
linarith : 1 + f i < 0 → -1 - f i + (1 + f i - 0) = 0
⊢ 0 ≤ 1 + f i

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ 1 + f i

Tactic:
multipliable_of_summable_log' ?_ (summable_log_one_add_of_summable hf)

Premises used: Real.summable_log_one_add_of_summable, Real.multipliable_of_summable_log'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
refine : ∀ᶠ (i : ι) in cofinite, 0 < 1 + f i
⊢ Multipliable (α := ℝ) fun (i : ι) ↦ 1 + f i

Tactic:
refine multipliable_of_summable_log' ?_ (summable_log_one_add_of_summable hf)

Premises used: Real.summable_log_one_add_of_summable, Real.multipliable_of_summable_log'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
h : ∀ (i : ι) (hi : -1 < f i), 0 < 1 + f i
⊢ ∀ᶠ (i : ι) in cofinite, 0 < 1 + f i

Tactic:
filter_upwards [hf.tendsto_cofinite_zero.eventually_const_lt neg_one_lt_zero] with i hi

Premises used: Filter.Tendsto.eventually_const_lt, Summable.tendsto_cofinite_zero, neg_one_lt_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
i : ι
hi : -1 < f i
linarith : 1 + f i ≤ 0 → -1 - f i + (1 + f i - 0) = 0
⊢ 0 < 1 + f i

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
⊢ Summable (α := ℝ) fun (s : Finset ι) ↦ ∏ i ∈ s, f i

Tactic:
summable_of_sum_le (c := Real.exp (∑' i, f i))
    (fun s ↦ Finset.prod_nonneg fun i _ ↦ hf i) fun T ↦ ?_

Premises used: summable_of_sum_le, Finset.prod_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
refine : ∀ (T : Finset (Finset ι)), ∑ x ∈ T, ∏ i ∈ x, f i ≤ Real.exp (∑' (i : ι), f i)
⊢ Summable (α := ℝ) fun (s : Finset ι) ↦ ∏ i ∈ s, f i

Tactic:
refine summable_of_sum_le (c := Real.exp (∑' i, f i))
    (fun s ↦ Finset.prod_nonneg fun i _ ↦ hf i) fun T ↦ ?_

Premises used: summable_of_sum_le, Finset.prod_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
T : Finset (Finset ι)
⊢ LE.le (α := ℝ) (∑ s ∈ T, ∏ i ∈ s, f i) (∑ s ∈ (T.biUnion id).powerset, ∏ i ∈ s, f i)

Tactic:
Finset.sum_le_sum_of_subset_of_nonneg (fun s hs ↦ Finset.mem_powerset.mpr
          (Finset.subset_biUnion_of_mem id hs)) (fun s _ _ ↦ Finset.prod_nonneg fun i _ ↦ hf i)

Premises used: Iff.mpr, id, Finset.mem_powerset, Finset.subset_biUnion_of_mem, Finset.sum_le_sum_of_subset_of_nonneg, Finset.prod_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Goal:
ι : Type u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hfs : Summable f
T : Finset (Finset ι)
⊢ Eq (α := ℝ) (∑ s ∈ (T.biUnion id).powerset, ∏ i ∈ s, f i) (∏ i ∈ T.biUnion id, (1 + f i))

Tactic:
(Finset.prod_one_add _).symm

Premises used: Finset.prod_one_add, Eq.symm