awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : ¬x = 0
y : ℝ
hy : y ≠ 0
⊢ deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1

Tactic:
deriv_mul_log hy

Premises used: Real.deriv_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : ¬x = 0
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1) x} x}
      a
h₁ h₂ : ∀ (y : ℝ) (hy : y ≠ 0), deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1

Tactic:
filter_upwards [eventually_ne_nhds hx] with y hy using deriv_mul_log hy

Premises used: eventually_ne_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ StrictConvexOn ℝ (β := ℝ) (Set.Ici 0) fun (x : ℝ) ↦ x * log x

Tactic:
strictConvexOn_of_deriv2_pos (convex_Ici 0) (continuous_mul_log.continuousOn) ?_

Premises used: Real.continuous_mul_log, Continuous.continuousOn, convex_Ici, OfNat.ofNat, strictConvexOn_of_deriv2_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
refine :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (interior (Set.Ici 0)) x →
      LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x * log x) x : ℝ)
⊢ StrictConvexOn ℝ (β := ℝ) (Set.Ici 0) fun (x : ℝ) ↦ x * log x

Tactic:
refine strictConvexOn_of_deriv2_pos (convex_Ici 0) (continuous_mul_log.continuousOn) ?_

Premises used: Real.continuous_mul_log, Continuous.continuousOn, convex_Ici, OfNat.ofNat, strictConvexOn_of_deriv2_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (interior (Set.Ici 0)) x
⊢ 0 < x

Tactic:
simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx

Premises used: Set.mem_Ioi, Set.nonempty_Iio, interior_Ici'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : 0 < x
rw : 0 < x⁻¹
⊢ LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x * log x) x : ℝ)

Tactic:
rw [deriv2_mul_log]

Premises used: Real.deriv2_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : 0 < x
⊢ 0 < x⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ ConvexOn ℝ (β := ℝ) (Set.Ici 0) fun (x : ℝ) ↦ x * log x

Tactic:
strictConvexOn_mul_log.convexOn

Premises used: Real.strictConvexOn_mul_log, StrictConvexOn.convexOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x * log x

Tactic:
mul_nonneg (zero_le_one.trans hx) (log_nonneg hx)

Premises used: mul_nonneg, zero_le_one, Real.log_nonneg, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : 1 < x
⊢ 0 < x * log x

Tactic:
mul_pos (zero_lt_one.trans hx) (log_pos hx)

Premises used: Real.log_pos, zero_lt_one, mul_pos, LT.lt.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx₀ : 0 ≤ x
hx₁ : x ≤ 1
⊢ x * log x ≤ 0

Tactic:
mul_nonpos_of_nonneg_of_nonpos hx₀ (log_nonpos hx₀ hx₁)

Premises used: Real.log_nonpos, mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx₀ : 0 < x
hx₁ : x < 1
⊢ x * log x < 0

Tactic:
mul_neg_of_pos_of_neg  hx₀ (log_neg hx₀ hx₁)

Premises used: Real.log_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ negMulLog = fun (x : ℝ) ↦ -x * log x

Tactic:
rfl

Premises used: Real.negMulLog, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ negMulLog = fun (x : ℝ) ↦ -(x * log x)

Tactic:
simp [negMulLog_def]

Premises used: Real.negMulLog_def
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ negMulLog 0 = 0

Tactic:
simp [negMulLog]

Premises used: Real.negMulLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ negMulLog 1 = 0

Tactic:
simp [negMulLog]

Premises used: Real.negMulLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
⊢ 0 ≤ x.negMulLog

Tactic:
simpa only [negMulLog_eq_neg, neg_nonneg] using mul_log_nonpos h1 h2

Premises used: Real.mul_log_nonpos, neg_nonneg, Real.negMulLog_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x y : ℝ
simp : -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
⊢ (x * y).negMulLog = y * x.negMulLog + x * y.negMulLog

Tactic:
simp only [negMulLog, neg_mul]

Premises used: Real.negMulLog, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x y : ℝ
pos : ∀ (hx : x = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
neg : ∀ (hx : ¬x = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x y : ℝ
hx : x = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x y : ℝ
hx : ¬x = 0
pos : ∀ (hy : y = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
neg : ∀ (hy : ¬y = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x y : ℝ
hx : ¬x = 0
hy : y = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
neg : -(x * y * (log x + log y)) = y * -(x * log x) + x * -(y * log y)
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
rw [log_mul hx hy]

Premises used: Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
⊢ -(x * y * (log x + log y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ Continuous negMulLog

Tactic:
simpa only [negMulLog_eq_neg] using continuous_mul_log.neg

Premises used: Continuous.neg, Real.continuous_mul_log, Real.negMulLog_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ DifferentiableOn ℝ negMulLog {0}ᶜ

Tactic:
simpa only [negMulLog_eq_neg] using differentiableOn_mul_log.neg

Premises used: Real.differentiableOn_mul_log, DifferentiableOn.neg, Real.negMulLog_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
mp : DifferentiableAt ℝ negMulLog x → x ≠ 0
mpr : x ≠ 0 → DifferentiableAt ℝ negMulLog x
⊢ DifferentiableAt ℝ negMulLog x ↔ x ≠ 0

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ -x * log x) x
eq0 : x = 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : ℝ) ↦ y * log y) 0

Tactic:
simp only [neg_mul, differentiableAt_fun_neg_iff, eq0] at h

Premises used: differentiableAt_fun_neg_iff, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
eq0 : x = 0
h : DifferentiableAt ℝ (F := ℝ) (fun (y : ℝ) ↦ y * log y) 0
⊢ False

Tactic:
not_DifferentiableAt_log_mul_zero h

Premises used: Real.not_DifferentiableAt_log_mul_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
eq0 : x = 0
h : DifferentiableAt ℝ (F := ℝ) (fun (y : ℝ) ↦ y * log y) 0
⊢ False

Tactic:
exact not_DifferentiableAt_log_mul_zero h

Premises used: Real.not_DifferentiableAt_log_mul_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ Membership.mem (γ := Set ℝ) {0}ᶜ x

Tactic:
simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true]

Premises used: ne_eq, Set.mem_singleton_iff, not_false_eq_true, Set.mem_compl_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ Membership.mem (γ := Set ℝ) {0}ᶜ x

Tactic:
have : x ∈ ({0} : Set ℝ)ᶜ := by
      simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
this : Membership.mem (γ := Set ℝ) {0}ᶜ x
⊢ DifferentiableWithinAt ℝ negMulLog {0}ᶜ x

Tactic:
have := differentiableOn_negMulLog x this
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
this_1 : Membership.mem (γ := Set ℝ) {0}ᶜ x
this mpr : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
mpr₁ : {0}ᶜ ∈ 𝓝 x
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
apply DifferentiableWithinAt.differentiableAt (s := {0}ᶜ)

Premises used: DifferentiableWithinAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
this_1 : Membership.mem (γ := Set ℝ) {0}ᶜ x
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ DifferentiableWithinAt ℝ negMulLog {0}ᶜ x

Tactic:
simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true,
      compl_singleton_mem_nhds_iff]

Premises used: compl_singleton_mem_nhds_iff, ne_eq, Set.mem_singleton_iff, not_false_eq_true, Set.mem_compl_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
this_1 : Membership.mem (γ := Set ℝ) {0}ᶜ x
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ {0}ᶜ ∈ 𝓝 x

Tactic:
simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true,
      compl_singleton_mem_nhds_iff]

Premises used: compl_singleton_mem_nhds_iff, ne_eq, Set.mem_singleton_iff, not_false_eq_true, Set.mem_compl_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
rw : -(log x + 1) = -log x - 1
⊢ deriv negMulLog x = -log x - 1

Tactic:
rw [negMulLog_eq_neg, deriv.fun_neg, deriv_mul_log hx]

Premises used: Real.deriv_mul_log, deriv.fun_neg, Real.negMulLog_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ -(log x + 1) = -log x - 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
rw : DifferentiableAt ℝ negMulLog x
⊢ HasDerivAt negMulLog (-log x - 1) x

Tactic:
rw [← deriv_negMulLog hx, hasDerivAt_deriv_iff]

Premises used: Real.deriv_negMulLog, hasDerivAt_deriv_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
DifferentiableOn.differentiableAt differentiableOn_negMulLog ?_

Premises used: DifferentiableOn.differentiableAt, Real.differentiableOn_negMulLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
refine : {0}ᶜ ∈ 𝓝 x
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
refine DifferentiableOn.differentiableAt differentiableOn_negMulLog ?_

Premises used: DifferentiableOn.differentiableAt, Real.differentiableOn_negMulLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
rw : deriv^[2] (fun (x : ℝ) ↦ -(x * log x)) x = -x⁻¹
⊢ deriv^[2] negMulLog x = -x⁻¹

Tactic:
rw [negMulLog_eq_neg]

Premises used: Real.negMulLog_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
⊢ ∀ (x : ℝ), deriv^[2] (fun (x : ℝ) ↦ x * log x) x = x⁻¹

Tactic:
have h := deriv2_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h : ∀ (x : ℝ), deriv^[2] (fun (x : ℝ) ↦ x * log x) x = x⁻¹
simp : -deriv (deriv fun (i : ℝ) ↦ i * log i) x = -x⁻¹
⊢ deriv^[2] (fun (x : ℝ) ↦ -(x * log x)) x = -x⁻¹

Tactic:
simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp, deriv.fun_neg',
    Function.comp_apply] at h ⊢

Premises used: Function.iterate_succ, deriv.fun_neg', Function.iterate_zero, Function.comp_apply, Function.id_comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h : ∀ (x : ℝ), deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
rw rw₁ : -x⁻¹ = -x⁻¹
⊢ -deriv (deriv fun (i : ℝ) ↦ i * log i) x = -x⁻¹

Tactic:
rw [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ StrictConcaveOn ℝ (Set.Ici 0) negMulLog

Tactic:
simpa only [negMulLog_eq_neg] using strictConvexOn_mul_log.neg

Premises used: StrictConvexOn.neg, Real.strictConvexOn_mul_log, Real.negMulLog_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ ConcaveOn ℝ (Set.Ici 0) negMulLog

Tactic:
strictConcaveOn_negMulLog.concaveOn

Premises used: StrictConcaveOn.concaveOn, Real.strictConcaveOn_negMulLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
linarith : 1 - x ≤ -x * log x → 1 - x - -x * log x + (x - 1 - x * log x) = 0
⊢ -x * log x < 1 - x

Tactic:
linarith [self_sub_one_lt_mul_log h0 h1]

Premises used: Real.self_sub_one_lt_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
inl : ∀ (h0 : LE.le (α := ℝ) 0 1), negMulLog 1 ≤ HSub.hSub (α := ℝ) 1 1
inr : ∀ (h1 : x ≠ 1), x.negMulLog ≤ 1 - x
⊢ x.negMulLog ≤ 1 - x

Tactic:
rcases eq_or_ne x 1 with rfl | h1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
h0 : LE.le (α := ℝ) 0 1
⊢ negMulLog 1 ≤ HSub.hSub (α := ℝ) 1 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x.negMulLog ≤ 1 - x

Tactic:
le_of_lt (negMulLog_lt_one_sub_self h0 h1)

Premises used: le_of_lt, Real.negMulLog_lt_one_sub_self
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x.negMulLog ≤ 1 - x

Tactic:
exact le_of_lt (negMulLog_lt_one_sub_self h0 h1)

Premises used: le_of_lt, Real.negMulLog_lt_one_sub_self
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
⊢ log⁺ x = max 0 (log x)

Tactic:
rfl

Premises used: Real.posLog, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
rw : max 0 (log x) - max 0 (-log x) = log x
⊢ log⁺ x - log⁺ x⁻¹ = log x

Tactic:
rw [posLog_def, posLog_def, log_inv]

Premises used: Real.posLog_def, Real.log_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
pos : ∀ (h : 0 ≤ log x), max 0 (log x) - max 0 (-log x) = log x
neg : ∀ (h : log x < 0), max 0 (log x) - max 0 (-log x) = log x
⊢ max 0 (log x) - max 0 (-log x) = log x

Tactic:
by_cases! h : 0 ≤ log x

Premises used: Real.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
h : 0 ≤ log x
⊢ max 0 (log x) - max 0 (-log x) = log x

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
h : log x < 0
⊢ max 0 (log x) - max 0 (-log x) = log x

Tactic:
simp [neg_nonneg.1 (Left.nonneg_neg_iff.2 h.le)]

Premises used: Iff.mpr, LT.lt.le, neg_nonneg, Iff.mp, Left.nonneg_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
pos : ∀ (hr : 0 ≤ log x), 2⁻¹ * (log x + |log x|) = log⁺ x
neg : ∀ (hr : log x < 0), 2⁻¹ * (log x + |log x|) = log⁺ x
⊢ 2⁻¹ * (log x + |log x|) = log⁺ x

Tactic:
by_cases! hr : 0 ≤ log x

Premises used: Real.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hr : 0 ≤ log x
pos : 2⁻¹ * (log x + log x) = log x
⊢ 2⁻¹ * (log x + |log x|) = log⁺ x

Tactic:
simp [posLog, hr, abs_of_nonneg]

Premises used: Real.posLog, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hr : 0 ≤ log x
⊢ 2⁻¹ * (log x + log x) = log x

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hr : log x < 0
⊢ 2⁻¹ * (log x + |log x|) = log⁺ x

Tactic:
simp [posLog, hr.le, abs_of_nonpos]

Premises used: Real.posLog, LT.lt.le, abs_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
⊢ log⁺ 0 = 0

Tactic:
simp [posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
⊢ log⁺ 1 = 0

Tactic:
simp [posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
⊢ 0 ≤ log⁺ x

Tactic:
simp [posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
⊢ log⁺ (-x) = log⁺ x

Tactic:
simp [posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
⊢ log⁺ |x| = log⁺ x

Tactic:
simp [posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
rw : log⁺ |x| = 0 ↔ log |x| ≤ 0
⊢ log⁺ x = 0 ↔ |x| ≤ 1

Tactic:
rw [← posLog_abs, ← log_nonpos_iff (abs_nonneg x)]

Premises used: Real.posLog_abs, Real.log_nonpos_iff, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
⊢ log⁺ |x| = 0 ↔ log |x| ≤ 0

Tactic:
simp [posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : 1 ≤ |x|
simp : 0 ≤ log x
⊢ log⁺ x = log x

Tactic:
simp only [posLog, sup_eq_right]

Premises used: Real.posLog, sup_eq_right
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : 1 ≤ |x|
rw : 0 ≤ log |x|
⊢ 0 ≤ log x

Tactic:
rw [← log_abs]

Premises used: Real.log_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : 1 ≤ |x|
⊢ 0 ≤ log |x|

Tactic:
apply log_nonneg hx

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
pos : ∀ (hn : n = 0), log⁺ (↑n : ℝ) = log (↑n : ℝ)
neg : ∀ (hn : ¬n = 0), log⁺ (↑n : ℝ) = log (↑n : ℝ)
⊢ log⁺ (↑n : ℝ) = log (↑n : ℝ)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
hn : n = 0
⊢ log⁺ (↑n : ℝ) = log (↑n : ℝ)

Tactic:
simp [hn, posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
hn : ¬n = 0
⊢ log⁺ (↑n : ℝ) = log (↑n : ℝ)

Tactic:
simp [posLog_eq_log, Nat.one_le_iff_ne_zero.2 hn]

Premises used: Iff.mpr, Real.posLog_eq_log, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log⁺ x = log (max 1 x)

Tactic:
grind [le_abs, posLog_eq_log, log_one, max_eq_left, log_nonpos, posLog_def]

Premises used: Real.log_nonpos, Real.posLog_eq_log, Real.log_one, le_abs, max_eq_left, Real.posLog_def
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
simp : log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
⊢ log⁺ x ≤ log⁺ y

Tactic:
simp only [posLog, le_sup_iff, sup_le_iff, le_refl, true_and]

Premises used: le_refl, Real.posLog, sup_le_iff, le_sup_iff, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
pos : ∀ (h : log x ≤ 0), log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
neg : ∀ (h : 0 < log x), log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

Tactic:
by_cases! h : log x ≤ 0

Premises used: Real.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : log x ≤ 0
pos : ¬log x ≤ 0 → 0 ≤ log y
pos₁ : ¬log x ≤ 0 → log x ≤ log y
pos₂ : ¬log x ≤ 0 → 0 ≤ log y
pos₃ : ¬log x ≤ 0 → log x ≤ log y
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : 0 < log x
neg : 0 ≤ log y ∧ log x ≤ log y
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

Tactic:
right
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : 0 < log x
⊢ log x ≤ log y

Tactic:
have := log_le_log (lt_trans Real.zero_lt_one ((log_pos_iff hx).1 h)) hxy
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : 0 < log x
this : log x ≤ log y
neg : 0 ≤ log y
⊢ 0 ≤ log y ∧ log x ≤ log y

Tactic:
simp only [this, and_true, ge_iff_le]

Premises used: and_true, ge_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ici 0) y
hxy : x ≤ y
h : 0 < log x
this : log x ≤ log y
linarith : log y < 0 → 0 - log x + (log x - log y) + (log y - 0) = 0
⊢ 0 ≤ log y

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
hx : 0 ≤ x
hxy : x ≤ y
⊢ log⁺ x ≤ log⁺ y

Tactic:
monotoneOn_posLog hx (hx.trans hxy) hxy

Premises used: Real.monotoneOn_posLog, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
x : ℝ
pos : ∀ (hn : n = 0), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
neg : ∀ (hn : ¬n = 0), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
x : ℝ
hn : n = 0
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
pos : ∀ (hx : |x| ≤ 1), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
neg : ∀ (hx : ¬|x| ≤ 1), log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x

Tactic:
by_cases hx : |x| ≤ 1
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
hx : |x| ≤ 1
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x

Tactic:
simp_all [pow_le_one₀, (posLog_eq_zero_iff _).2]

Premises used: Iff.mpr, Real.posLog_eq_zero_iff, pow_le_one₀
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
hx : ¬|x| ≤ 1
⊢ 1 < |x|

Tactic:
rw [not_le] at hx

Premises used: not_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
hx : 1 < |x|
⊢ 1 ≤ |x ^ n|

Tactic:
simp_all [one_le_pow₀, hx.le]

Premises used: one_le_pow₀, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
hx : 1 < |x|
⊢ 1 ≤ |x ^ n|

Tactic:
have : 1 ≤ |x ^ n| := by simp_all [one_le_pow₀, hx.le]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
n : ℕ
x : ℝ
hn : ¬n = 0
hx : 1 < |x|
this : 1 ≤ |x ^ n|
⊢ log⁺ (x ^ n) = (↑n : ℝ) * log⁺ x

Tactic:
simp [posLog_eq_log this, posLog_eq_log hx.le]

Premises used: Real.posLog_eq_log, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
pos : ∀ (ha : x = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
neg : ∀ (ha : ¬x = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y

Tactic:
by_cases ha : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
ha : x = 0
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y

Tactic:
simp [ha, posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
ha : ¬x = 0
pos : ∀ (hb : y = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
neg : ∀ (hb : ¬y = 0), log⁺ (x * y) ≤ log⁺ x + log⁺ y
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y

Tactic:
by_cases hb : y = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
ha : ¬x = 0
hb : y = 0
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y

Tactic:
simp [hb, posLog]

Premises used: Real.posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
neg : max (HAdd.hAdd (α := ℝ) 0 0) (log x + log y) ≤ max 0 (log x) + max 0 (log y)
⊢ max 0 (log (x * y)) ≤ max 0 (log x) + max 0 (log y)

Tactic:
nth_rw 1 [← add_zero 0, log_mul ha hb]

Premises used: add_zero, OfNat.ofNat, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
⊢ max (HAdd.hAdd (α := ℝ) 0 0) (log x + log y) ≤ max 0 (log x) + max 0 (log y)

Tactic:
max_add_add_le_max_add_max

Premises used: max_add_add_le_max_add_max
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
⊢ max (HAdd.hAdd (α := ℝ) 0 0) (log x + log y) ≤ max 0 (log x) + max 0 (log y)

Tactic:
exact max_add_add_le_max_add_max

Premises used: max_add_add_le_max_add_max
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
n : ℕ
rw : log⁺ ((↑n : ℝ) * x) ≤ log⁺ (↑n : ℝ) + log⁺ x
⊢ log⁺ ((↑n : ℝ) * x) ≤ log (↑n : ℝ) + log⁺ x

Tactic:
rw [← log_of_nat_eq_posLog]

Premises used: Real.log_of_nat_eq_posLog
-- Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog
Goal:
x : ℝ
n : ℕ
⊢ log⁺ ((↑n : ℝ) * x) ≤ log⁺ (↑n : ℝ) + log⁺ x

Tactic:
posLog_mul

Premises used: Real.posLog_mul