Contributions grouped by support and order

Defines supportContribution and supportOrderContribution, the sums of terminal branch integrals whose growth reaches a prescribed support edge set (and, in the refined version, follows a prescribed order), and proves the regrouping identities expressing the total branch integral from the empty forest as a sum over supports, then over first edge and tail order. This is the combinatorial regrouping behind the sum-over-forests form of the BKAR forest interpolation formula (see BKAR.Formula).

noncomputable def BKAR.Forest.ActiveTerminalBranchData.supportContribution {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : ℝ

Contribution of the selected empty-start terminal branches whose terminal forest has a fixed finite support index.

Equations

• data.supportContribution I ρ = ∑ e ∈ (BKAR.Forest.empty V).activeEdges.attach with (data.growth e).support = I, (data.growth e).terminal.orderedContribution (data.growthOrder e) ρ

theorem BKAR.Forest.ActiveTerminalBranchData.supportContribution_def {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : data.supportContribution I ρ = ∑ e ∈ (empty V).activeEdges.attach with (data.growth e).support = I, (data.growth e).terminal.orderedContribution (data.growthOrder e) ρ

noncomputable def BKAR.Forest.ActiveTerminalBranchData.supportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : ℝ

Contribution of selected empty-start terminal branches with both fixed support and fixed terminal edge order.

Equations

• One or more equations did not get rendered due to their size.

theorem BKAR.Forest.ActiveTerminalBranchData.supportOrderContribution_def {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : data.supportOrderContribution I order ρ = ∑ e ∈ (empty V).activeEdges.attach with (data.growth e).support = I ∧ data.growthOrder e = order, (data.growth e).terminal.orderedContribution order ρ

theorem BKAR.Forest.ActiveTerminalBranchData.branchIntegral_empty_eq_sum_supportContribution {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral emptyParam ρ = ∑ I : ForestIndex V, data.supportContribution I ρ

The selected active-terminal branches from the empty forest can be regrouped by their finite terminal forest support.

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

For selected terminal branches from the empty forest, equality of finite supports is exactly equality of the selected order's edge set.

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

Edge-set form of ActiveTerminalBranchData.supportContribution. This removes the proof-carrying support index from the fiber predicate.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_support_eq_iff_first_mem_and_tail_order_mem_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) (I : ForestIndex V) : (data.growth e).support = I ↔ ↑e ∈ I.edges ∧ (data.tail e).order ∈ edgeSetOrders (I.edges.erase ↑e)

Support equality for a selected terminal branch from the empty forest is equivalent to choosing the first edge in the support and a canonical ordering of the support with that edge erased.

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

First-edge/tail-order form of ActiveTerminalBranchData.supportContribution. This is the support-fiber shape used by the recursive BKAR sector enumeration.

theorem BKAR.Forest.ActiveTerminalBranchData.supportContribution_eq_sum_support_edges_filter_tail_order {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : data.supportContribution I ρ = ∑ e ∈ I.edges.attach with (data.tail (emptyActiveEdge ↑e)).order ∈ edgeSetOrders (I.edges.erase ↑e), (data.growth (emptyActiveEdge ↑e)).terminal.orderedContribution (data.growthOrder (emptyActiveEdge ↑e)) ρ

Support-fiber form indexed directly by first edges in I.edges. Since every edge is active over the empty forest, the ambient active-edge filter can be collapsed to the actual support edge set, with the tail order carrying the remaining fiber predicate.

theorem BKAR.Forest.ActiveTerminalBranchData.supportContribution_eq_sum_support_edges_filter_tail_branchIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : data.supportContribution I ρ = ∑ e ∈ I.edges.attach with (data.tail (emptyActiveEdge ↑e)).order ∈ edgeSetOrders (I.edges.erase ↑e), ∫ (t : ℝ) in 0..1, (data.tail (emptyActiveEdge ↑e)).branchIntegralAux t (⋯.extendParam emptyParam t) (partialDeriv (↑e) ρ)

Recursive support-fiber form: over a fixed support I, each admissible first edge contributes the tail branch integral after that first edge.

theorem BKAR.Forest.ActiveTerminalBranchData.branchIntegral_empty_eq_sum_support_edges_filter_tail_branchIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral emptyParam ρ = ∑ I : ForestIndex V, ∑ e ∈ I.edges.attach with (data.tail (emptyActiveEdge ↑e)).order ∈ edgeSetOrders (I.edges.erase ↑e), ∫ (t : ℝ) in 0..1, (data.tail (emptyActiveEdge ↑e)).branchIntegralAux t (⋯.extendParam emptyParam t) (partialDeriv (↑e) ρ)

Full empty-start recursive form after regrouping by terminal support: the selected terminal branch sum is a support-indexed sum of tail branch integrals.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_first_mem_support_edges_of_support_eq_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) : ↑e ∈ I.edges

The first edge of a selected terminal branch lies in its support fiber.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_tail_order_mem_edgeSetOrders_support_erase_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) : (data.tail e).order ∈ edgeSetOrders (I.edges.erase ↑e)

The tail of a selected terminal branch over support I is a canonical ordering of I.edges with the first edge erased.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_tail_order_length_eq_card_support_erase_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) : (data.tail e).order.length = (I.edges.erase ↑e).card

Over a fixed support fiber, the tail branch has exactly the number of edges left after erasing the selected first edge.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_order_mem_edgeSetOrders_of_support_eq_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) : ↑e :: (data.tail e).order ∈ edgeSetOrders I.edges

A selected terminal branch lying over support I carries a canonical ordering of the edge set I.edges.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_order_length_eq_card_support_edges_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) : (↑e :: (data.tail e).order).length = I.edges.card

The selected first-edge/tail order has length equal to the cardinality of its support edge set.

theorem BKAR.Forest.ActiveTerminalBranchData.growthOrderTail_order_mem_edgeSetOrders_of_support_eq_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) : ↑(data.growthOrderTail e).fst :: (data.growthOrderTail e).snd ∈ edgeSetOrders I.edges

The packaged first-edge/tail sector of a selected terminal branch over I is one of the canonical orderings of I.edges.

theorem BKAR.Forest.ActiveTerminalBranchData.growthOrder_mem_edgeSetOrders_of_support_eq_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) : data.growthOrder e ∈ edgeSetOrders I.edges

The selected terminal order of a branch over support I is one of the canonical orderings of I.edges.

theorem BKAR.Forest.ActiveTerminalBranchData.supportContribution_eq_sum_supportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : data.supportContribution I ρ = ∑ order ∈ edgeSetOrders I.edges, data.supportOrderContribution I order ρ

A support contribution splits further into fixed ordered-sector fibers.

theorem BKAR.Forest.ActiveTerminalBranchData.branchIntegral_empty_eq_sum_supportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral emptyParam ρ = ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, data.supportOrderContribution I order ρ

The full empty-start terminal branch sum is indexed by support and then by one of the canonical ordered sectors of that support.