rpowIntegrand₀₁_monotoneOn — Mathlib

English

Let p ∈ (0,1) and t ≥ 0. Then the family t ↦ rpowIntegrand₀₁(p, t) is monotone on [0, ∞).

Русский

Пусть p ∈ (0,1) и t ≥ 0. Тогда отображение t ↦ rpowIntegrand₀₁(p,t) неубывающее на интервале [0, ∞).

LaTeX

$$$\\text{MonotoneOn}\\bigl(t \\mapsto rpowIntegrand_{01}\\,p\\,t\\bigr)\\bigl([0,\\infty)\\bigr)$$$

Lean4

theorem rpowIntegrand₀₁_monotoneOn (hp : p ∈ Ioo 0 1) (ht : 0 ≤ t) : MonotoneOn (rpowIntegrand₀₁ p t) (Ici 0) :=
  by
  intro x hx y hy hxy
  by_cases h : x = 0
  case pos => simpa [h, rpowIntegrand₀₁] using rpowIntegrand₀₁_nonneg hp.1 ht hy
  case neg =>
    simp only [rpowIntegrand₀₁, mem_Ici] at hx h ⊢
    gcongr

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