Fibers of the boundary tree sum

Defines boundarySupportOrderTreeFiber, the contribution of the boundary tree sum in the fiber over a prescribed final support and order, together with supportOrderPairs and the integrability certificates for these fibers. Vanishing lemmas dispose of fibers whose order is too short or whose node has no active edges. The root fibers assemble into the support/order form of the BKAR forest interpolation formula (see BKAR.Formula).

noncomputable def BKAR.Forest.supportOrderPairs (V : Type u_2) [Fintype V] [DecidableEq V] : Finset ((_ : ForestIndex V) × List (Edge V))

Finite support/order pairs used by the final folded tree sum.

Equations

• BKAR.Forest.supportOrderPairs V = Finset.univ.sigma fun (I : BKAR.ForestIndex V) => BKAR.Forest.edgeSetOrders I.edges

@[irreducible]

noncomputable def BKAR.Forest.boundarySupportOrderTreeFiber {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The folded contribution of the boundary tree lying over one fixed global support/order pair.

Equations

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

theorem BKAR.Forest.boundarySupportOrderTreeFiber_def {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : boundarySupportOrderTreeFiber choices F pref prefixTs top I order ρ = localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ + ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, boundarySupportOrderTreeFiber choices (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t I order ρ

theorem BKAR.Forest.boundarySupportOrderTreeFiber_eq_zero_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) (hF : F.activeEdges = ∅) : boundarySupportOrderTreeFiber choices F pref prefixTs top I order ρ = 0

theorem BKAR.Forest.boundarySupportOrderTreeFiber_eq_zero_of_order_length_le_pref_length {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : F.activeEdges.card ≤ n → order.length ≤ pref.length → boundarySupportOrderTreeFiber choices F pref prefixTs top I order ρ = 0

A support/order fiber is zero once the requested global order is no longer long enough to contain the current prefix plus one more boundary edge.

theorem BKAR.Forest.boundarySupportOrderTreeFiber_empty_order_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : boundarySupportOrderTreeFiber choices (empty V) [] [] 1 I [] ρ = 0

theorem BKAR.Forest.boundarySupportOrderTreeFiber_intervalIntegrable_of_order_length_le_pref_length {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) (hlen : order.length ≤ pref.length) : IntervalIntegrable (fun (t : ℝ) => boundarySupportOrderTreeFiber choices F pref prefixTs t I order ρ) MeasureTheory.volume 0 top

theorem BKAR.Forest.boundarySupportOrderTreeFiber_intervalIntegrable_of_support_edges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) (hI : I.edges = ∅) (horder : order ∈ edgeSetOrders I.edges) : IntervalIntegrable (fun (t : ℝ) => boundarySupportOrderTreeFiber choices F pref prefixTs t I order ρ) MeasureTheory.volume 0 top

def BKAR.Forest.boundarySupportOrderTreeFiberIntegrable {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) : ℕ → (F : Forest V) → List (Edge V) → List ℝ → ℝ → ((Edge V → ℝ) → ℝ) → Prop

Linearity hypotheses needed to commute the finite support/order fiber sum through the recursive child integrals.

Equations

• One or more equations did not get rendered due to their size.
• BKAR.Forest.boundarySupportOrderTreeFiberIntegrable choices 0 x✝⁴ x✝³ x✝² x✝¹ x✝ = True

theorem BKAR.Forest.boundarySupportOrderTreeFiberIntegrable_zero {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : boundarySupportOrderTreeFiberIntegrable choices 0 F pref prefixTs top ρ

theorem BKAR.Forest.boundarySupportOrderTreeFiberIntegrable_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : F.activeEdges = ∅ → boundarySupportOrderTreeFiberIntegrable choices n F pref prefixTs top ρ

def BKAR.Forest.boundarySupportOrderTreeFiberNontrivialIntegrable {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) : ℕ → (F : Forest V) → List (Edge V) → List ℝ → ℝ → ((Edge V → ℝ) → ℝ) → Prop

The genuinely remaining fiber-integrability obligation. It only asks for support/order fibers not already killed by the structural zero lemmas: the target support is nonempty and the target order is strictly longer than the child prefix.

Equations

• One or more equations did not get rendered due to their size.
• BKAR.Forest.boundarySupportOrderTreeFiberNontrivialIntegrable choices 0 x✝⁴ x✝³ x✝² x✝¹ x✝ = True

theorem BKAR.Forest.boundarySupportOrderTreeFiberNontrivialIntegrable_zero {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : boundarySupportOrderTreeFiberNontrivialIntegrable choices 0 F pref prefixTs top ρ

theorem BKAR.Forest.boundarySupportOrderTreeFiberNontrivialIntegrable_of_le {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {m n : ℕ} {F : Forest V} {pref : List (Edge V)} {prefixTs : List ℝ} {top : ℝ} {ρ : (Edge V → ℝ) → ℝ} : m ≤ n → boundarySupportOrderTreeFiberNontrivialIntegrable choices n F pref prefixTs top ρ → boundarySupportOrderTreeFiberNontrivialIntegrable choices m F pref prefixTs top ρ

theorem BKAR.Forest.boundarySupportOrderTreeFiberNontrivialIntegrable.child_activeEdges_card {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (e : ↥F.activeEdges) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hfiber : boundarySupportOrderTreeFiberNontrivialIntegrable choices F.activeEdges.card F pref prefixTs top ρ) {t : ℝ} (ht : t ∈ Set.uIcc 0 top) : boundarySupportOrderTreeFiberNontrivialIntegrable choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

The exact-depth child nontrivial fiber-integrability hypothesis contained in the parent exact-depth hypothesis.

theorem BKAR.Forest.boundarySupportOrderTreeFiberIntegrable_of_nontrivialIntegrable {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : boundarySupportOrderTreeFiberNontrivialIntegrable choices n F pref prefixTs top ρ → boundarySupportOrderTreeFiberIntegrable choices n F pref prefixTs top ρ

theorem BKAR.Forest.localBoundarySupportOrderSum_eq_sum_supportOrderPairs {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : localBoundarySupportOrderSum choices F pref prefixTs top ρ = ∑ x ∈ supportOrderPairs V, localBoundarySupportOrderContribution choices F pref prefixTs top x.fst x.snd ρ

theorem BKAR.Forest.treeContribution_eq_sum_supportOrderPairs_treeFiber_of_activeEdges_card_le {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : F.activeEdges.card ≤ n → boundarySupportOrderTreeFiberIntegrable choices n F pref prefixTs top ρ → boundarySupportOrderTreeContribution choices F pref prefixTs top ρ = ∑ x ∈ supportOrderPairs V, boundarySupportOrderTreeFiber choices F pref prefixTs top x.fst x.snd ρ

The folded boundary tree is the finite sum of its global support/order fibers.

theorem BKAR.Forest.boundarySupportOrderTreeContribution_eq_sum_treeFiber_of_activeEdges_card_le {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hle : F.activeEdges.card ≤ n) (hfiber : boundarySupportOrderTreeFiberIntegrable choices n F pref prefixTs top ρ) : boundarySupportOrderTreeContribution choices F pref prefixTs top ρ = ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, boundarySupportOrderTreeFiber choices F pref prefixTs top I order ρ

noncomputable def BKAR.Forest.rootBoundarySupportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (order : List (Edge V)) : ℝ

The final root support/order contribution: the empty sector contributes ρ zeroConfig, and every nonempty sector is supplied by the folded tree fiber.

Equations

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

theorem BKAR.Forest.rootBoundarySupportOrderContribution_def {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (order : List (Edge V)) : rootBoundarySupportOrderContribution choices ρ I order = (if I.edges = ∅ ∧ order = [] then ρ zeroConfig else 0) + boundarySupportOrderTreeFiber choices (empty V) [] [] 1 I order ρ

theorem BKAR.Forest.rootBoundarySupportOrderContribution_empty_order_eq_zeroConfig {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (hI : I.edges = ∅) : rootBoundarySupportOrderContribution choices ρ I [] = ρ zeroConfig

theorem BKAR.Forest.rootBoundarySupportOrderContribution_eq_zeroConfig_of_edges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (order : List (Edge V)) (hI : I.edges = ∅) (horder : order ∈ edgeSetOrders I.edges) : rootBoundarySupportOrderContribution choices ρ I order = ρ zeroConfig

theorem BKAR.Forest.rootBoundarySupportOrderContribution_eq_treeFiber_of_not_empty_marker {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (order : List (Edge V)) (hmarker : ¬(I.edges = ∅ ∧ order = [])) : rootBoundarySupportOrderContribution choices ρ I order = boundarySupportOrderTreeFiber choices (empty V) [] [] 1 I order ρ

theorem BKAR.Forest.rootBoundarySupportOrderContribution_eq_treeFiber_of_edges_ne_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (order : List (Edge V)) (hI : I.edges ≠ ∅) : rootBoundarySupportOrderContribution choices ρ I order = boundarySupportOrderTreeFiber choices (empty V) [] [] 1 I order ρ

theorem BKAR.Forest.rootBoundarySupportOrderContribution_empty_eq_orderedContribution_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (hI : I.edges = ∅) : rootBoundarySupportOrderContribution choices ρ I [] = (empty V).orderedContribution [] ρ

theorem BKAR.Forest.boundarySupportOrderTreeFiber_empty_singleton_eq_localBoundary {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (a : Edge V) (ρ : (Edge V → ℝ) → ℝ) : boundarySupportOrderTreeFiber choices (empty V) [] [] 1 I [a] ρ = localBoundarySupportOrderContribution choices (empty V) [] [] 1 I [a] ρ

theorem BKAR.Forest.rootBoundarySupportOrderContribution_singleton_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (a : Edge V) (ρ : (Edge V → ℝ) → ℝ) : rootBoundarySupportOrderContribution choices ρ (ForestIndex.singleton a) [a] = (choices (empty V) (emptyActiveEdge a)).forest.orderedContribution [a] ρ

theorem BKAR.Forest.sum_emptySupportOrderMarker {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) : (∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, if I.edges = ∅ ∧ order = [] then ρ zeroConfig else 0) = ρ zeroConfig

theorem BKAR.Forest.sum_rootBoundarySupportOrderContribution_eq_zeroConfig_add_sum_treeFiber {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) : ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, rootBoundarySupportOrderContribution choices ρ I order = ρ zeroConfig + ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, boundarySupportOrderTreeFiber choices (empty V) [] [] 1 I order ρ

theorem BKAR.Forest.sum_rootContribution_eq_zeroConfig_add_sum_treeFiber_filter_edges_ne_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) : ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, rootBoundarySupportOrderContribution choices ρ I order = ρ zeroConfig + ∑ I : ForestIndex V with I.edges ≠ ∅, ∑ order ∈ edgeSetOrders I.edges, boundarySupportOrderTreeFiber choices (empty V) [] [] 1 I order ρ

theorem BKAR.Forest.rho_oneConfig_eq_sum_rootBoundarySupportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) (hfiber : boundarySupportOrderTreeFiberIntegrable choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) : ρ oneConfig = ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, rootBoundarySupportOrderContribution choices ρ I order

Root BKAR identity with the folded boundary tree flattened into the final global support/order sector sum. The empty support/order sector contributes ρ zeroConfig.

theorem BKAR.Forest.oneConfig_eq_zeroConfig_add_nonemptyTreeSum {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) (hfiber : boundarySupportOrderTreeFiberIntegrable choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) : ρ oneConfig = ρ zeroConfig + ∑ I : ForestIndex V with I.edges ≠ ∅, ∑ order ∈ edgeSetOrders I.edges, boundarySupportOrderTreeFiber choices (empty V) [] [] 1 I order ρ

Equivalent final-shaped root identity with the empty support removed from the remaining tree-fiber sum.

theorem BKAR.Forest.oneConfig_eq_zeroConfig_add_nonemptyTreeSum_of_nontrivialIntegrable {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) (hfiber : boundarySupportOrderTreeFiberNontrivialIntegrable choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) : ρ oneConfig = ρ zeroConfig + ∑ I : ForestIndex V with I.edges ≠ ∅, ∑ order ∈ edgeSetOrders I.edges, boundarySupportOrderTreeFiber choices (empty V) [] [] 1 I order ρ

Root identity whose remaining analytic side condition is restricted to the nontrivial support/order fibers.