Documentation

Verification.SquaredUniformMoments

← Mathematical handbook

Difference moments of two squared uniform variables #

theorem Verification.integral_square_diff_cube :

∫ (x : ↑unitInterval) (y : ↑unitInterval), |↑x ^ 2 - ↑y ^ 2| ^ 3 = 4 / 35

theorem Verification.integral_square_diff_sq :

∫ (x : ↑unitInterval) (y : ↑unitInterval), (↑x ^ 2 - ↑y ^ 2) ^ 2 = 8 / 45

noncomputable def Verification.squarePotential (u : ↑unitInterval) :

Equations

Verification.squarePotential u = (1 - ↑u) ^ 2

Instances For

noncomputable def Verification.squareDelta (p : ↑unitInterval × ↑unitInterval) :

Equations

Verification.squareDelta p = Verification.squarePotential p.2 - Verification.squarePotential p.1

Instances For

theorem Verification.continuous_squarePotential :

Continuous squarePotential

theorem Verification.continuous_squareDelta :

Continuous squareDelta

theorem Verification.squarePotential_mem (u : ↑unitInterval) :

squarePotential u ∈ Set.Icc 0 1

theorem Verification.squareDelta_abs_le (p : ↑unitInterval × ↑unitInterval) :

|squareDelta p| ≤ 1

theorem Verification.integral_squareDelta_cube :

∫ (p : ↑unitInterval × ↑unitInterval), |squareDelta p| ^ 3 = 4 / 35

theorem Verification.integral_squareDelta_sq :

∫ (p : ↑unitInterval × ↑unitInterval), squareDelta p ^ 2 = 8 / 45

theorem Verification.integral_squarePotential :

∫ (u : ↑unitInterval), squarePotential u = 1 / 3

theorem Verification.integral_pair_symmetrize (f : ↑unitInterval × ↑unitInterval → ℝ) (hf : Continuous f) :

∫ (p : ↑unitInterval × ↑unitInterval), f p = ∫ (p : ↑unitInterval × ↑unitInterval), (f p + f p.swap) / 2