Canonical forests realizing a support

For each forest index and each enumeration of its edge set, defines the forest grown by following that order through a fixed active-extension choice system (grownForestForSupportOrder), and the canonical representative canonicalGrownForestForSupport obtained from the canonical order of the support. Both carry the support as their edge set, so every abstract forest index acquires a concrete forest realizing it.

noncomputable def BKAR.ForestIndex.canonicalOrder {V : Type u_1} [Fintype V] [DecidableEq V] (I : ForestIndex V) : ↥(Forest.edgeSetOrders I.edges)

The canonical list order of a forest index, obtained from the finite edge-set enumeration. This is a definite support representative; later sector sums may still range over all permutations of the same support.

Equations

• I.canonicalOrder = ⟨I.edges.toList, ⋯⟩

@[simp]

theorem BKAR.ForestIndex.canonicalOrder_val {V : Type u_1} [Fintype V] [DecidableEq V] (I : ForestIndex V) : ↑I.canonicalOrder = I.edges.toList

noncomputable def BKAR.Forest.grownForestForSupportOrder {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) : Forest V

The Forest representative grown by following a canonical order of a forest index from the empty forest through the selected active-extension choices.

Equations

• BKAR.Forest.grownForestForSupportOrder choices I order = Classical.choose ⋯

theorem BKAR.Forest.followOrderOption_grownForestForSupportOrder {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) : followOrderOption choices (empty V) ↑order = some (grownForestForSupportOrder choices I order)

theorem BKAR.Forest.grownForestForSupportOrder_support {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) : (grownForestForSupportOrder choices I order).support = I

theorem BKAR.Forest.grownForestForSupportOrder_edges {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) : (grownForestForSupportOrder choices I order).edges = I.edges

theorem BKAR.Forest.grownForestForSupportOrder_order_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) : ↑order ∈ (grownForestForSupportOrder choices I order).edgeOrders

noncomputable def BKAR.Forest.canonicalGrownForestForSupport {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) : Forest V

The Forest representative grown through the canonical order of the support. This is a fixed representative for the support once an active-extension choice system is fixed.

Equations

• BKAR.Forest.canonicalGrownForestForSupport choices I = BKAR.Forest.grownForestForSupportOrder choices I I.canonicalOrder

theorem BKAR.Forest.canonicalGrownForestForSupport_support {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) : (canonicalGrownForestForSupport choices I).support = I

theorem BKAR.Forest.canonicalGrownForestForSupport_edges {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) : (canonicalGrownForestForSupport choices I).edges = I.edges

theorem BKAR.Forest.canonicalGrownForestForSupport_order_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) {order : List (Edge V)} (horder : order ∈ edgeSetOrders I.edges) : order ∈ (canonicalGrownForestForSupport choices I).edgeOrders

theorem BKAR.Forest.canonicalGrownForestForSupport_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) : (canonicalGrownForestForSupport choices I).edgeOrders = edgeSetOrders I.edges

theorem BKAR.Forest.rootBoundarySupportOrderContribution_eq_grownForestForSupportOrder {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ρ : (Edge V → ℝ) → ℝ) : rootBoundarySupportOrderContribution choices ρ I ↑order = (grownForestForSupportOrder choices I order).orderedContribution (↑order) ρ

Canonical-representative bridge for one support/order sector: the root support fiber is the ordered contribution of the Forest representative grown by following that order.

theorem BKAR.Forest.rootBoundarySupportOrderContribution_eq_grownForestForSupportOrder_of_mem {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) {order : List (Edge V)} (horder : order ∈ edgeSetOrders I.edges) (ρ : (Edge V → ℝ) → ℝ) : rootBoundarySupportOrderContribution choices ρ I order = (grownForestForSupportOrder choices I ⟨order, horder⟩).orderedContribution order ρ

theorem BKAR.Forest.sum_rootBoundarySupportOrderContribution_eq_sum_grownForestForSupportOrder {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : ∑ order ∈ edgeSetOrders I.edges, rootBoundarySupportOrderContribution choices ρ I order = ∑ order ∈ (edgeSetOrders I.edges).attach, (grownForestForSupportOrder choices I order).orderedContribution (↑order) ρ