Enumerations of a finite edge set

Defines edgeSetOrders S, the finite set of duplicate-free lists enumerating a finset of edges, and edgeOrders F, the enumerations of a forest's edge set, with membership, cardinality, and head/tail decomposition lemmas, together with the cube-coordinate parametrization paramsOfOrder sending an ordered simplex parameter list to the corresponding edge-parameter vector. Sums over these orders convert between order-by-order sector contributions and the order-free contribution of a forest in the BKAR forest interpolation formula (see BKAR.Formula).

noncomputable def BKAR.Forest.edgeSetOrders {V : Type u_1} [DecidableEq V] (S : Finset (Edge V)) : Finset (List (Edge V))

All lists enumerating the forest edges exactly once.

Equations

• BKAR.Forest.edgeSetOrders S = S.toList.permutations.toFinset

theorem BKAR.Forest.mem_edgeSetOrders_iff {V : Type u_1} [DecidableEq V] (S : Finset (Edge V)) {order : List (Edge V)} : order ∈ edgeSetOrders S ↔ order.Perm S.toList

theorem BKAR.Forest.mem_edgeSetOrders_iff_toFinset_eq_and_nodup {V : Type u_1} [DecidableEq V] (S : Finset (Edge V)) {order : List (Edge V)} : order ∈ edgeSetOrders S ↔ order.toFinset = S ∧ order.Nodup

theorem BKAR.Forest.toFinset_eq_of_mem_edgeSetOrders {V : Type u_1} [DecidableEq V] {S : Finset (Edge V)} {order : List (Edge V)} (h : order ∈ edgeSetOrders S) : order.toFinset = S

theorem BKAR.Forest.nodup_of_mem_edgeSetOrders {V : Type u_1} [DecidableEq V] {S : Finset (Edge V)} {order : List (Edge V)} (h : order ∈ edgeSetOrders S) : order.Nodup

theorem BKAR.Forest.card_edgeSetOrders {V : Type u_1} [DecidableEq V] (S : Finset (Edge V)) : (edgeSetOrders S).card = S.card.factorial

theorem BKAR.Forest.length_eq_card_of_mem_edgeSetOrders {V : Type u_1} [DecidableEq V] {S : Finset (Edge V)} {order : List (Edge V)} (h : order ∈ edgeSetOrders S) : order.length = S.card

theorem BKAR.Forest.edgeSetOrders_empty {V : Type u_1} [DecidableEq V] : edgeSetOrders ∅ = {[]}

theorem BKAR.Forest.eq_and_tail_eq_nil_of_cons_toFinset_eq_singleton_of_nodup {V : Type u_1} [DecidableEq V] {e a : Edge V} {tail : List (Edge V)} (hset : (e :: tail).toFinset = {a}) (hnodup : (e :: tail).Nodup) : e = a ∧ tail = []

theorem BKAR.Forest.edgeSetOrders_singleton {V : Type u_1} [DecidableEq V] (a : Edge V) : edgeSetOrders {a} = {[a]}

theorem BKAR.Forest.cons_mem_edgeSetOrders_iff {V : Type u_1} [DecidableEq V] (S : Finset (Edge V)) {e : Edge V} {order : List (Edge V)} : e :: order ∈ edgeSetOrders S ↔ e ∈ S ∧ order ∈ edgeSetOrders (S.erase e)

noncomputable def BKAR.Forest.edgeSetOrderTails {V : Type u_1} [DecidableEq V] (S : Finset (Edge V)) : Finset ((_ : ↥S) × List (Edge V))

First-edge/tail-order pairs attached to a finite edge set.

Equations

• BKAR.Forest.edgeSetOrderTails S = S.attach.sigma fun (e : ↥S) => BKAR.Forest.edgeSetOrders (S.erase ↑e)

theorem BKAR.Forest.mem_edgeSetOrderTails_iff {V : Type u_1} [DecidableEq V] (S : Finset (Edge V)) {x : (_ : ↥S) × List (Edge V)} : x ∈ edgeSetOrderTails S ↔ x.snd ∈ edgeSetOrders (S.erase ↑x.fst)

theorem BKAR.Forest.mem_edgeSetOrders_filter_ne_nil_iff_exists_orderTail {V : Type u_1} [DecidableEq V] (S : Finset (Edge V)) {order : List (Edge V)} : order ∈ {order ∈ edgeSetOrders S | order ≠ []} ↔ ∃ x ∈ edgeSetOrderTails S, ↑x.fst :: x.snd = order

def BKAR.Forest.edgeSetOrderTailConsEmbedding {V : Type u_1} (S : Finset (Edge V)) : (_ : ↥S) × List (Edge V) ↪ List (Edge V)

The embedding sending a first-edge/tail-order pair to the consed order.

Equations

• BKAR.Forest.edgeSetOrderTailConsEmbedding S = { toFun := fun (x : (_ : ↥S) × List (BKAR.Edge V)) => ↑x.fst :: x.snd, inj' := ⋯ }

theorem BKAR.Forest.sum_edgeSetOrders_filter_ne_nil_eq_sum_cons {V : Type u_1} [DecidableEq V] {β : Type u_2} [AddCommMonoid β] (S : Finset (Edge V)) (φ : List (Edge V) → β) : ∑ ord ∈ edgeSetOrders S with ord ≠ [], φ ord = ∑ e ∈ S.attach, ∑ ord ∈ edgeSetOrders (S.erase ↑e), φ (↑e :: ord)

theorem BKAR.Forest.edgeSetOrders_filter_ne_nil_eq_self_of_nonempty {V : Type u_1} [DecidableEq V] {S : Finset (Edge V)} (hS : S.Nonempty) : {order ∈ edgeSetOrders S | order ≠ []} = edgeSetOrders S

theorem BKAR.Forest.sum_edgeSetOrders_eq_sum_cons_of_nonempty {V : Type u_1} [DecidableEq V] {β : Type u_2} [AddCommMonoid β] {S : Finset (Edge V)} (hS : S.Nonempty) (φ : List (Edge V) → β) : ∑ order ∈ edgeSetOrders S, φ order = ∑ e ∈ S.attach, ∑ order ∈ edgeSetOrders (S.erase ↑e), φ (↑e :: order)

noncomputable def BKAR.Forest.edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : Finset (List (Edge V))

All linear orderings of the edge set of a forest.

Equations

• F.edgeOrders = BKAR.Forest.edgeSetOrders F.edges

theorem BKAR.Forest.mem_edgeOrders_iff {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} : order ∈ F.edgeOrders ↔ order.Perm F.edges.toList

theorem BKAR.Forest.toList_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : F.edges.toList ∈ F.edgeOrders

theorem BKAR.Forest.mem_edgeOrders_iff_toFinset_eq_and_nodup {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} : order ∈ F.edgeOrders ↔ order.toFinset = F.edges ∧ order.Nodup

theorem BKAR.Forest.toFinset_eq_of_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (h : order ∈ F.edgeOrders) : order.toFinset = F.edges

theorem BKAR.Forest.nodup_of_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (h : order ∈ F.edgeOrders) : order.Nodup

theorem BKAR.Forest.length_eq_card_of_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (h : order ∈ F.edgeOrders) : order.length = F.edges.card

theorem BKAR.Forest.card_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : F.edgeOrders.card = F.edges.card.factorial

theorem BKAR.Forest.empty_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] : (empty V).edgeOrders = {[]}

theorem BKAR.Forest.cons_mem_edgeOrders_iff {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} {order : List (Edge V)} : e :: order ∈ F.edgeOrders ↔ e ∈ F.edges ∧ order ∈ edgeSetOrders (F.edges.erase e)

theorem BKAR.Forest.edgeOrders_filter_ne_nil_eq_self_of_edges_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (hF : F.edges.Nonempty) : {order ∈ F.edgeOrders | order ≠ []} = F.edgeOrders

theorem BKAR.Forest.sum_edgeOrders_eq_sum_cons_of_edges_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] {β : Type u_2} [AddCommMonoid β] (F : Forest V) (hF : F.edges.Nonempty) (φ : List (Edge V) → β) : ∑ order ∈ F.edgeOrders, φ order = ∑ e ∈ F.edges.attach, ∑ order ∈ edgeSetOrders (F.edges.erase ↑e), φ (↑e :: order)

def BKAR.Forest.paramsOfOrder {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) (ts : List ℝ) : F.EdgeParam → ℝ

Read a list of simplex parameters as edge parameters for a forest, according to a chosen edge order. Missing parameters default to zero; on valid orders and simplex-length parameter lists, this default is never used.

Equations

• F.paramsOfOrder order ts e = ts.getD (List.idxOf (↑e) order) 0

theorem BKAR.Forest.paramValue_paramsOfOrder_eq_of_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (F G : Forest V) (hedges : F.edges = G.edges) (order : List (Edge V)) (ts : List ℝ) (e : Edge V) : F.paramValue (F.paramsOfOrder order ts) e = G.paramValue (G.paramsOfOrder order ts) e

theorem BKAR.Forest.standardInterp_paramsOfOrder_eq_of_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (F G : Forest V) (hedges : F.edges = G.edges) (order : List (Edge V)) (ts : List ℝ) : F.standardInterp (F.paramsOfOrder order ts) = G.standardInterp (G.paramsOfOrder order ts)

In a common edge order, paramsOfOrder gives the same standard interpolation point for any two Forest representatives with the same underlying edge set.

theorem BKAR.Forest.paramsOfOrder_empty {V : Type u_1} [Fintype V] [DecidableEq V] (order : List (Edge V)) (ts : List ℝ) : (empty V).paramsOfOrder order ts = emptyParam

theorem BKAR.Forest.paramsOfOrder_cons_self {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (e : Edge V) (order : List (Edge V)) (t : ℝ) (ts : List ℝ) (he : e ∈ F.edges) : F.paramsOfOrder (e :: order) (t :: ts) ⟨e, he⟩ = t

theorem BKAR.Forest.paramsOfOrder_cons_of_ne {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e e' : Edge V} (order : List (Edge V)) (t : ℝ) (ts : List ℝ) (he' : e' ∈ F.edges) (hne : e' ≠ e) : F.paramsOfOrder (e :: order) (t :: ts) ⟨e', he'⟩ = ts.getD (List.idxOf e' order) 0

theorem BKAR.Forest.EdgeExtension.extendParam_eq_paramsOfOrder_cons {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} (h : F.EdgeExtension F' e) (order : List (Edge V)) (ts : List ℝ) (u : F.EdgeParam → ℝ) (t : ℝ) (hu : u = F.paramsOfOrder order ts) : h.extendParam u t = F'.paramsOfOrder (e :: order) (t :: ts)

theorem BKAR.Forest.EdgeExtension.extendParam_empty_eq_paramsOfOrder_singleton {V : Type u_1} [Fintype V] [DecidableEq V] {F' : Forest V} {e : Edge V} (h : (empty V).EdgeExtension F' e) (t : ℝ) : h.extendParam emptyParam t = F'.paramsOfOrder [e] [t]

theorem BKAR.Forest.EdgeExtension.extendParam_eq_paramsOfOrder_append_singleton {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} (h : F.EdgeExtension F' e) (pref : List (Edge V)) (prefixTs : List ℝ) (t : ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) : h.extendParam (F.paramsOfOrder pref prefixTs) t = F'.paramsOfOrder (pref ++ [e]) (prefixTs ++ [t])

Appending one newly-added edge to an existing order is compatible with the recursive one-edge parameter extension.

theorem BKAR.Forest.OrderedGrowth.params_eq_paramsOfOrder_append_of_length {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) {ts : List ℝ} (hlen : ts.length = order.length) : h.params (F.paramsOfOrder pref prefixTs) ts = G.paramsOfOrder (pref ++ order) (prefixTs ++ ts)

If the starting forest parameters are read from an ordered prefix, then an ordered growth reads the combined prefix-plus-growth parameter list in the canonical paramsOfOrder way. The length condition rules out the fallback zeroes used for malformed parameter lists.

theorem BKAR.Forest.OrderedGrowth.params_emptyStart_eq_paramsOfOrder_of_length {V : Type u_1} [Fintype V] [DecidableEq V] {G : Forest V} {order : List (Edge V)} (h : (empty V).OrderedGrowth order G) {ts : List ℝ} (hlen : ts.length = order.length) : h.params emptyParam ts = G.paramsOfOrder order ts

For an ordered growth from the empty forest, the recursive branch parameters are exactly the canonical parameters attached to its terminal edge order.

noncomputable def BKAR.Forest.orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The ordered-simplex contribution attached to one concrete ordering of a forest edge set.

Equations

• F.orderedContribution order ρ = BKAR.orderedSimplexIntegral order fun (ts : List ℝ) => BKAR.mixedPartialList order.reverse ρ (F.standardInterp (F.paramsOfOrder order ts))

theorem BKAR.Forest.orderedContribution_empty {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) : (empty V).orderedContribution [] ρ = ρ zeroConfig

The ordered-simplex contribution of the empty forest.

noncomputable def BKAR.Forest.orderedSectorSum {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The canonical ordered-sector sum attached to a forest. The cube-partition theorem identifies this with the usual cube integral over F.edges.

Equations

• F.orderedSectorSum ρ = ∑ order ∈ F.edgeOrders, F.orderedContribution order ρ

theorem BKAR.Forest.orderedSectorSum_empty {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) : (empty V).orderedSectorSum ρ = ρ zeroConfig

The empty forest contributes exactly the zero-configuration term.

theorem BKAR.Forest.orderedSectorSum_eq_sum_cons_of_edges_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (hF : F.edges.Nonempty) (ρ : (Edge V → ℝ) → ℝ) : F.orderedSectorSum ρ = ∑ e ∈ F.edges.attach, ∑ order ∈ edgeSetOrders (F.edges.erase ↑e), F.orderedContribution (↑e :: order) ρ

For a nonempty forest, the ordered-sector sum splits by first edge and then by an ordering of the remaining edge set.

theorem BKAR.Forest.orderedSectorSum_eq_sum_orderTails_of_edges_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (hF : F.edges.Nonempty) (ρ : (Edge V → ℝ) → ℝ) : F.orderedSectorSum ρ = ∑ x ∈ edgeSetOrderTails F.edges, F.orderedContribution (↑x.fst :: x.snd) ρ

Tail-pair version of Forest.orderedSectorSum_eq_sum_cons_of_edges_nonempty. This is the indexing shape used by recursive branch assembly.

theorem BKAR.Forest.ActiveExtension.singletonGrowth_branchIntegral_empty_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] {e : Edge V} (h : (empty V).ActiveExtension e) (ρ : (Edge V → ℝ) → ℝ) : h.singletonGrowth.branchIntegral emptyParam ρ = h.forest.orderedContribution [e] ρ

The one-edge branch grown from the empty forest is exactly the canonical one-edge ordered-sector contribution for its terminal forest.