Prove2Me

Eq. (6): the weighted bin redshift zˉ\bar z lies within the bin

Proved
HuWang2023.weightedMeanRedshift_mem_Icc

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

cosmologystatistics

Let SS be a nonempty finite set of data points, with redshifts znz_n and nonzero errors σn\sigma_n for n∈Sn\in S. If every znz_n lies in an interval [m,M][m, M], then so does the inverse-variance weighted redshift of Eq. (6):

m≤zˉ=∑n∈Sznσn−2∑n∈Sσn−2≤M.m \le \bar z = \frac{\sum_{n\in S} z_n\sigma_n^{-2}}{\sum_{n\in S}\sigma_n^{-2}} \le M.

This guarantees that the effective redshift assigned to a bin in the binned H0H_0 analysis of Section 5 is a genuine redshift of that bin.

Preamble
import Mathlib
import Definitions.Def_HuWang2023_HubbleTension_Defs
Formal statement
namespace HuWang2023

theorem weightedMeanRedshift_mem_Icc {ι : Type} (s : Finset ι) (z σ : ι → ℝ) (m M : ℝ)
    (hs : s.Nonempty) (hσ : ∀ n ∈ s, σ n ≠ 0) (hz : ∀ n ∈ s, z n ∈ Set.Icc m M) :
    weightedMeanRedshift s z σ ∈ Set.Icc m M := 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. 12, Eq. (6)
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