The local recursion step

One step of the recursion at a fixed node: the branch integral unfolds into a sum over active one-edge extensions plus local first-tail remainders (localFirstTailRemainder), and the mixed-partial value at the current interpolation point splits accordingly. Iterating this step generates the all-branches expansion behind the BKAR forest interpolation formula (see BKAR.Formula).

noncomputable def BKAR.Forest.ActiveTerminalBranchData.localFirstTailRemainder {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) (top : ℝ) (u : F.EdgeParam → ℝ) (es : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : ℝ

Local tail error for one selected terminal branch.

At a general recursion node, the selected terminal tail integral can be compared to the one-step active-extension integral. The difference is the piece that remains to be expanded by the all-branches induction.

Equations

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

theorem BKAR.Forest.ActiveTerminalBranchData.localFirstTailRemainder_def {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) (top : ℝ) (u : F.EdgeParam → ℝ) (es : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : data.localFirstTailRemainder e top u es ρ = (∫ (t : ℝ) in 0..top, (data.tail e).branchIntegralAux t (⋯.extendParam u t) (partialDeriv (↑e) (mixedPartialList es ρ))) - ∫ (t : ℝ) in 0..top, mixedPartialList (↑e :: es) ρ ((data.extension e).forest.interpWithFill (⋯.extendParam u t) t)

theorem BKAR.Forest.ActiveTerminalBranchData.branchIntegralAux_eq_sum_activeExtension_integrals_add_sum_localFirstTailRemainder {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (top : ℝ) (u : F.EdgeParam → ℝ) (es : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegralAux top u (mixedPartialList es ρ) = (∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, mixedPartialList (↑e :: es) ρ ((data.extension e).forest.interpWithFill (⋯.extendParam u t) t)) + ∑ e ∈ F.activeEdges.attach, data.localFirstTailRemainder e top u es ρ

The selected terminal branch sum at a local recursion node is the one-step active-extension remainder plus the sum of the local first-tail errors.

theorem BKAR.Forest.ActiveTerminalBranchData.mixedPartial_eq_standard_add_branchIntegralAux_sub_sum_tailRemainder {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (b : ℝ) (hbound : ∀ t ∈ Set.uIcc 0 b, ∀ (e : F.EdgeParam), t ≤ u e) (hρ : ∀ t ∈ Set.uIcc 0 b, DifferentiableAt ℝ (mixedPartialList es ρ) (F.interpWithFill u t)) (hint : ∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => mixedPartialList (e :: es) ρ (F.interpWithFill u t)) MeasureTheory.volume 0 b) : mixedPartialList es ρ (F.interpWithFill u b) = mixedPartialList es ρ (F.standardInterp u) + data.branchIntegralAux b u (mixedPartialList es ρ) - ∑ e ∈ F.activeEdges.attach, data.localFirstTailRemainder e b u es ρ

Local selected-terminal recursion. Starting from any forest and accumulated derivative list, one FTC layer contributes the selected terminal branch sum and leaves exactly the local first-tail errors.

theorem BKAR.Forest.ActiveTerminalBranchData.mixedPartial_eq_standard_add_prefixedSimplexSum_sub_sum_tailRemainder {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (ρ : (Edge V → ℝ) → ℝ) (b : ℝ) (hbound : ∀ t ∈ Set.uIcc 0 b, ∀ (e : F.EdgeParam), t ≤ F.paramsOfOrder pref prefixTs e) (hρ : ∀ t ∈ Set.uIcc 0 b, DifferentiableAt ℝ (mixedPartialList pref.reverse ρ) (F.interpWithFill (F.paramsOfOrder pref prefixTs) t)) (hint : ∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => mixedPartialList (e :: pref.reverse) ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) t)) MeasureTheory.volume 0 b) : mixedPartialList pref.reverse ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) b) = (mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs)) + ∑ e ∈ F.activeEdges.attach, orderedSimplexIntegralAux b (data.growth e).order fun (ts : List ℝ) => mixedPartialList (pref ++ (data.growth e).order).reverse ρ ((data.growth e).terminal.standardInterp ((data.growth e).terminal.paramsOfOrder (pref ++ (data.growth e).order) (prefixTs ++ ts)))) - ∑ e ∈ F.activeEdges.attach, data.localFirstTailRemainder e b (F.paramsOfOrder pref prefixTs) pref.reverse ρ

Prefixed sector form of the local selected-terminal recursion. This is the shape needed by the finishing induction: selected terminal branches are already expressed using the accumulated edge order pref.

theorem BKAR.Forest.ActiveTerminalBranchData.localFirstTailRemainder_eq_zero_of_tail_order_eq_nil {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) (htail : (data.tail e).order = []) (top : ℝ) (u : F.EdgeParam → ℝ) (es : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : data.localFirstTailRemainder e top u es ρ = 0

A local first-tail error vanishes when the selected tail stops immediately.

theorem BKAR.Forest.ActiveTerminalBranchData.branchIntegralAux_eq_sum_activeExtension_integrals_of_forall_tail_order_eq_nil {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (htail : ∀ (e : ↥F.activeEdges), (data.tail e).order = []) (top : ℝ) (u : F.EdgeParam → ℝ) (es : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegralAux top u (mixedPartialList es ρ) = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, mixedPartialList (↑e :: es) ρ ((data.extension e).forest.interpWithFill (⋯.extendParam u t) t)

If every selected tail stops immediately, the local selected-terminal branch sum is exactly the one-step active-extension remainder.