← Copula mathematical handbook

Moving a constrained quadratic to the boundary of the simplex

This is the boundary reduction in Schreyer–Paulin–Trutschnig, Lemma 4.7. The interval endpoint is constructed from a minimum over the negative coordinates of a nonzero direction.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.exists_positive_boundary_step {ι : Type u_1} [Fintype ι] (u δ : ι → ℝ) (hu : ∀ (i : ι), 0 < u i) (hδ : ∑ i : ι, δ i = 0) (hne : ∃ (i : ι), δ i ≠ 0) : ∃ (t : ℝ), 0 < t ∧ (∀ (i : ι), 0 ≤ u i + t * δ i) ∧ ∃ (i : ι), u i + t * δ i = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.exists_quadratic_boundary_step {ι : Type u_1} [Fintype ι] (u δ : ι → ℝ) (hu : ∀ (i : ι), 0 < u i) (hδ : ∑ i : ι, δ i = 0) (hne : ∃ (i : ι), δ i ≠ 0) (b₁ b₂ : ℝ) (hb₂ : b₂ ≤ 0) : ∃ (t : ℝ), t ≠ 0 ∧ (∀ (i : ι), 0 ≤ u i + t * δ i) ∧ (∃ (i : ι), u i + t * δ i = 0) ∧ b₁ * t + b₂ * t ^ 2 ≤ 0

The sign of the linear term selects one of the two endpoints.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.exists_three_direction (a b c : ℝ) : ∃ (x : ℝ) (y : ℝ) (z : ℝ), (x ≠ 0 ∨ y ≠ 0 ∨ z ≠ 0) ∧ x + y + z = 0 ∧ a * x + b * y + c * z = 0

Two linear constraints on three coordinates always admit a nonzero direction.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.exists_four_direction (a b c d : ℝ) : ∃ (x : ℝ) (y : ℝ), (x ≠ 0 ∨ y ≠ 0) ∧ (a - b) * x + (c - d) * y = 0

Three linear constraints on the four coordinates of a 3412 pattern.