← Copula mathematical handbook

Inverting the clamped mean on its effective parameter interval

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMean_mem (b a : ℝ) : quadraticMean b a ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMean_strictMonoOn {b : ℝ} (hb : 0 ≤ b) : StrictMonoOn (quadraticMean b) (Set.Icc (-b) 1)

Strictness holds on the entire effective intercept range, including its endpoints.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticIntercept_mem (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : quadraticIntercept b hb v ∈ Set.Icc (-b) 1

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMeanUnit (b a : ℝ) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMeanUnit b a = ⟨ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMean b a, ⋯⟩

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.continuous_quadraticMeanUnit (b : ℝ) : Continuous (quadraticMeanUnit b)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticIntercept_quadraticMean (b : ℝ) (hb : 0 ≤ b) {a : ℝ} (ha : a ∈ Set.Icc (-b) 1) : quadraticIntercept b hb (quadraticMeanUnit b a) = a

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMean_le_iff (b : ℝ) (hb : 0 ≤ b) {a : ℝ} (ha : a ∈ Set.Icc (-b) 1) (v : ↑unitInterval) : quadraticMean b a ≤ ↑v ↔ a ≤ quadraticIntercept b hb v