LeanPool.ErdosTuzaValtr.Etv.AlphaBeta

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Etv.AlphaBeta.

def Config.Label.IsAlphaCup {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) (a : α) (c : List α) : Prop

A candidate alpha-cup ending at a: in S, strictly sorted, with non-slope edges.

Equations

• l.IsAlphaCup a c = ((c ++ [a]).In S ∧ List.Pairwise (fun (x1 x2 : α) => x1 < x2) (c ++ [a]) ∧ List.IsChain l.Slopeᶜ (c ++ [a]))

theorem Config.Label.alphaCup_is_cup {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) (c : List α) (c_in_S : c.In S) (c_sorted : List.Pairwise (fun (x1 x2 : α) => x1 < x2) c) (c_chain : List.IsChain l.Slopeᶜ c) : C.Cup c

noncomputable def Config.Label.alphaCups' {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) (a : α) : List (List α)

All alpha-cups ending at a, drawn from sublists of the sorted S.

Equations

• l.alphaCups' a = List.filter (fun (b : List α) => decide (l.IsAlphaCup a b)) (S.sort fun (x1 x2 : α) => x1 ≤ x2).sublists

noncomputable def Config.Label.alphaCup' {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) (a : α) : Option (List α)

A longest alpha-cup ending at a, if one exists.

Equations

• l.alphaCup' a = List.argmax List.length (l.alphaCups' a)

theorem Config.Label.alphaCup'_isSome {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) {a : α} (ha : a ∈ S) : (l.alphaCup' a).isSome = true

noncomputable def Config.Label.alpha {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) (a : α) : ℕ

One less than the length of a longest alpha-cup ending at a (zero off S).

Equations

• l.alpha a = if ha : a ∈ S then ((l.alphaCup' a).get ⋯).length else 0

noncomputable def Config.Label.alphaCup {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) {a : α} (ha : a ∈ S) : (c : List α) ×' c.length = l.alpha a + 1 ∧ c.In S ∧ List.Pairwise (fun (x1 x2 : α) => x1 < x2) c ∧ List.IsChain l.Slopeᶜ c ∧ a ∈ c.getLast?

A witnessing alpha-cup of length alpha a + 1 ending at a.

Equations

• l.alphaCup ha = ⋯.mpr (⋯.mpr (⋯.mpr (have h_argmax := ⋯; have c_alpha_cup := ⋯; ⟨(l.alphaCup' a).get ⋯ ++ [a], ⋯⟩)))

theorem Config.Label.cup_length_le_alpha {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) {a : α} {c : List α} (c_in_S : c.In S) (c_sorted : List.Pairwise (fun (x1 x2 : α) => x1 < x2) c) (c_chain : List.IsChain l.Slopeᶜ c) (c_last : a ∈ c.getLast?) : c.length ≤ l.alpha a + 1

theorem Config.Label.add_alpha {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) {a : α} (ha : a ∈ S) {n : ℕ} {c : List α} (c_in_S : c.In S) (c_cup : C.NCup n c) (c_head : a ∈ c.head?) : C.HasNCup (n + l.alpha a) S

def Config.IsBetaCup {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) (a : α) (c : List α) : Prop

A candidate beta-cup ending at a: a cup in S ending at a.

Equations

• C.IsBetaCup S a c = ((c ++ [a]).In S ∧ C.Cup (c ++ [a]))

@[implicit_reducible]

noncomputable instance Config.decidableIsBetaCup {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) (a : α) (c : List α) : Decidable (C.IsBetaCup S a c)

Equations

• C.decidableIsBetaCup S a c = ⋯.mpr inferInstance

noncomputable def Config.betaCups' {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) (a : α) : List (List α)

All beta-cups ending at a, drawn from sublists of the sorted S.

Equations

• C.betaCups' S a = List.filter (fun (b : List α) => decide (C.IsBetaCup S a b)) (S.sort fun (x1 x2 : α) => x1 ≤ x2).sublists

noncomputable def Config.betaCup' {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) (a : α) : Option (List α)

A longest beta-cup ending at a, if one exists.

Equations

• C.betaCup' S a = List.argmax List.length (C.betaCups' S a)

theorem Config.betaCup'_isSome {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) {a : α} (ha : a ∈ S) : (C.betaCup' S a).isSome = true

noncomputable def Config.beta {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) (a : α) : ℕ

One less than the length of a longest beta-cup ending at a (zero off S).

Equations

• C.beta S a = if ha : a ∈ S then ((C.betaCup' S a).get ⋯).length else 0

noncomputable def Config.betaCup {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) {a : α} (ha : a ∈ S) : (c : List α) ×' c.In S ∧ C.NCup (C.beta S a + 1) c ∧ a ∈ c.getLast?

A witnessing beta-cup of length beta a + 1 ending at a.

Equations

• C.betaCup S ha = ⋯.mpr (⋯.mpr (⋯.mpr (have h_argmax := ⋯; have c_beta_cup := ⋯; ⟨(C.betaCup' S a).get ⋯ ++ [a], ⋯⟩)))

theorem Config.has_beta_cup {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) {a : α} (ha : a ∈ S) : C.HasNCup (C.beta S a + 1) S

theorem Config.cup_length_le_beta {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) {a : α} {c : List α} (c_in_S : c.In S) (c_cup : C.Cup c) (c_last : a ∈ c.getLast?) : c.length ≤ C.beta S a + 1

theorem Config.Label.alpha_le_beta {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) {a : α} (ha : a ∈ S) : l.alpha a ≤ C.beta S a

theorem slope_ff_inc_alpha {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} {l : C.Label S} {a b : α} (sab : ¬l.Slope a b) (ha : a ∈ S) (hb : b ∈ S) (a_le_b : a < b) : l.alpha a < l.alpha b

theorem slope_tt_inc_beta {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} {l : C.Label S} {a b : α} (sab : l.Slope a b) (ha : a ∈ S) (hb : b ∈ S) (a_le_b : a < b) : C.beta S a < C.beta S b

theorem Config.alpha_eq_beta_inc {α : Type u_1} [LinearOrder α] (C : Config α) {S : Finset α} {l : C.Label S} {a b : α} (ha : a ∈ S) (hb : b ∈ S) (h : l.alpha a = l.alpha b) : a < b ↔ C.beta S a < C.beta S b

theorem Config.Label.beta_eq_alpha_inc {α : Type u_1} [LinearOrder α] {C : Config α} {S : Finset α} (l : C.Label S) {a b : α} (ha : a ∈ S) (hb : b ∈ S) (h : C.beta S a = C.beta S b) : a < b ↔ l.alpha a < l.alpha b