rpowIntegrand₀₁_zero_left

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

URI: https://scilib.ai/kg/mathlib#Real.rpowIntegrand₀₁_zero_left

English

If 0 < p, then rpowIntegrand₀₁ p 0 x = 0 for all x.

Русский

Если 0 < p, то rpowIntegrand₀₁ p 0 x = 0 для всех x.

LaTeX

$$$rpowIntegrand_{01}(p,0,x) = 0$ for $p>0$$$

Lean4

theorem rpowIntegrand₀₁_zero_left (hp : 0 < p) : rpowIntegrand₀₁ p 0 x = 0 := by
  simp [rpowIntegrand₀₁, Real.zero_rpow hp.ne']

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru