← Mathematical handbook

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

Affine embedding of the unit interval into one partition cell.

Equations

• Verification.partitionEmbed P i u = ⟨↑(P.point i.castSucc) + P.width i * ↑u, ⋯⟩

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

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

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

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