nnrpow — Mathlib

English

Real powers of operators are defined by applying NNReal powers inside the nonunital continuous functional calculus: a^y = cfcₙ (NNReal.nnrpow · y) a.

Русский

Реальные степени операторов задаются через NNReal-степени внутри неполного непрерывного функционального вычислителя: a^y = cfcₙ (NNReal.nnrpow · y) a.

LaTeX

$$a^y = cfcₙ (NNReal.nnrpow · y) a$$

Lean4

/-- Taking a nonnegative power of a nonnegative number. This is defined as a standalone definition
in order to speed up automation such as `cfc_cont_tac`. -/
noncomputable abbrev nnrpow (a : ℝ≥0) (b : ℝ≥0) : ℝ≥0 :=
  a ^ (b : ℝ)

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