Documentation

Copula.Rank.Region.XiBlest.Support.SquaredUniformMoments

← Copula mathematical handbook

Difference moments of two squared uniform variables #

source
theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_square_diff_cube :
∫ (x : ↑unitInterval) (y : ↑unitInterval), |↑x ^ 2 - ↑y ^ 2| ^ 3 = 4 / 35
source
theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_square_diff_sq :
∫ (x : ↑unitInterval) (y : ↑unitInterval), (↑x ^ 2 - ↑y ^ 2) ^ 2 = 8 / 45
source
noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.squarePotential (u : ↑unitInterval) :
ℝ
Equations
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.squareDelta (p : ↑unitInterval × ↑unitInterval) :
    ℝ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.continuous_squarePotential :
      Continuous squarePotential
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.continuous_squareDelta :
      Continuous squareDelta
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.squarePotential_mem (u : ↑unitInterval) :
      squarePotential u ∈ Set.Icc 0 1
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.squareDelta_abs_le (p : ↑unitInterval × ↑unitInterval) :
      |squareDelta p| ≤ 1
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_squareDelta_cube :
      ∫ (p : ↑unitInterval × ↑unitInterval), |squareDelta p| ^ 3 = 4 / 35
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_squareDelta_sq :
      ∫ (p : ↑unitInterval × ↑unitInterval), squareDelta p ^ 2 = 8 / 45
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_squarePotential :
      ∫ (u : ↑unitInterval), squarePotential u = 1 / 3
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_pair_symmetrize (f : ↑unitInterval × ↑unitInterval → ℝ) (hf : Continuous f) :
      ∫ (p : ↑unitInterval × ↑unitInterval), f p = ∫ (p : ↑unitInterval × ↑unitInterval), (f p + f p.swap) / 2