← Copula mathematical handbook

Pattern avoidance in the permutation reduction

The non-endpoint case of Schreyer–Paulin–Trutschnig, Lemma 4.9. The two excluded patterns are 123 and 3412.

def ProbabilityTheory.Copula.RankRegion.RhoTau.NoIncreasingTriple {n : ℕ} (π : Equiv.Perm (Fin n)) : Prop

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.NoIncreasingTriple π = ∀ (i j k : Fin n), i < j → j < k → ¬(π i < π j ∧ π j < π k)

def ProbabilityTheory.Copula.RankRegion.RhoTau.No3412 {n : ℕ} (π : Equiv.Perm (Fin n)) : Prop

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.No3412 π = ∀ (i j k l : Fin n), i < j → j < k → k < l → ¬(π k < π l ∧ π l < π i ∧ π i < π j)

def ProbabilityTheory.Copula.RankRegion.RhoTau.TwoDecreasingBlocks {n : ℕ} (π : Equiv.Perm (Fin n)) : Prop

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.TwoDecreasingBlocks π = ∃ (c : Fin n), ∀ (i j : Fin n), i < j → j ≤ c ∨ c < i → π j < π i

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.NoIncreasingTriple.inverse {n : ℕ} {π : Equiv.Perm (Fin n)} (h : NoIncreasingTriple π) : NoIncreasingTriple (Equiv.symm π)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.min_before_max_blocks {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (h : NoIncreasingTriple π) (horder : (Equiv.symm π) 0 < (Equiv.symm π) (Fin.last (n + 1))) : TwoDecreasingBlocks π

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.avoiding_patterns_blocks {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (h123 : NoIncreasingTriple π) (h3412 : No3412 π) (hfirst : π 0 ≠ Fin.last (n + 1)) (hlast : π (Fin.last (n + 1)) ≠ 0) : TwoDecreasingBlocks π ∨ TwoDecreasingBlocks (Equiv.symm π)

Unless an endpoint can be stripped off, the permutation or its inverse splits into two decreasing blocks.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.extrema_orientation {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (h3412 : No3412 π) (hfirst : π 0 ≠ Fin.last (n + 1)) (hlast : π (Fin.last (n + 1)) ≠ 0) : (Equiv.symm π) 0 < (Equiv.symm π) (Fin.last (n + 1)) ∨ π 0 < π (Fin.last (n + 1))

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.extremal_entries_adjacent {n : ℕ} (π : Equiv.Perm (Fin (n + 2))) (h : NoIncreasingTriple π) (ho : (Equiv.symm π) 0 < (Equiv.symm π) (Fin.last (n + 1))) : ↑((Equiv.symm π) (Fin.last (n + 1))) = ↑((Equiv.symm π) 0) + 1