Telescoping the recursive boundary remainder

Defines the local recursive boundary remainder and the boundary support/order tree contribution, and telescopes: after finitely many regrouping steps — bounded by the number of active edges — the recursive remainder is exhausted, leaving only integrals of boundary tree contributions. This closes the depth induction in the proof of the BKAR forest interpolation formula (see BKAR.Formula).

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

The exact recursive boundary remainder left after one arbitrary-node support/order regrouping step.

Equations

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

theorem BKAR.Forest.localRecursiveBoundaryRemainder_def {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : localRecursiveBoundaryRemainder choices F pref prefixTs top ρ = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, ∑ e' ∈ (choices F e).forest.activeEdges.attach, ∫ (s : ℝ) in 0..t, allBranchesBoundaryExpansion choices (choices (choices F e).forest e').forest.activeEdges.card (choices (choices F e).forest e').forest (pref ++ [↑e] ++ [↑e']) (prefixTs ++ [t] ++ [s]) s ρ

theorem BKAR.Forest.localRecursiveBoundaryRemainder_eq_zero_of_forall_child_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : ∀ (e : ↥F.activeEdges), (choices F e).forest.activeEdges = ∅) : localRecursiveBoundaryRemainder choices F pref prefixTs top ρ = 0

If every first child of a local node is already terminal, the local recursive boundary remainder vanishes.

theorem BKAR.Forest.allBranchesAnalytic.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 → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) {t : ℝ} (ht : t ∈ Set.uIcc 0 top) : allBranchesAnalytic choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

The exact-depth child analytic hypothesis contained in allBranchesAnalytic.

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

The local support/order boundary layer at one recursion node.

Equations

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

theorem BKAR.Forest.localBoundarySupportOrderSum_def {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 ρ = ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ

theorem BKAR.Forest.localBoundarySupportOrderSum_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 : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hF : F.activeEdges = ∅) : localBoundarySupportOrderSum choices F pref prefixTs top ρ = 0

@[irreducible]

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

The exact recursive sum of all support/order boundary layers below a node. This is the invariant that folds the local recursive boundary remainder.

Equations

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

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

theorem BKAR.Forest.boundarySupportOrderTreeContribution_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 : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hF : F.activeEdges = ∅) : boundarySupportOrderTreeContribution choices F pref prefixTs top ρ = 0

theorem BKAR.Forest.recursiveRemainder_eq_childBoundarySum_add_remainder_of_analytic {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hpref : pref.toFinset = F.edges) (hnodup : pref.Nodup) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : localRecursiveBoundaryRemainder choices F pref prefixTs top ρ = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, localBoundarySupportOrderContribution choices (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t I order ρ + localRecursiveBoundaryRemainder choices (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

One telescoping recurrence for the local recursive boundary remainder: each child remainder splits into its local support/order boundary layer plus its own recursive remainder.

theorem BKAR.Forest.recursiveRemainder_eq_sum_integral_treeContribution_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 → pref.toFinset = F.edges → pref.Nodup → allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ → localRecursiveBoundaryRemainder choices F pref prefixTs top ρ = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, boundarySupportOrderTreeContribution choices (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

The local recursive remainder folds into the exact recursive support/order tree contribution below the current node.

theorem BKAR.Forest.firstRecursiveBoundaryRemainder_eq_localRecursiveBoundaryRemainder_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) : firstRecursiveBoundaryRemainder choices ρ = localRecursiveBoundaryRemainder choices (empty V) [] [] 1 ρ

The root recursive remainder is the empty-node instance of the local one.

theorem BKAR.Forest.boundaryExpansion_eq_standard_add_boundarySum_add_remainder {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hpref : pref.toFinset = F.edges) (hnodup : pref.Nodup) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : allBranchesBoundaryExpansion choices F.activeEdges.card F pref prefixTs top ρ = mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs)) + (∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ + localRecursiveBoundaryRemainder choices F pref prefixTs top ρ)

Exact one-step support/order regrouping of the boundary tree at an arbitrary node.

theorem BKAR.Forest.boundaryExpansion_activeEdges_card_eq_standard_add_treeContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hpref : pref.toFinset = F.edges) (hnodup : pref.Nodup) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : allBranchesBoundaryExpansion choices F.activeEdges.card F pref prefixTs top ρ = mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs)) + boundarySupportOrderTreeContribution choices F pref prefixTs top ρ

Exact-depth local boundary expansion with all recursive remainders folded into the support/order tree contribution.

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

Root exact boundary-tree regrouping with the remaining recursive contribution expressed by the local remainder API.

theorem BKAR.Forest.rho_oneConfig_eq_orderedSectorSum_empty_add_boundarySupportOrderTreeContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) : ρ oneConfig = (empty V).orderedSectorSum ρ + boundarySupportOrderTreeContribution choices (empty V) [] [] 1 ρ

Root exact boundary-tree regrouping with the recursive remainder completely folded into the support/order tree contribution.