sqrt_rpow_nnreal — Mathlib

English

For any invertible element a and nonnegative NNReal exponent x, sqrt(a^x) = a^(x/2).

Русский

Для обратимого элемента a и неотриценного показателя x ∈ NNReal выполняется sqrt(a^x) = a^(x/2).

LaTeX

$$$\sqrt{a^{x}} = a^{x/2}$ for $a$ invertible and $x \in \mathbb{R}_{\ge 0}$$$

Lean4

theorem sqrt_rpow_nnreal {a : A} {x : ℝ≥0} : sqrt (a ^ (x : ℝ)) = a ^ (x / 2 : ℝ) :=
  by
  by_cases htriv : 0 ≤ a
  case neg => simp [sqrt_eq_cfc, rpow_def, cfc_apply_of_not_predicate a htriv]
  case pos =>
    cases eq_zero_or_pos x with
    | inl hx => simp [hx, rpow_zero _ htriv]
    | inr h₁ =>
      have h₂ : (x : ℝ) / 2 = NNReal.toReal (x / 2) := by simp
      have h₃ : 0 < x / 2 := by positivity
      rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]

Похожие утверждения