rpowIntegrand₀₁_nonneg — Mathlib

English

For p in (0,1) and t,x ≥ 0, rpowIntegrand equals t^(p-1) x/(t+x).

Русский

Для p ∈ (0,1) и t,x ≥ 0, rpowIntegrand = t^{p-1} x/(t+x).

LaTeX

$$$\text{rpowIntegrand}_{01}(p,t,x) = t^{p-1} \cdot \dfrac{x}{t+x}$$$

Lean4

theorem rpowIntegrand₀₁_nonneg (hp : 0 < p) (ht : 0 ≤ t) (hx : 0 ≤ x) : 0 ≤ rpowIntegrand₀₁ p t x :=
  by
  unfold rpowIntegrand₀₁
  cases eq_or_lt_of_le' ht with
  | inl ht_zero => simp [ht_zero, Real.zero_rpow (ne_of_gt hp)]
  | inr ht_pos =>
    refine mul_nonneg (by positivity) ?_
    rw [sub_nonneg]
    gcongr
    linarith

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