← Mathematical handbook

Exact tail corrections to both coefficient polynomials

noncomputable def Verification.xiTail (b t : ℝ) : ℝ

Equations

• Verification.xiTail b t = max 0 (b * t - 1) ^ 2 * (2 * b * t + 1)

noncomputable def Verification.nuTail (b t : ℝ) : ℝ

Equations

• Verification.nuTail b t = 3 * t * max 0 (b * t - 1) ^ 2

theorem Verification.continuous_xiTail (b : ℝ) : Continuous (xiTail b)

theorem Verification.continuous_nuTail (b : ℝ) : Continuous (nuTail b)

theorem Verification.integral_noise_square_tail (b : ℝ) (hb : 0 ≤ b) : ∫ (p : ↑unitInterval × ↑unitInterval), noiseMoment 2 (b * squareDelta p) = 1 / 3 + 4 * b ^ 2 / 45 - 4 * b ^ 3 / 105 + (∫ (p : ↑unitInterval × ↑unitInterval), xiTail b |squareDelta p|) / 6

theorem Verification.integral_noise_weighted_tail (b : ℝ) (hb : 0 ≤ b) : ∫ (p : ↑unitInterval × ↑unitInterval), squarePotential p.2 * noiseMoment 1 (b * squareDelta p) = 1 / 6 + 4 * b / 45 - b ^ 2 / 35 + (∫ (p : ↑unitInterval × ↑unitInterval), nuTail b |squareDelta p|) / 12

theorem Verification.quadraticBand_xi_tail (b : ℝ) (hb : 0 ≤ b) : (quadraticBand b hb).chatterjeeXi = 8 * b ^ 2 * (7 - 3 * b) / 105 + ∫ (p : ↑unitInterval × ↑unitInterval), xiTail b |squareDelta p|