Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.rpow_add_of_pos

Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:132 to 139

Mathematical statement

Exact Lean statement

lemma rpow_add_of_pos (a : ℝ≥0∞) (c d : ℝ) (hc : 0 < c) (hd : 0 < d) :
    a ^ (c + d) = a ^ c * a ^ d

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rpow_add_of_pos (a : ℝ≥0∞) (c d : ℝ) (hc : 0 < c) (hd : 0 < d) :    a ^ (c + d) = a ^ c * a ^ d := by  have hcd : 0 < c + d := by linarith  rcases (eq_or_ne a 0) with a_eq_zero | a_ne_zero  · rw [a_eq_zero, zero_rpow_of_pos hcd, zero_rpow_of_pos hc, zero_rpow_of_pos hd, mul_zero]  · rcases (eq_or_ne a ⊤) with a_eq_top | a_ne_top    · rw [a_eq_top, top_rpow_of_pos hcd, top_rpow_of_pos hc, top_rpow_of_pos hd, top_mul_top]    · rw [ENNReal.rpow_add c d a_ne_zero a_ne_top]