Eq. (7): $g(z) = \tilde H_0/(1+z)^\alpha$ is decreasing for $\alpha>0$

Proved

HuWang2023.gEvolution_strictAntiOn

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

cosmology

Let $\tilde H_0 > 0$ and $\alpha>0$ . Then the evolution function of Eq. (7),

g(z) = H_0(z) = \frac{\tilde H_0}{(1+z)^{\alpha}},

is strictly decreasing on $(-1,\infty)$ (in particular on all physical redshifts $z\ge0$ ).

This is the sense in which a positive $\alpha$ describes a descending trend of the inferred $H_0$ with redshift (Section 5).

Formalization Note $(1+z)^\alpha$ is the real power, defined for $1+z>0$ .

Preamble

import Mathlib
import Definitions.Def_HuWang2023_HubbleTension_Defs

Formal statement

namespace HuWang2023

theorem gEvolution_strictAntiOn (H0tilde α : ℝ) (hH : 0 < H0tilde) (hα : 0 < α) :
    StrictAntiOn (gEvolution H0tilde α) (Set.Ioi (-1)) := by sorry

end HuWang2023

Source

Jian-Ping Hu and Fa-Yin Wang, *Hubble Tension: The Evidence of New Physics*, Universe 2023, 9(2), 94, https://doi.org/10.3390/universe9020094, Section 5, p. 13, Eq. (7) and the sentence following it

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eq. (7): g(z)=H~0/(1+z)αg(z) = \tilde H_0/(1+z)^\alphag(z)=H~0​/(1+z)α is decreasing for α>0\alpha>0α>0

Eq. (7): $g(z) = \tilde H_0/(1+z)^\alpha$ is decreasing for $\alpha>0$