Squared quantile transport for dyadic masses

For a dyadic probability mass q, this module proves

∫₀¹ (q.quantile u - u)² du = ∫₀¹ (q.piecewiseCDF z - z)² dz.

The proof keeps track of an affine spatial interval and a cumulative-mass offset. On each leaf it is an elementary polynomial identity. At a branch, the two boundary cubic terms cancel.

theorem FD1D.DyadicMass.quantile_sq_integral_eq_haarL2 {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) : ∫ (u : ℝ) in Set.Icc 0 1, (q.quantile u - u) ^ 2 = haarL2 haarNodeLeft haarNodeWidth q.nodeCoefficient

Exact conditional second moment for any dyadic probability mass.