Eq. (5): $\langle \mathrm{DM_{IGM}}(z)\rangle$ is strictly increasing in redshift

Proved

HuWang2023.meanDMIGM_strictMonoOn

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

cosmologyfast-radio-bursts

Let $A>0$ , $\Omega_b>0$ , $H_0>0$ and $\Omega_m\ge0$ , and let $f_{\rm IGM}$ and $f_e$ be functions that are continuous and strictly positive on $[0,\infty)$ . Then the mean intergalactic dispersion measure of Eq. (5),

\langle {\rm DM_{IGM}}(z)\rangle = \frac{A\Omega_b H_0^2}{H_0}\int_0^{z}\frac{f_{\rm IGM}(z')f_e(z')(1+z')}{\sqrt{\Omega_m(1+z')^3+1-\Omega_m}}\,dz',

is a strictly increasing function of $z$ on $[0,\infty)$ .

Strict monotonicity means the dispersion measure–redshift relation can be inverted, which is what allows FRBs to serve as distance indicators and cosmological probes (Section 3.4).

Preamble

import Mathlib
import Definitions.Def_HuWang2023_HubbleTension_Defs

Formal statement

namespace HuWang2023

theorem meanDMIGM_strictMonoOn (A Ωb H0 Ωm : ℝ) (fIGM fe : ℝ → ℝ)
    (hA : 0 < A) (hΩb : 0 < Ωb) (hH0 : 0 < H0) (hΩm0 : 0 ≤ Ωm)
    (hfIGM_cont : ContinuousOn fIGM (Set.Ici 0)) (hfe_cont : ContinuousOn fe (Set.Ici 0))
    (hfIGM_pos : ∀ z, 0 ≤ z → 0 < fIGM z) (hfe_pos : ∀ z, 0 ≤ z → 0 < fe z) :
    StrictMonoOn (meanDMIGM A Ωb H0 Ωm fIGM fe) (Set.Ici 0) := 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 3.4 Fast Radio Burst, p. 6, Eq. (5) and the following paragraph

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. (5): ⟨DMIGM(z)⟩\langle \mathrm{DM_{IGM}}(z)\rangle⟨DMIGM​(z)⟩ is strictly increasing in redshift

Eq. (5): $\langle \mathrm{DM_{IGM}}(z)\rangle$ is strictly increasing in redshift