awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
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
⊢ ‖log x‖ / (‖log x‖ + 1) ≤ 1
have rw : ‖log x‖ ≤ ‖log x‖ + 1
Tactic: rw [div_le_one₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
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
rw : ‖log x‖ ≤ ‖log x‖ + 1
⊢ ‖log x‖ / (‖log x‖ + 1) ≤ 1
have rw₁ : 0 < ‖log x‖ + 1
Tactic: rw [div_le_one₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
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
⊢ dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε
have hx' : ‖p * log x‖ ≤ 1
Tactic: have hx' : ‖p * log x‖ ≤ 1 := calc
    _ = p * ‖log x‖ := by grind [norm_mul, Real.norm_of_nonneg]
    _ ≤ 1 / (sSup ((fun y => ‖log y‖) '' s) + 1) * ‖log x‖ := by gcongr
    _ ≤ 1 / (‖log x‖ + 1) * ‖log x‖ := by
        gcongr
        refine le_csSup ?_ (by grind)
        grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
    _ = ‖log x‖ / (‖log x‖ + 1) := by grind
    _ ≤ 1 := by rw [div_le_one₀] <;> grind [norm_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (hypothesis)
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
⊢ dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε
have pinv_nonneg : 0 ≤ p⁻¹
Tactic: have pinv_nonneg : 0 ≤ p⁻¹ := by grind [_root_.inv_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
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⁻¹
⊢ dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε
have h : ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ ε
Tactic: rw [dist_eq_norm']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
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)
have hbc : HPow.hPow (β := ℕ) ‖log x‖ 2 ≤ sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
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⁻¹
⊢ HPow.hPow (β := ℕ) ‖log x‖ 2 ≤ sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)
have hbc : BddAbove (α := ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)
Tactic: refine le_csSup ?_ (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
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 * sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) ≤
    pbound * HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
have h₃ : sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) ≤
  HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
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⁻¹ * (x ^ p - 1) - log x‖ ≤ ε
have _ : p * HPow.hPow (β := ℕ) ‖log x‖ 2 ≤ p * sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
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⁻¹ * (x ^ p - 1) - log x‖ ≤ ε
have _₁ : p * sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) ≤
  pbound * HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto (goal)
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
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ ε
have _₂ : pbound * HAdd.hAdd (α := ℝ) (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s)) 1 = ε
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable (α := ℂ) fun (i : ι) ↦ log (f i)
⊢ Multipliable f
have pos : ∀ (hfn : ∃ (n : ι), f n = 0), Multipliable f
Tactic: by_cases! hfn : ∃ n, f n = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable (α := ℂ) fun (i : ι) ↦ log (f i)
pos : ∀ (hfn : ∃ (n : ι), f n = 0), Multipliable f
⊢ Multipliable f
have neg : ∀ (hfn : ∀ (n : ι), f n ≠ 0), Multipliable f
Tactic: by_cases! hfn : ∃ n, f n = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable f
⊢ Summable (α := ℂ) fun (i : ι) ↦ log (1 + f i)
have apply : ∀ᶠ (i : ι) in cofinite, ‖log (1 + f i)‖ ≤ 3 / 2 * ‖f i‖
Tactic: apply (hf.norm.mul_left (3 / 2)).of_norm_bounded_eventually
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℂ
hf : Summable f
⊢ ∀ᶠ (i : ι) in cofinite, ‖log (1 + f i)‖ ≤ 3 / 2 * ‖f i‖
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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
⊢ ∀ᶠ (i : ι) in cofinite, ‖log (1 + f i)‖ ≤ 3 / 2 * ‖f i‖
have h₁ : ∀ (a : ι), ‖f a‖ ≤ 1 / 2 → ‖log (1 + f a)‖ ≤ 3 / 2 * ‖f a‖
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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)
have apply : EventuallyEq (β := ℝ) cofinite (fun (i : ι) ↦ log (f i)) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
Tactic: apply hf.congr_cofinite
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
⊢ EventuallyEq (β := ℝ) cofinite (fun (i : ι) ↦ log (f i)) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
have 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
Tactic: filter_upwards [hfn] with i hi using by simp [hi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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
⊢ EventuallyEq (β := ℝ) cofinite (fun (i : ι) ↦ log (f i)) fun (i : ι) ↦ log (if 0 < f i then f i else 1)
have h₁ : ∀ (a : ι), 0 < f a → log (f a) = log (if 0 < f a then f a else 1)
Tactic: filter_upwards [hfn] with i hi using by simp [hi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (hypothesis)
Goal:
ι : Type u_1
f : ι → ℝ
hfn : ∀ᶠ (i : ι) in cofinite, 0 < f i
hf : Summable (α := ℝ) fun (i : ι) ↦ log (f i)
⊢ Multipliable f
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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
have refine : ∀ (i : ι), 0 < if 0 < f i then f i else 1
Tactic: refine multipliable_of_summable_log (fun i ↦ ?_) this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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 : ι
⊢ 0 < if 0 < f i then f i else 1
have pos : ∀ (h : 0 < f i), 0 < f i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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
⊢ 0 < if 0 < f i then f i else 1
have neg : ∀ (h : ¬0 < f i), LT.lt (α := ℝ) 0 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (hypothesis)
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 f
have this₁ : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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
have refine_1 : ∀ (i : ι), (if 0 < f i then f i else 1) ≠ 0
Tactic: refine this.congr_cofinite₀ (fun i ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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
⊢ Multipliable f
have refine_2 : ∀ᶠ (a : ι) in cofinite, (if 0 < f a then f a else 1) = f a
Tactic: refine this.congr_cofinite₀ (fun i ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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 : ι
⊢ (if 0 < f i then f i else 1) ≠ 0
have pos : ∀ (h : 0 < f i), f i ≠ 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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
⊢ (if 0 < f i then f i else 1) ≠ 0
have neg : ∀ (h : ¬0 < f i), Ne (α := ℝ) 1 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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
⊢ ∀ᶠ (a : ι) in cofinite, (if 0 < f a then f a else 1) = f a
have 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
Tactic: filter_upwards [hfn] with i hi using by simp [hi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
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
⊢ ∀ᶠ (a : ι) in cofinite, (if 0 < f a then f a else 1) = f a
have h₁ : ∀ (a : ι), 0 < f a → (if 0 < f a then f a else 1) = f a
Tactic: filter_upwards [hfn] with i hi using by simp [hi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ Summable (α := ℝ) fun (i : ι) ↦ log (1 + f i)
have rw : Summable (α := ℂ) fun (x : ι) ↦ (↑(log (1 + f x)) : ℂ)
Tactic: rw [← summable_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ Summable (α := ℂ) fun (x : ι) ↦ (↑(log (1 + f x)) : ℂ)
have apply : EventuallyEq (β := ℂ) cofinite (fun (i : ι) ↦ Complex.log (1 + (↑(f i) : ℂ))) fun (x : ι) ↦ (↑(log (1 + f x)) : ℂ)
Tactic: apply (Complex.summable_log_one_add_of_summable (summable_ofReal.mpr hf)).congr_cofinite
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ EventuallyEq (β := ℂ) cofinite (fun (i : ι) ↦ Complex.log (1 + (↑(f i) : ℂ))) fun (x : ι) ↦ (↑(log (1 + f x)) : ℂ)
have h : ∀ (i : ι) (hi : -1 ≤ f i), Complex.log (1 + (↑(f i) : ℂ)) = (↑(log (1 + f i)) : ℂ)
Tactic: filter_upwards [hf.tendsto_cofinite_zero.eventually_const_le neg_one_lt_zero] with i hi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Summable (goal)
Goal:
ι : Type u_1
f : ι → ℝ
hf : Summable f
i : ι
hi : -1 ≤ f i
⊢ Complex.log (1 + (↑(f i) : ℂ)) = (↑(log (1 + f i)) : ℂ)
have h : 0 ≤ 1 + f i
Tactic: rw [ofReal_log, ofReal_add, ofReal_one]