Terminal growths

Packages a terminal ordered growth (TerminalGrowth): an ordered branch starting from a given forest together with the certificate that its final forest has no active edges left. Defines its branch integrals and the constructors (ofActiveEdgesEqEmpty, cons) and unfolding lemmas used to run the recursion behind the BKAR forest interpolation formula (see BKAR.Formula) to completion.

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

A terminal ordered growth from a starting forest.

This packages one ordered branch together with the certificate that its final forest has no active edges left.

• order : List (Edge V)

  The list of edges adjoined along the terminal branch.

• terminal : Forest V

  The final forest, which has no active edges.

• growth : F.OrderedGrowth self.order self.terminal

  The ordered sequence of extensions reaching the terminal forest.

• terminal_activeEdges_eq_empty : self.terminal.activeEdges = ∅

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

The ordered branch integral with an explicit outer bound.

Equations

• data.branchIntegralAux top u ρ = BKAR.Forest.OrderedGrowth.branchIntegralAux top data.growth u ρ

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

The ordered branch integral over the unit simplex.

Equations

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

def BKAR.Forest.TerminalGrowth.ofActiveEdgesEqEmpty {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (hF : F.activeEdges = ∅) : F.TerminalGrowth

The empty terminal branch attached to a forest with no active edges.

Equations

• BKAR.Forest.TerminalGrowth.ofActiveEdgesEqEmpty F hF = { order := [], terminal := F, growth := BKAR.Forest.OrderedGrowth.nil F, terminal_activeEdges_eq_empty := hF }

def BKAR.Forest.TerminalGrowth.cons {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (tail : h.forest.TerminalGrowth) : F.TerminalGrowth

Prepend a chosen active extension to a terminal branch from the extended forest.

Equations

• BKAR.Forest.TerminalGrowth.cons h tail = { order := e :: tail.order, terminal := tail.terminal, growth := h.consGrowth tail.growth, terminal_activeEdges_eq_empty := ⋯ }

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

theorem BKAR.Forest.TerminalGrowth.ofActiveEdgesEqEmpty_branchIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (hF : F.activeEdges = ∅) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (ofActiveEdgesEqEmpty F hF).branchIntegralAux top u ρ = ρ (F.standardInterp u)

theorem BKAR.Forest.TerminalGrowth.ofActiveEdgesEqEmpty_branchIntegral {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (hF : F.activeEdges = ∅) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (ofActiveEdgesEqEmpty F hF).branchIntegral u ρ = ρ (F.standardInterp u)

theorem BKAR.Forest.TerminalGrowth.cons_order {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (tail : h.forest.TerminalGrowth) : (cons h tail).order = e :: tail.order

theorem BKAR.Forest.TerminalGrowth.cons_terminal {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (tail : h.forest.TerminalGrowth) : (cons h tail).terminal = tail.terminal

theorem BKAR.Forest.TerminalGrowth.cons_growth {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (tail : h.forest.TerminalGrowth) : (cons h tail).growth = h.consGrowth tail.growth

theorem BKAR.Forest.TerminalGrowth.growth_derivativeOrder {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : data.growth.derivativeOrder = data.order.reverse

theorem BKAR.Forest.TerminalGrowth.edges_eq_toFinset_union {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : data.terminal.edges = data.order.toFinset ∪ F.edges

def BKAR.Forest.TerminalGrowth.support {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : ForestIndex V

The finite forest index grown by a terminal branch.

Equations

• data.support = data.terminal.support

theorem BKAR.Forest.TerminalGrowth.support_edges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : data.support.edges = data.terminal.edges

theorem BKAR.Forest.TerminalGrowth.support_edges_eq_toFinset_union {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : data.support.edges = data.order.toFinset ∪ F.edges

theorem BKAR.Forest.TerminalGrowth.terminal_eq_initial_of_order_eq_nil {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (horder : data.order = []) : data.terminal = F

If a terminal branch carries no growth order, its terminal forest is the initial forest.

theorem BKAR.Forest.TerminalGrowth.support_eq_initial_support_of_order_eq_nil {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (horder : data.order = []) : data.support = F.support

If a terminal branch carries no growth order, its support is the support of the initial forest.

theorem BKAR.Forest.TerminalGrowth.branchIntegralAux_eq_standardInterp_of_order_eq_nil {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (horder : data.order = []) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegralAux top u ρ = ρ (F.standardInterp u)

The branch integral of a terminal growth with empty order is just evaluation at the initial standard interpolation point.

theorem BKAR.Forest.TerminalGrowth.branchIntegral_eq_standardInterp_of_order_eq_nil {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (horder : data.order = []) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral u ρ = ρ (F.standardInterp u)

theorem BKAR.Forest.TerminalGrowth.edges_eq_toFinset_of_initial_edges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (hF : F.edges = ∅) : data.terminal.edges = data.order.toFinset

theorem BKAR.Forest.TerminalGrowth.support_edges_eq_toFinset_of_initial_edges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (hF : F.edges = ∅) : data.support.edges = data.order.toFinset

theorem BKAR.Forest.TerminalGrowth.terminal_edges_eq_toFinset_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).TerminalGrowth) : data.terminal.edges = data.order.toFinset

theorem BKAR.Forest.TerminalGrowth.support_edges_eq_toFinset_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).TerminalGrowth) : data.support.edges = data.order.toFinset

theorem BKAR.Forest.TerminalGrowth.order_toFinset_subset_edges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : data.order.toFinset ⊆ data.terminal.edges

theorem BKAR.Forest.TerminalGrowth.initial_edges_subset_edges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : F.edges ⊆ data.terminal.edges

theorem BKAR.Forest.TerminalGrowth.mem_edges_of_mem_order {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) {e : Edge V} (he : e ∈ data.order) : e ∈ data.terminal.edges

theorem BKAR.Forest.TerminalGrowth.order_toFinset_disjoint_initial_edges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : Disjoint data.order.toFinset F.edges

theorem BKAR.Forest.TerminalGrowth.order_nodup {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : data.order.Nodup

theorem BKAR.Forest.TerminalGrowth.order_toFinset_card_eq_length {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : data.order.toFinset.card = data.order.length

theorem BKAR.Forest.TerminalGrowth.card_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) : data.terminal.edges.card = F.edges.card + data.order.length

theorem BKAR.Forest.TerminalGrowth.cons_branchIntegralAux_eq_integral_tail_partialDeriv {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (tail : h.forest.TerminalGrowth) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (cons h tail).branchIntegralAux top u ρ = ∫ (t : ℝ) in 0..top, tail.branchIntegralAux t (⋯.extendParam u t) (partialDeriv e ρ)

The recursive form of a terminal branch obtained by prepending one active extension.

theorem BKAR.Forest.TerminalGrowth.cons_branchIntegral_eq_integral_tail_partialDeriv {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (tail : h.forest.TerminalGrowth) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (cons h tail).branchIntegral u ρ = ∫ (t : ℝ) in 0..1, tail.branchIntegralAux t (⋯.extendParam u t) (partialDeriv e ρ)

Unit-simplex recursive form of TerminalGrowth.cons_branchIntegralAux_eq_integral_tail_partialDeriv.

theorem BKAR.Forest.TerminalGrowth.branchIntegralAux_eq_orderedSimplexIntegralAux_mixedPartialList_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegralAux top u ρ = orderedSimplexIntegralAux top data.order fun (ts : List ℝ) => mixedPartialList data.order.reverse ρ (data.terminal.standardInterp (data.growth.params u ts))

A terminal branch integral in the standard interpolation form used by BKAR main terms.

theorem BKAR.Forest.TerminalGrowth.branchIntegral_eq_orderedSimplexIntegral_mixedPartialList_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral u ρ = orderedSimplexIntegral data.order fun (ts : List ℝ) => mixedPartialList data.order.reverse ρ (data.terminal.standardInterp (data.growth.params u ts))

Unit-simplex version of TerminalGrowth.branchIntegralAux_eq_orderedSimplexIntegralAux_mixedPartialList_standardInterp.

theorem BKAR.Forest.TerminalGrowth.branchIntegral_emptyStart_eq_orderedSimplexIntegral_mixedPartialList_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).TerminalGrowth) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral emptyParam ρ = orderedSimplexIntegral data.order fun (ts : List ℝ) => mixedPartialList data.order.reverse ρ (data.terminal.standardInterp (data.growth.params emptyParam ts))

theorem BKAR.Forest.TerminalGrowth.branchIntegralAux_eq_orderedSimplexIntegralAux_mixedPartialList_interpWithFill {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (b : ℝ) : data.branchIntegralAux top u ρ = orderedSimplexIntegralAux top data.order fun (ts : List ℝ) => mixedPartialList data.order.reverse ρ (data.terminal.interpWithFill (data.growth.params u ts) b)

The same terminal branch integral, with the final standard interpolation expressed as the terminal fill-parameter interpolation.

theorem BKAR.Forest.TerminalGrowth.branchIntegral_eq_orderedSimplexIntegral_mixedPartialList_interpWithFill {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (b : ℝ) : data.branchIntegral u ρ = orderedSimplexIntegral data.order fun (ts : List ℝ) => mixedPartialList data.order.reverse ρ (data.terminal.interpWithFill (data.growth.params u ts) b)

Unit-simplex version of TerminalGrowth.branchIntegralAux_eq_orderedSimplexIntegralAux_mixedPartialList_interpWithFill.

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

Terminal branch data chosen independently for each active edge of a forest.

For each active edge, this chooses a one-edge active extension and a terminal ordered tail branch from the extended forest.

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

  The first extension chosen for each active edge.

• tail (e : ↥F.activeEdges) : (self.extension e).forest.TerminalGrowth

  The terminal ordered branch following each chosen first extension.

def BKAR.Forest.ActiveTerminalBranchData.branchData {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) : F.ActiveBranchData

Forget terminality, retaining the active-branch data underneath.

Equations

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

def BKAR.Forest.ActiveTerminalBranchData.growth {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) : F.TerminalGrowth

The full terminal branch selected over one active edge.

Equations

• data.growth e = BKAR.Forest.TerminalGrowth.cons (data.extension e) (data.tail e)

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

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

Equations

• data.branchIntegralAux top u ρ = data.branchData.branchIntegralAux top u ρ

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

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

Equations

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

def BKAR.Forest.ActiveTerminalBranchData.singleton {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) : F.ActiveTerminalBranchData

The active-terminal 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.ActiveTerminalBranchData.branchData_terminal_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) : (data.branchData.terminal e).activeEdges = ∅

theorem BKAR.Forest.ActiveTerminalBranchData.singleton_branchData {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) : (singleton extensions hterm).branchData = ActiveBranchData.singleton extensions

theorem BKAR.Forest.ActiveTerminalBranchData.branchData_growth {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) : data.branchData.growth e = (data.growth e).growth

theorem BKAR.Forest.ActiveTerminalBranchData.growth_order {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) : (data.growth e).order = ↑e :: (data.tail e).order

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

theorem BKAR.Forest.ActiveTerminalBranchData.growth_support_eq_extension_support_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 = []) : (data.growth e).support = (data.extension e).forest.support

If the selected tail after an active edge has empty order, then the full branch support is just the support of the one-edge extension.

theorem BKAR.Forest.ActiveTerminalBranchData.extension_activeEdges_eq_empty_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 = []) : (data.extension e).forest.activeEdges = ∅

If the selected tail after an active edge has empty order, terminality of the tail says that the one-edge extension is already terminal.

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

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

theorem BKAR.Forest.ActiveTerminalBranchData.growth_edges_eq_toFinset_union {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) : (data.growth e).terminal.edges = (↑e :: (data.tail e).order).toFinset ∪ F.edges

theorem BKAR.Forest.ActiveTerminalBranchData.growth_support_edges_eq_toFinset_union {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) : (data.growth e).support.edges = (↑e :: (data.tail e).order).toFinset ∪ F.edges

theorem BKAR.Forest.ActiveTerminalBranchData.growth_order_nodup {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) : (↑e :: (data.tail e).order).Nodup

theorem BKAR.Forest.ActiveTerminalBranchData.growth_card_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (e : ↥F.activeEdges) : (data.growth e).terminal.edges.card = F.edges.card + (↑e :: (data.tail e).order).length

theorem BKAR.Forest.ActiveTerminalBranchData.singleton_growth_growth_eq_singletonGrowth {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) (e : ↥F.activeEdges) : ((singleton extensions hterm).growth e).growth = (extensions e).singletonGrowth

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

theorem BKAR.Forest.ActiveTerminalBranchData.singleton_branchIntegralAux_eq_activeBranchData_singleton {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (singleton extensions hterm).branchIntegralAux top u ρ = (ActiveBranchData.singleton extensions).branchIntegralAux top u ρ

theorem BKAR.Forest.ActiveTerminalBranchData.singleton_branchIntegral_eq_activeBranchData_singleton {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (singleton extensions hterm).branchIntegral u ρ = (ActiveBranchData.singleton extensions).branchIntegral u ρ

theorem BKAR.Forest.ActiveTerminalBranchData.branchIntegralAux_eq_sum_growth_branchIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegralAux top u ρ = ∑ e ∈ F.activeEdges.attach, (data.growth e).branchIntegralAux top u ρ

The active-terminal branch sum is the sum of the selected full terminal branch integrals.

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

Recursive form of the active-terminal branch sum after the first active edge.

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

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

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

Terminal fill-parameter form of the active-terminal branch sum.

theorem BKAR.Forest.ActiveTerminalBranchData.singleton_branchIntegralAux_eq_sum_integrals_mixedPartialList_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) (hterm : ∀ (e : ↥F.activeEdges), (extensions e).forest.activeEdges = ∅) (es : List (Edge V)) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (singleton extensions hterm).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 active-terminal branches in the standard terminal-interpolation form.

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

Terminal singleton active-terminal branches in the terminal fill-parameter form.

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

Unit-simplex standard-interpolation version of The standard-interpolation identity for ActiveTerminalBranchData.singleton_branchIntegralAux.