Vanishing and base cases for support/order contributions

Support/order contributions vanish unless the order enumerates the support; contributions with empty order or empty support degenerate as expected; and one-edge supports are characterized. Together with the unfolding of a nonempty order into an integral of tail branch integrals, these are the boundary cases closing the support/order recursion of the BKAR forest interpolation formula (see BKAR.Formula).

theorem BKAR.Forest.ActiveTerminalBranchData.supportOrderContribution_eq_zero_of_order_not_mem_edgeSetOrders {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) {order : List (Edge V)} (horder : order ∉ edgeSetOrders I.edges) (ρ : (Edge V → ℝ) → ℝ) : data.supportOrderContribution I order ρ = 0

An order outside edgeSetOrders I.edges has no selected branch in the support I fiber.

theorem BKAR.Forest.ActiveTerminalBranchData.supportOrderContribution_nil_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : data.supportOrderContribution I [] ρ = 0

No selected empty-start terminal branch has empty terminal order.

theorem BKAR.Forest.ActiveTerminalBranchData.supportOrderContribution_cons_eq_orderedContribution_of_support_eq_and_tail_eq {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (a : Edge V) (tail : List (Edge V)) (hsupport : (data.growth (emptyActiveEdge a)).support = I) (htail : (data.tail (emptyActiveEdge a)).order = tail) (ρ : (Edge V → ℝ) → ℝ) : data.supportOrderContribution I (a :: tail) ρ = (data.growth (emptyActiveEdge a)).terminal.orderedContribution (a :: tail) ρ

A fixed nonempty ordered sector can only be supplied by the branch whose first edge is the head of that order.

theorem BKAR.Forest.ActiveTerminalBranchData.supportOrderContribution_cons_eq_integral_tail_branchIntegralAux_of_support_eq_and_tail_eq {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (a : Edge V) (tail : List (Edge V)) (hsupport : (data.growth (emptyActiveEdge a)).support = I) (htail : (data.tail (emptyActiveEdge a)).order = tail) (ρ : (Edge V → ℝ) → ℝ) : data.supportOrderContribution I (a :: tail) ρ = ∫ (t : ℝ) in 0..1, (data.tail (emptyActiveEdge a)).branchIntegralAux t (⋯.extendParam emptyParam t) (partialDeriv a ρ)

Recursive form of a fixed nonempty support/order fiber: once the selected branch over the head edge has the requested support and tail order, the fiber is exactly the tail branch integral after the first edge.

theorem BKAR.Forest.ActiveTerminalBranchData.supportOrderContribution_cons_eq_zero_of_support_ne {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (a : Edge V) (tail : List (Edge V)) (hsupport : (data.growth (emptyActiveEdge a)).support ≠ I) (ρ : (Edge V → ℝ) → ℝ) : data.supportOrderContribution I (a :: tail) ρ = 0

If the branch over the head edge does not have support I, then no branch can contribute to the ordered sector a :: tail over I.

theorem BKAR.Forest.ActiveTerminalBranchData.supportOrderContribution_cons_eq_zero_of_tail_ne {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (a : Edge V) (tail : List (Edge V)) (htail : (data.tail (emptyActiveEdge a)).order ≠ tail) (ρ : (Edge V → ℝ) → ℝ) : data.supportOrderContribution I (a :: tail) ρ = 0

If the branch over the head edge has a different tail order, then it does not contribute to the ordered sector a :: tail.

theorem BKAR.Forest.ActiveTerminalBranchData.supportContribution_eq_zero_of_edges_empty {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) {I : ForestIndex V} (hI : I.edges = ∅) (ρ : (Edge V → ℝ) → ℝ) : data.supportContribution I ρ = 0

No selected active-terminal branch from the empty forest has empty terminal support.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_support_eq_singleton_iff_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) (a : Edge V) : (data.growth e).support = ForestIndex.singleton a ↔ ↑e = a ∧ (data.tail e).order = []

A selected terminal branch from the empty forest has singleton support exactly when its first edge is that singleton and its tail order is empty.

theorem BKAR.Forest.ActiveTerminalBranchData.tail_order_eq_nil_iff_growth_support_eq_singleton_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : (data.tail e).order = [] ↔ (data.growth e).support = ForestIndex.singleton ↑e

The tail order is empty exactly when the selected terminal support is the singleton generated by the first edge.

theorem BKAR.Forest.ActiveTerminalBranchData.tail_order_ne_nil_of_growth_support_ne_singleton_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) (hsupport : (data.growth e).support ≠ ForestIndex.singleton ↑e) : (data.tail e).order ≠ []

If the selected terminal support is not the singleton of its first edge, then the branch has a nonempty tail order.

theorem BKAR.Forest.ActiveTerminalBranchData.tail_order_ne_nil_of_one_lt_support_edges_card_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) {I : ForestIndex V} (hsupport : (data.growth e).support = I) (hcard : 1 < I.edges.card) : (data.tail e).order ≠ []

Branches over a support with more than one edge have a genuinely nonempty tail after the first selected edge.

theorem BKAR.Forest.ActiveTerminalBranchData.one_lt_growth_support_edges_card_of_tail_order_ne_nil_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) (htail : (data.tail e).order ≠ []) : 1 < (data.growth e).support.edges.card

Conversely, if the selected empty-start branch has a nonempty tail, its terminal support has at least two edges.

theorem BKAR.Forest.ActiveTerminalBranchData.one_lt_growth_support_edges_card_iff_tail_order_ne_nil_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : 1 < (data.growth e).support.edges.card ↔ (data.tail e).order ≠ []

For selected empty-start terminal branches, higher-support fibers are exactly the branches whose selected tail order is nonempty.

theorem BKAR.Forest.ActiveTerminalBranchData.supportContribution_singleton_eq_sum_first_eq_and_tail_nil {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (a : Edge V) (ρ : (Edge V → ℝ) → ℝ) : data.supportContribution (ForestIndex.singleton a) ρ = ∑ e ∈ (empty V).activeEdges.attach with ↑e = a ∧ (data.tail e).order = [], (data.growth e).terminal.orderedContribution (data.growthOrder e) ρ

Singleton-support terminal branch fibers can be read as the branches with the specified first edge and empty tail order.

theorem BKAR.Forest.ActiveTerminalBranchData.supportContribution_singleton_eq_orderedContribution_of_tail_eq_nil {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (a : Edge V) (htail : (data.tail (emptyActiveEdge a)).order = []) (ρ : (Edge V → ℝ) → ℝ) : data.supportContribution (ForestIndex.singleton a) ρ = (data.growth (emptyActiveEdge a)).terminal.orderedContribution [a] ρ

If the selected branch over a stops after its first edge, the singleton support fiber is exactly its one-edge ordered contribution.

theorem BKAR.Forest.ActiveTerminalBranchData.supportContribution_singleton_eq_zero_of_tail_ne_nil {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (a : Edge V) (htail : (data.tail (emptyActiveEdge a)).order ≠ []) (ρ : (Edge V → ℝ) → ℝ) : data.supportContribution (ForestIndex.singleton a) ρ = 0

If the selected branch over a has a nonempty tail, then it contributes nothing to the singleton support fiber over {a}.

theorem BKAR.Forest.ActiveTerminalBranchData.singleton_branchIntegral_empty_eq_sum_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (extensions : (e : ↥(empty V).activeEdges) → (empty V).ActiveExtension ↑e) (hterm : ∀ (e : ↥(empty V).activeEdges), (extensions e).forest.activeEdges = ∅) (ρ : (Edge V → ℝ) → ℝ) : (singleton extensions hterm).branchIntegral emptyParam ρ = ∑ e ∈ (empty V).activeEdges.attach, (extensions e).forest.orderedContribution [↑e] ρ

For singleton terminal branches from the empty forest, the active-terminal branch sum is a finite sum of canonical one-edge ordered-sector contributions.