Source indexedlemma · leanprover/lean4:v4.32.0

Real.mul_four_le_exp_add

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Exp.lean:26 to 39

Source documentation

Combine four elementary exponential majorants.

Exact Lean statement

lemma mul_four_le_exp_add {a b c d A B C D : ℝ}
    (hb0 : 0 ≤ b) (hc0 : 0 ≤ c) (hd0 : 0 ≤ d)
    (ha : a ≤ exp A) (hb : b ≤ exp B) (hc : c ≤ exp C) (hd : d ≤ exp D) :
    a * b * c * d ≤ exp (A + B + C + D)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma mul_four_le_exp_add {a b c d A B C D : ℝ}    (hb0 : 0 ≤ b) (hc0 : 0 ≤ c) (hd0 : 0 ≤ d)    (ha : a ≤ exp A) (hb : b ≤ exp B) (hc : c ≤ exp C) (hd : d ≤ exp D) :    a * b * c * d ≤ exp (A + B + C + D) := by  have hab : a * b ≤ exp A * exp B :=    mul_le_mul ha hb hb0 (exp_pos A).le  have habc : (a * b) * c ≤ (exp A * exp B) * exp C :=    mul_le_mul hab hc hc0 (by positivity)  have hprod : a * b * c * d ≤ exp A * exp B * exp C * exp D :=    mul_le_mul habc hd hd0 (by positivity)  calc    a * b * c * d ≤ exp A * exp B * exp C * exp D := hprod    _ = exp (A + B + C + D) := by        rw [← exp_add, ← exp_add, ← exp_add]