English
For x,y ∈ ENNReal and z ∈ ℝ, (x y)^z equals ⊤ if a certain negative-exponent condition holds; otherwise equals x^z y^z.
Русский
Для x,y ∈ ENNReal и z ∈ ℝ, (xy)^z равно ⊤, если выполняется условие соотношения нулей и бесконечности при z<0; иначе равно x^z y^z.
LaTeX
$$$$(x y)^{z} = \begin{cases} \top, & \text{если } ((x=0 \land y=\top) \lor (x=\top \land y=0)) \land z<0 \\ x^{z} y^{z}, & \text{иначе} \end{cases}$$$$
Lean4
theorem mul_rpow_eq_ite (x y : ℝ≥0∞) (z : ℝ) :
(x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z :=
by
rcases eq_or_ne z 0 with (rfl | hz); · simp
replace hz := hz.lt_or_gt
wlog hxy : x ≤ y
· convert this y x z hz (le_of_not_ge hxy) using 2 <;> simp only [mul_comm, and_comm, or_comm]
rcases eq_or_ne x 0 with (rfl | hx0)
· induction y <;> rcases hz with hz | hz <;> simp [*, hz.not_gt]
rcases eq_or_ne y 0 with (rfl | hy0)
· exact (hx0 (bot_unique hxy)).elim
induction x
· rcases hz with hz | hz <;> simp [hz, top_unique hxy]
induction y
· rw [ne_eq, coe_eq_zero] at hx0
rcases hz with hz | hz <;> simp [*]
simp only [*]
norm_cast at *
rw [← coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), NNReal.mul_rpow]
norm_cast
