awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
n : ℕ
⊢ log⁺ ((↑n : ℝ) * x) ≤ log⁺ (↑n : ℝ) + log⁺ x

Tactic:
exact posLog_mul

Premises used: Real.posLog_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
f : α → ℝ
⊢ log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)

Tactic:
simp [posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
rw rw₁ : log⁺ (f a * ∏ x ∈ s, f x) = log⁺ (f a * ∏ t ∈ s, f t)
⊢ log⁺ (∏ t ∈ insert a s, f t) = log⁺ (f a * ∏ t ∈ s, f t)

Tactic:
rw [Finset.prod_insert ha]

Premises used: Finset.prod_insert
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (f a * ∏ t ∈ s, f t) ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t)

Tactic:
posLog_mul

Premises used: Real.posLog_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (f a) ≤ log⁺ (f a)

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
rw rw₁ : log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) = log⁺ (f a) + ∑ x ∈ s, log⁺ (f x)
⊢ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) = ∑ t ∈ insert a s, log⁺ (f t)

Tactic:
rw [Finset.sum_insert ha]

Premises used: Finset.sum_insert
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
calc : log⁺ (∏ t ∈ insert a s, f t) = log⁺ (f a * ∏ t ∈ s, f t)
calc₁ : log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) = ∑ t ∈ insert a s, log⁺ (f t)
⊢ log⁺ (∏ t ∈ insert a s, f t) ≤ ∑ t ∈ insert a s, log⁺ (f t)

Tactic:
calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]

Premises used: HMul.hMul, Real.posLog, add_le_add, Insert.insert, Finset.prod, Real.posLog_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
empty : log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s) (hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)),
    log⁺ (∏ t ∈ Insert.insert a s, f t) ≤ ∑ t ∈ Insert.insert a s, log⁺ (f t)
⊢ log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
induction s using Finset.induction with
  | empty => simp [posLog]
  | insert a s ha hs =>
    calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]

Premises used: Real.posLog, Insert.insert, Finset.prod, Real.posLog_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
empty : log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s) (hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)),
    log⁺ (∏ t ∈ Insert.insert a s, f t) ≤ ∑ t ∈ Insert.insert a s, log⁺ (f t)
⊢ log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp [posLog]
  | insert a s ha hs =>
    calc log⁺ (∏ t ∈ insert a s, f t)
    _ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
    _ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
    _ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
    _ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]

Premises used: Real.posLog, Insert.insert, Finset.prod, Real.posLog_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
pos : ∀ (hs : s = ∅), log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
neg : ∀ (hs : s.Nonempty), log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)

Tactic:
by_cases! hs : s = ∅
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s = ∅
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)

Tactic:
simp [hs, posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
neg :
  ∀ (t_max : α) (ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|),
    log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)

Tactic:
obtain ⟨t_max, ht_max⟩ := s.exists_max_image (fun t ↦ |f t|) hs

Premises used: abs, Finset.exists_max_image
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
rw rw₁ : log⁺ (∑ t ∈ s, f t) = log⁺ (∑ t ∈ s, f t)
⊢ log⁺ (∑ t ∈ s, f t) = log⁺ |∑ t ∈ s, f t|

Tactic:
rw [Real.posLog_abs]

Premises used: Real.posLog_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) |∑ t ∈ s, f t|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) (∑ t ∈ s, |f t|)

Tactic:
simp [Finset.sum_nonneg]

Premises used: Finset.sum_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
apply : LE.le (α := ℝ) |∑ t ∈ s, f t| (∑ t ∈ s, |f t|)
⊢ log⁺ |∑ t ∈ s, f t| ≤ log⁺ (∑ t ∈ s, |f t|)

Tactic:
apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])

Premises used: Real.monotoneOn_posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ LE.le (α := ℝ) |∑ t ∈ s, f t| (∑ t ∈ s, |f t|)

Tactic:
simp [Finset.abs_sum_le_sum_abs]

Premises used: Finset.abs_sum_le_sum_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) (∑ t ∈ s, |f t_max|)

Tactic:
simp [mul_nonneg]

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
apply : LE.le (α := ℝ) (∑ t ∈ s, |f t|) (∑ t ∈ s, |f t_max|)
⊢ log⁺ (∑ t ∈ s, |f t|) ≤ log⁺ (∑ t ∈ s, |f t_max|)

Tactic:
apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])

Premises used: Real.monotoneOn_posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ LE.le (α := ℝ) (∑ t ∈ s, |f t|) (∑ t ∈ s, |f t_max|)

Tactic:
apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)

Premises used: And.right, Finset.sum_le_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, |f t_max|) = log⁺ ((↑s.card : ℝ) * |f t_max|)

Tactic:
simp [Finset.sum_const]

Premises used: Finset.sum_const
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ ((↑s.card : ℝ) * |f t_max|) ≤ log (↑s.card : ℝ) + log⁺ |f t_max|

Tactic:
posLog_nat_mul

Premises used: Real.posLog_nat_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
bc : log⁺ |f t_max| ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log (↑s.card : ℝ) + log⁺ |f t_max| ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
bc : log⁺ (f t_max) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ |f t_max| ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
rw [posLog_abs]

Premises used: Real.posLog_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (f t_max) ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1

Premises used: And.left, Finset.single_le_sum, Real.posLog_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
calc : log⁺ (∑ t ∈ s, f t) = log⁺ |∑ t ∈ s, f t|
calc₁ : log⁺ |∑ t ∈ s, f t| ≤ log⁺ (∑ t ∈ s, |f t|)
calc₂ : log⁺ (∑ t ∈ s, |f t|) ≤ log⁺ (∑ t ∈ s, |f t_max|)
calc₃ : log⁺ (∑ t ∈ s, |f t_max|) = log⁺ ((↑s.card : ℝ) * |f t_max|)
calc₄ : log (↑s.card : ℝ) + log⁺ |f t_max| ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∑ t ∈ s, f t) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ (f t)

Tactic:
calc log⁺ (∑ t ∈ s, f t)
  _ = log⁺ |∑ t ∈ s, f t| := by
    rw [Real.posLog_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t|) := by
    apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
    simp [Finset.abs_sum_le_sum_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by
    apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
    apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)
  _ = log⁺ (s.card * |f t_max|) := by
    simp [Finset.sum_const]
  _ ≤ log s.card + log⁺ |f t_max| := posLog_nat_mul
  _ ≤ log s.card + ∑ t ∈ s, log⁺ (f t) := by
    gcongr
    rw [posLog_abs]
    apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1

Premises used: HMul.hMul, Real.posLog, abs, Nat.cast, Real.log, Finset.card, Finset.sum, Real.posLog_nat_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
α : Type u_2
s : Finset α
f : α → E
h₁ : LE.le (α := ℝ) 0 (Norm.norm.{u_1} (E := E) (∑ i ∈ s, f i))
grw : log⁺ (∑ i ∈ s, ‖f i‖) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖
grw₁ grw₂ : log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖ ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖
⊢ log⁺ (Norm.norm.{u_1} (E := E) (∑ t ∈ s, f t)) ≤ log (↑s.card : ℝ) + ∑ t ∈ s, log⁺ ‖f t‖

Tactic:
grw [norm_sum_le, posLog_sum]

Premises used: Real.posLog_sum, norm_sum_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
⊢ log⁺ (∑ t : Fin (Nat.succ 0).succ, ![x, y] t) ≤
    log (↑(Finset.card (α := Fin (Nat.succ 0).succ) Finset.univ) : ℝ) + ∑ t : Fin (Nat.succ 0).succ, log⁺ (![x, y] t)

Tactic:
posLog_sum Finset.univ ![x, y]

Premises used: Finset.univ, Matrix.vecEmpty, Real.posLog_sum, Matrix.vecCons
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
h : log⁺ (x + y) = log⁺ (∑ t : Fin (Nat.succ 0).succ, ![x, y] t)
h₁ :
  log 2 + log⁺ x + log⁺ y =
    log (↑(Finset.card (α := Fin (Nat.succ 0).succ) Finset.univ) : ℝ) + ∑ t : Fin (Nat.succ 0).succ, log⁺ (![x, y] t)
⊢ log⁺ (x + y) ≤ log 2 + log⁺ x + log⁺ y

Tactic:
convert! posLog_sum Finset.univ ![x, y] using 1

Premises used: Finset.univ, Matrix.vecEmpty, Real.posLog_sum, Matrix.vecCons
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
⊢ log⁺ (x + y) = log⁺ (∑ t : Fin (Nat.succ 0).succ, ![x, y] t)

Tactic:
simp [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
⊢ log 2 + log⁺ x + log⁺ y =
    log (↑(Finset.card (α := Fin (Nat.succ 0).succ) Finset.univ) : ℝ) + ∑ t : Fin (Nat.succ 0).succ, log⁺ (![x, y] t)

Tactic:
simp [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
h₁ : LE.le (α := ℝ) 0 ‖a + b‖
grw : log⁺ (‖a‖ + ‖b‖) ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
grw₁ : log 2 + log⁺ ‖a‖ + log⁺ ‖b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
grw₂ grw₃ : log⁺ ‖a‖ + log⁺ ‖b‖ + log 2 ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
⊢ log⁺ ‖a + b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2

Tactic:
grw [norm_add_le, posLog_add, add_rotate]

Premises used: norm_add_le, add_rotate, Real.posLog_add
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
⊢ 0 ≤ p⁻¹

Tactic:
grind [_root_.inv_nonneg]

Premises used: inv_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
⊢ 0 ≤ p⁻¹

Tactic:
have pinv_nonneg : 0 ≤ p⁻¹ := by grind [_root_.inv_nonneg]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ = ‖p⁻¹ * (x ^ p - 1 - p * log x)‖

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
simp : p⁻¹ * ‖x ^ p - 1 - p * log x‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖
⊢ ‖p⁻¹ * (x ^ p - 1 - p * log x)‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖

Tactic:
simp only [norm_mul, Real.norm_of_nonneg (r := p⁻¹) pinv_nonneg]

Premises used: norm_mul, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
e_a : x ^ p = rexp (p * log x)
⊢ p⁻¹ * ‖x ^ p - 1 - p * log x‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ 0 < x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
e_a : x ^ p = rexp (log x * p)
e_a₁ : x ^ p = rexp (log x) ^ p
e_a₂ e_a₃ : x ^ p = x ^ p
⊢ x ^ p = rexp (p * log x)

Tactic:
rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]

Premises used: Real.exp_mul, Real.exp_log, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
hbc : ‖rexp (p * log x) - 1 - p * log x‖ ≤ HPow.hPow (β := ℕ) ‖p * log x‖ 2
⊢ p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖ ≤ p⁻¹ * HPow.hPow (β := ℕ) ‖p * log x‖ 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ ‖rexp (p * log x) - 1 - p * log x‖ ≤ HPow.hPow (β := ℕ) ‖p * log x‖ 2

Tactic:
Real.norm_exp_sub_one_sub_id_le ?_

Premises used: Real.norm_exp_sub_one_sub_id_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
hbc : ‖p * log x‖ ≤ 1
⊢ ‖rexp (p * log x) - 1 - p * log x‖ ≤ HPow.hPow (β := ℕ) ‖p * log x‖ 2

Tactic:
refine Real.norm_exp_sub_one_sub_id_le ?_

Premises used: Real.norm_exp_sub_one_sub_id_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ ‖p * log x‖ ≤ 1

Tactic:
simp only [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
simp : p⁻¹ * HPow.hPow (β := ℕ) (‖p‖ * ‖log x‖) 2 = p * HPow.hPow (β := ℕ) ‖log x‖ 2
⊢ p⁻¹ * HPow.hPow (β := ℕ) ‖p * log x‖ 2 = p * HPow.hPow (β := ℕ) ‖log x‖ 2

Tactic:
simp only [norm_mul]

Premises used: norm_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p⁻¹ * HPow.hPow (β := ℕ) (‖p‖ * ‖log x‖) 2 = p * HPow.hPow (β := ℕ) ‖log x‖ 2

Tactic:
grind [Real.norm_of_nonneg]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
_ : ‖p⁻¹ * (x ^ p - 1) - log x‖ = ‖p⁻¹ * (x ^ p - 1 - p * log x)‖
_₁ : ‖p⁻¹ * (x ^ p - 1 - p * log x)‖ = p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖
_₂ : p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖ ≤ p⁻¹ * HPow.hPow (β := ℕ) ‖p * log x‖ 2
_₃ : p⁻¹ * HPow.hPow (β := ℕ) ‖p * log x‖ 2 = p * HPow.hPow (β := ℕ) ‖log x‖ 2
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ p * HPow.hPow (β := ℕ) ‖log x‖ 2

Tactic:
calc
    _ = ‖p⁻¹ * ((x ^ p - 1) - p * log x)‖ := by grind
    _ = p⁻¹ * ‖(rexp (p * log x) - 1) - p * log x‖ := by
          simp only [norm_mul, Real.norm_of_nonneg (r := p⁻¹) pinv_nonneg]
          congr
          rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]
    _ ≤ p⁻¹ * ‖p * log x‖ ^ 2 := by
          gcongr
          refine Real.norm_exp_sub_one_sub_id_le ?_
          simp only [hx]
    _ = p * ‖log x‖ ^ 2 := by
          simp only [norm_mul]
          grind [Real.norm_of_nonneg]

Premises used: HMul.hMul, HSub.hSub, Real.exp, Real.log, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
⊢ TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) (Ioi 0)

Tactic:
(tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi).mpr ?_

Premises used: Iff.mpr, isOpen_Ioi, tendstoLocallyUniformlyOn_iff_forall_isCompact
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
refine : ∀ K ⊆ Ioi 0, IsCompact K → TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) K
⊢ TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) (Ioi 0)

Tactic:
refine (tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi).mpr ?_

Premises used: Iff.mpr, isOpen_Ioi, tendstoLocallyUniformlyOn_iff_forall_isCompact
-- Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Goal:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
rw :
  ∀ (i : ℝ),
    0 < i →
      ∀ᶠ (n : ℝ) in 𝓝[>] 0,
        ∀ x ∈ s, Membership.mem (γ := Set (ℝ × ℝ)) {p : ℝ × ℝ | dist p.1 p.2 ≤ i} (log x, n⁻¹ * (x ^ n - 1))
⊢ TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) s

Tactic:
rw [Metric.uniformity_basis_dist_le.tendstoUniformlyOn_iff_of_uniformity]

Premises used: Filter.HasBasis.tendstoUniformlyOn_iff_of_uniformity, Metric.uniformity_basis_dist_le
-- 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
⊢ ∀ x ∈ s, x ≠ 0

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
⊢ ∀ x ∈ s, x ≠ 0

Tactic:
have hxs : ∀ x ∈ s, x ≠ 0 := by 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
⊢ LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))

Tactic:
Real.sSup_nonneg ?_

Premises used: Real.sSup_nonneg
-- 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
refine : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) x → 0 ≤ x
⊢ LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))

Tactic:
refine Real.sSup_nonneg ?_

Premises used: Real.sSup_nonneg
-- 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
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s) x → 0 ≤ x

Tactic:
grind [← sq_nonneg]

Premises used: sq_nonneg
-- 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
⊢ LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖log x‖ 2) '' s))

Tactic:
have sSup_nonneg : 0 ≤ sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
    refine Real.sSup_nonneg ?_
    grind [← sq_nonneg]
-- 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))
⊢ LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))

Tactic:
Real.sSup_nonneg ?_

Premises used: Real.sSup_nonneg
-- 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))
refine : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ ‖log x‖) '' s) x → 0 ≤ x
⊢ LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))

Tactic:
refine Real.sSup_nonneg ?_

Premises used: Real.sSup_nonneg
-- 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))
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ ‖log x‖) '' s) x → 0 ≤ x

Tactic:
grind [← sq_nonneg]

Premises used: sq_nonneg
-- 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))
⊢ LE.le (α := ℝ) 0 (sSup ((fun (x : ℝ) ↦ ‖log x‖) '' s))

Tactic:
have sSup_nonneg' : 0 ≤ sSup ((fun x => ‖log x‖) '' s) := by
    refine Real.sSup_nonneg ?_
    grind [← sq_nonneg]
-- 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))
⊢ 0 < pbound

Tactic:
positivity
-- 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))
⊢ 0 < pbound

Tactic:
have pbound_pos : 0 < pbound := by positivity