← Copula mathematical handbook

Inverting the clamped mean on its effective parameter interval

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.clampedMean_strictMonoOn {b : ℝ} (hb : 0 ≤ b) : StrictMonoOn (clampedMean b) (Set.Icc 0 (b + 1))

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.bandIntercept_mem (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : bandIntercept b hb v ∈ Set.Icc 0 (b + 1)

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

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.clampedMeanUnit b a = ⟨ProbabilityTheory.Copula.RankRegion.Common.clampedMean b a, ⋯⟩

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.continuous_clampedMeanUnit (b : ℝ) : Continuous (clampedMeanUnit b)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.bandIntercept_clampedMean (b : ℝ) (hb : 0 ≤ b) {a : ℝ} (ha : a ∈ Set.Icc 0 (b + 1)) : bandIntercept b hb (clampedMeanUnit b a) = a

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.clampedMean_le_iff (b : ℝ) (hb : 0 ≤ b) {a : ℝ} (ha : a ∈ Set.Icc 0 (b + 1)) (v : ↑unitInterval) : clampedMean b a ≤ ↑v ↔ a ≤ bandIntercept b hb v