← Mathematical handbook

Conditional moments along the central-revelation family

theorem Verification.foldKernel_response_square_integral (u : ↑unitInterval) : ∫ (v : ↑unitInterval), foldKernel v u ^ 2 = 1 / 2 - 1 / 4 * ↑u

theorem Verification.partialRevealKernel_response_integral (t u : ↑unitInterval) : ∫ (v : ↑unitInterval), partialRevealKernel t v u = if u ≤ t then 1 - ((1 - ↑t) / 2 + ↑u) else 1 / 2

theorem Verification.partialRevealKernel_response_square_integral (t u : ↑unitInterval) : ∫ (v : ↑unitInterval), partialRevealKernel t v u ^ 2 = if u ≤ t then (1 + ↑t) / 2 - ↑u else 1 / 2 - 1 / 4 * ↑u

theorem Verification.partialReveal_conditionalMean (t : ↑unitInterval) : conditionalMean (partialReveal t) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => if u ≤ t then (1 - ↑t) / 2 + ↑u else 1 / 2