← Copula mathematical handbook

def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionEmbed {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) : ↑unitInterval

Affine embedding of the unit interval into one partition cell.

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionEmbed P i u = ⟨↑(P.point i.castSucc) + P.width i * ↑u, ⋯⟩

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionEmbed_continuous {n : ℕ} (P : IntervalPartition n) (i : Fin n) : Continuous (partitionEmbed P i)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionEmbed_lower {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) : P.point i.castSucc ≤ partitionEmbed P i u

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionEmbed_upper {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) : partitionEmbed P i u ≤ P.point i.succ

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionEmbed_le_iff {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u v : ↑unitInterval) (hv : P.point i.castSucc ≤ v) : partitionEmbed P i u ≤ v ↔ u ≤ P.coord i v