Branch data over the active edges

Defines ActiveBranchData: for each active edge of a forest, a chosen one-edge active extension together with an ordered tail growth from the extended forest. Its branch integrals aggregate the per-edge remainder terms produced by one round of the expansion step, in the form consumed by the telescoping argument behind the BKAR forest interpolation formula (see BKAR.Formula).

structure BKAR.Forest.ActiveBranchData {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : Type u_1

Branch data chosen independently for each active edge of a forest.

For each active edge, the data consists of a one-edge active extension and an ordered tail growth starting from the extended forest.

• extension (e : ↥F.activeEdges) : F.ActiveExtension ↑e

  The chosen one-edge extension for each active edge.

• order : ↥F.activeEdges → List (Edge V)

  The order of the remaining edges along each chosen branch.

• terminal : ↥F.activeEdges → Forest V

  The final forest of each chosen branch.

• tail (e : ↥F.activeEdges) : (self.extension e).forest.OrderedGrowth (self.order e) (self.terminal e)

  The ordered growth following the chosen first extension of each branch.

def BKAR.Forest.ActiveBranchData.growth {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) : F.OrderedGrowth (↑e :: data.order e) (data.terminal e)

The full ordered branch obtained by prepending the selected active edge.

Equations

• data.growth e = (data.extension e).consGrowth (data.tail e)

noncomputable def BKAR.Forest.ActiveBranchData.branchIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The finite active-edge sum of branch integrals with an explicit top bound.

Equations

• data.branchIntegralAux top u ρ = ∑ e ∈ F.activeEdges.attach, BKAR.Forest.OrderedGrowth.branchIntegralAux top (data.growth e) u ρ

noncomputable def BKAR.Forest.ActiveBranchData.branchIntegral {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The finite active-edge sum of branch integrals over the unit simplex.

Equations

• data.branchIntegral u ρ = data.branchIntegralAux 1 u ρ

def BKAR.Forest.ActiveBranchData.singleton {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) : F.ActiveBranchData

The active-branch data whose selected branch over each active edge stops after the first extension.

Equations

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

theorem BKAR.Forest.ActiveBranchData.growth_eq_consGrowth {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) : data.growth e = (data.extension e).consGrowth (data.tail e)

theorem BKAR.Forest.ActiveBranchData.growth_firstStep {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) : ⋯ = ⋯

theorem BKAR.Forest.ActiveBranchData.growth_tailForest {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) : (data.growth e).tailForest = (data.extension e).forest

theorem BKAR.Forest.ActiveBranchData.growth_tailGrowth {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) : (data.growth e).tailGrowth = data.tail e

theorem BKAR.Forest.ActiveBranchData.growth_firstActiveExtension {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) : (data.growth e).firstActiveExtension = data.extension e

theorem BKAR.Forest.ActiveBranchData.growth_derivativeOrder {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) : (data.growth e).derivativeOrder = (data.order e).reverse ++ [↑e]

theorem BKAR.Forest.ActiveBranchData.growth_branchPoint_first {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) (u : F.EdgeParam → ℝ) (t : ℝ) (ts : List ℝ) : (data.growth e).branchPoint u (t :: ts) ↑e = t

theorem BKAR.Forest.ActiveBranchData.growth_branchPoint_of_initial_mem {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) (u : F.EdgeParam → ℝ) (ts : List ℝ) {e' : Edge V} (he' : e' ∈ F.edges) : (data.growth e).branchPoint u ts e' = u ⟨e', he'⟩

theorem BKAR.Forest.ActiveBranchData.growth_branchIntegralAux_eq_integral_tail_partialDeriv {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : OrderedGrowth.branchIntegralAux top (data.growth e) u ρ = ∫ (t : ℝ) in 0..top, OrderedGrowth.branchIntegralAux t (data.tail e) (⋯.extendParam u t) (partialDeriv (↑e) ρ)

theorem BKAR.Forest.ActiveBranchData.singleton_growth_eq_singletonGrowth {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (e : ↥F.activeEdges) : (singleton extensions).growth e = (extensions e).singletonGrowth

theorem BKAR.Forest.ActiveBranchData.branchIntegral_eq_branchIntegralAux_one {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral u ρ = data.branchIntegralAux 1 u ρ

theorem BKAR.Forest.ActiveBranchData.branchIntegralAux_eq_sum_integrals_tail_partialDeriv {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegralAux top u ρ = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, OrderedGrowth.branchIntegralAux t (data.tail e) (⋯.extendParam u t) (partialDeriv (↑e) ρ)

The finite active-edge branch sum is exactly the sum of the recursive tail integrals obtained after the chosen first active extension.

theorem BKAR.Forest.ActiveBranchData.branchIntegral_eq_sum_integrals_tail_partialDeriv {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral u ρ = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..1, OrderedGrowth.branchIntegralAux t (data.tail e) (⋯.extendParam u t) (partialDeriv (↑e) ρ)

Unit-simplex version of ActiveBranchData.branchIntegralAux_eq_sum_integrals_tail_partialDeriv.

theorem BKAR.Forest.ActiveBranchData.singleton_branchIntegralAux_eq_integralSum_partialDeriv_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) : (singleton extensions).branchIntegralAux top u ρ = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, partialDeriv (↑e) ρ ((extensions e).forest.interpWithFill (⋯.extendParam u t) t)

Terminal singleton branches turn the active-edge branch sum into the sum of one-edge partial-derivative integrals on the terminal fill-parameter interpolations.

theorem BKAR.Forest.ActiveBranchData.growth_branchIntegrand_eq_mixedPartialList_interpWithFill_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (hterm : ∀ (e : ↥F.activeEdges), (data.terminal e).activeEdges = ∅) (e : ↥F.activeEdges) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (ts : List ℝ) (b : ℝ) : (data.growth e).branchIntegrand u ρ ts = mixedPartialList (↑e :: data.order e).reverse ρ ((data.terminal e).interpWithFill ((data.growth e).params u ts) b)

For a terminal selected branch, its integrand may be read on the terminal fill-parameter interpolation point.

theorem BKAR.Forest.ActiveBranchData.growth_branchIntegrand_eq_mixedPartialList_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (e : ↥F.activeEdges) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (ts : List ℝ) : (data.growth e).branchIntegrand u ρ ts = mixedPartialList (↑e :: data.order e).reverse ρ ((data.terminal e).standardInterp ((data.growth e).params u ts))

The selected branch integrand in its standard terminal-interpolation form.

theorem BKAR.Forest.ActiveBranchData.branchIntegralAux_eq_sum_orderedSimplexIntegralAux_mixedPartialList_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegralAux top u ρ = ∑ e ∈ F.activeEdges.attach, orderedSimplexIntegralAux top (↑e :: data.order e) fun (ts : List ℝ) => mixedPartialList (↑e :: data.order e).reverse ρ ((data.terminal e).standardInterp ((data.growth e).params u ts))

The active-branch sum in the standard terminal-interpolation form used by the ordered BKAR main terms.

theorem BKAR.Forest.ActiveBranchData.branchIntegral_eq_sum_orderedSimplexIntegral_mixedPartialList_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral u ρ = ∑ e ∈ F.activeEdges.attach, orderedSimplexIntegral (↑e :: data.order e) fun (ts : List ℝ) => mixedPartialList (↑e :: data.order e).reverse ρ ((data.terminal e).standardInterp ((data.growth e).params u ts))

Unit-simplex version of The standard-interpolation identity for ActiveBranchData.branchIntegralAux.

theorem BKAR.Forest.ActiveBranchData.branchIntegralAux_eq_simplexSum_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveBranchData) (hterm : ∀ (e : ↥F.activeEdges), (data.terminal e).activeEdges = ∅) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (b : ℝ) : data.branchIntegralAux top u ρ = ∑ e ∈ F.activeEdges.attach, orderedSimplexIntegralAux top (↑e :: data.order e) fun (ts : List ℝ) => mixedPartialList (↑e :: data.order e).reverse ρ ((data.terminal e).interpWithFill ((data.growth e).params u ts) b)

Terminal selected branches rewrite the active-branch sum as a sum of ordered simplex integrals over terminal fill-parameter interpolation points.

theorem BKAR.Forest.ActiveBranchData.singleton_branchIntegralAux_eq_integralSum_mixedPartial_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (es : List (Edge V)) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) : (singleton extensions).branchIntegralAux top u (mixedPartialList es ρ) = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, mixedPartialList (↑e :: es) ρ ((extensions e).forest.interpWithFill (⋯.extendParam u t) t)

Accumulated-derivative version of the terminal singleton branch-sum identity.

theorem BKAR.Forest.ActiveBranchData.singleton_branchIntegralAux_eq_standardIntegralSum_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (es : List (Edge V)) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) : (singleton extensions).branchIntegralAux top u (mixedPartialList es ρ) = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, mixedPartialList (↑e :: es) ρ ((extensions e).forest.standardInterp (⋯.extendParam u t))

Terminal singleton branches in the standard terminal-interpolation form.

theorem BKAR.Forest.ActiveBranchData.singleton_branchIntegral_eq_integralSum_mixedPartial_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) : (singleton extensions).branchIntegral u (mixedPartialList es ρ) = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..1, mixedPartialList (↑e :: es) ρ ((extensions e).forest.interpWithFill (⋯.extendParam u t) t)

Unit-simplex version of ActiveBranchData.singleton_branchIntegralAux_eq_integralSum_mixedPartial_of_emptyActiveEdges.

theorem BKAR.Forest.ActiveBranchData.singleton_branchIntegral_eq_integralSum_standardMixedPartial_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) : (singleton extensions).branchIntegral u (mixedPartialList es ρ) = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..1, mixedPartialList (↑e :: es) ρ ((extensions e).forest.standardInterp (⋯.extendParam u t))

Unit-simplex version of ActiveBranchData.singleton_branchIntegralAux_eq_standardIntegralSum_of_emptyActiveEdges.

theorem BKAR.Forest.mixedPartial_eq_standard_add_singletonBranchIntegralAux_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (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) (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) : mixedPartialList es ρ (F.interpWithFill u b) = mixedPartialList es ρ (F.standardInterp u) + (ActiveBranchData.singleton extensions).branchIntegralAux b u (mixedPartialList es ρ)

Terminal active-extension expansion rewritten as a singleton active-branch remainder.

theorem BKAR.Forest.mixedPartial_eq_standard_add_singletonIntegralSum_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (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) (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) : mixedPartialList es ρ (F.interpWithFill u b) = mixedPartialList es ρ (F.standardInterp u) + ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..b, mixedPartialList (↑e :: es) ρ ((extensions e).forest.standardInterp (⋯.extendParam u t))

Terminal active-extension expansion rewritten directly as standard singleton-branch integrals.