← Mathematical handbook

The clipped tail corrections beyond the polynomial branch

theorem Verification.noiseMoment_ge_one (d : ℝ) (hd : 1 ≤ d) (k : ℕ) : noiseMoment k d = 1

theorem Verification.noiseMoment_le_neg_one (d : ℝ) (hd : d ≤ -1) (k : ℕ) (hk : k ≠ 0) : noiseMoment k d = 0

theorem Verification.noise_square_full (d : ℝ) : (noiseMoment 2 d + noiseMoment 2 (-d)) / 2 = 1 / 3 + d ^ 2 / 2 - |d| ^ 3 / 3 + max 0 (|d| - 1) ^ 2 * (2 * |d| + 1) / 6

theorem Verification.noise_weighted_full (b x y : ℝ) (hb : 0 ≤ b) : (x * noiseMoment 1 (b * (x - y)) + y * noiseMoment 1 (b * (y - x))) / 2 = (x + y) / 4 + b / 2 * (x - y) ^ 2 - b ^ 2 / 4 * |x - y| ^ 3 + |x - y| * max 0 (b * |x - y| - 1) ^ 2 / 4