Branch integrals along ordered growths

For an ordered growth of forests, defines the accumulated derivative order (derivativeOrder), the interpolation point of a branch (branchPoint), the branch integrand obtained by applying the corresponding mixed partials, and the nested branch integrals branchIntegralAux and branchIntegral over the ordered simplex. These are the basic objects manipulated by the recursion proving the BKAR forest interpolation formula (see BKAR.Formula).

def BKAR.Forest.OrderedGrowth.derivativeOrder {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (_h : F.OrderedGrowth order G) : List (Edge V)

Derivative order accumulated by following a growth list from left to right.

The one-step recursion conses each new derivative onto the front, so the final mixed-partial list is the reverse of the growth order.

Equations

• _h.derivativeOrder = order.reverse

noncomputable def BKAR.Forest.OrderedGrowth.branchPoint {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ts : List ℝ) : Edge V → ℝ

The terminal BKAR interpolation point attached to one ordered branch and a list of simplex parameters.

Equations

• h.branchPoint u ts = G.standardInterp (h.params u ts)

noncomputable def BKAR.Forest.OrderedGrowth.branchIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : List ℝ → ℝ

The terminal integrand attached to one ordered forest-growth branch.

Equations

• h.branchIntegrand u ρ ts = BKAR.mixedPartialList h.derivativeOrder ρ (h.branchPoint u ts)

noncomputable def BKAR.Forest.OrderedGrowth.branchIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (top : ℝ) (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The ordered-simplex integral with an explicit outer bound attached to one ordered forest-growth branch.

Equations

• BKAR.Forest.OrderedGrowth.branchIntegralAux top h u ρ = BKAR.orderedSimplexIntegralAux top order (h.branchIntegrand u ρ)

noncomputable def BKAR.Forest.OrderedGrowth.branchIntegral {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The ordered-simplex integral attached to one ordered forest-growth branch.

Equations

• h.branchIntegral u ρ = BKAR.Forest.OrderedGrowth.branchIntegralAux 1 h u ρ

theorem BKAR.Forest.OrderedGrowth.derivativeOrder_def {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) : h.derivativeOrder = order.reverse

theorem BKAR.Forest.OrderedGrowth.branchPoint_def {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ts : List ℝ) : h.branchPoint u ts = G.standardInterp (h.params u ts)

theorem BKAR.Forest.OrderedGrowth.branchPoint_initial {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ts : List ℝ) (e : F.EdgeParam) : h.branchPoint u ts ↑e = u e

A branch point agrees with the starting parameter on every starting edge.

theorem BKAR.Forest.OrderedGrowth.branchPoint_of_initial_mem {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ts : List ℝ) {e : Edge V} (he : e ∈ F.edges) : h.branchPoint u ts e = u ⟨e, he⟩

theorem BKAR.Forest.OrderedGrowth.branchPoint_first {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) (u : F.EdgeParam → ℝ) (t : ℝ) (ts : List ℝ) : h.branchPoint u (t :: ts) e = t

The first edge of a nonempty branch receives the first simplex parameter.

theorem BKAR.Forest.OrderedGrowth.branchPoint_cons_nil {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) (u : F.EdgeParam → ℝ) : (cons step tail).branchPoint u [] = tail.branchPoint (step.extendParam u 0) []

theorem BKAR.Forest.OrderedGrowth.branchPoint_cons_cons {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (t : ℝ) (ts : List ℝ) : (cons step tail).branchPoint u (t :: ts) = tail.branchPoint (step.extendParam u t) ts

theorem BKAR.Forest.OrderedGrowth.branchPoint_mem_Icc {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) {top : ℝ} {ts : List ℝ} (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) (htop : top ≤ 1) (hts : OrderedSimplexParams top ts) (e : Edge V) : 0 ≤ h.branchPoint u ts e ∧ h.branchPoint u ts e ≤ 1

theorem BKAR.Forest.OrderedGrowth.branchPoint_mem_Icc_one {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) {ts : List ℝ} (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) (hts : OrderedSimplexParams 1 ts) (e : Edge V) : 0 ≤ h.branchPoint u ts e ∧ h.branchPoint u ts e ≤ 1

theorem BKAR.Forest.OrderedGrowth.branchPoint_eq_interpWithFill_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ts : List ℝ) (b : ℝ) (hG : G.activeEdges = ∅) : h.branchPoint u ts = G.interpWithFill (h.params u ts) b

theorem BKAR.Forest.OrderedGrowth.branchIntegrand_eq_mixedPartialList_interpWithFill_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (ts : List ℝ) (b : ℝ) (hG : G.activeEdges = ∅) : h.branchIntegrand u ρ ts = mixedPartialList h.derivativeOrder ρ (G.interpWithFill (h.params u ts) b)

theorem BKAR.Forest.OrderedGrowth.derivativeOrder_cons {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) : (cons step tail).derivativeOrder = tail.derivativeOrder ++ [e]

@[simp]

theorem BKAR.Forest.OrderedGrowth.derivativeOrder_nil {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : (nil F).derivativeOrder = []

theorem BKAR.Forest.OrderedGrowth.branchIntegrand_def {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (ts : List ℝ) : h.branchIntegrand u ρ ts = mixedPartialList order.reverse ρ (h.branchPoint u ts)

theorem BKAR.Forest.OrderedGrowth.branchIntegrand_def_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (ts : List ℝ) : h.branchIntegrand u ρ ts = mixedPartialList order.reverse ρ (G.standardInterp (h.params u ts))

theorem BKAR.Forest.OrderedGrowth.branchIntegrand_congr_branchPoint {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u v : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hpoint : ∀ (ts : List ℝ), h.branchPoint u ts = h.branchPoint v ts) : h.branchIntegrand u ρ = h.branchIntegrand v ρ

theorem BKAR.Forest.OrderedGrowth.branchIntegrand_congr {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) {u v : F.EdgeParam → ℝ} {ρ σ : (Edge V → ℝ) → ℝ} (hfg : ∀ (ts : List ℝ), h.branchIntegrand u ρ ts = h.branchIntegrand v σ ts) : h.branchIntegrand u ρ = h.branchIntegrand v σ

@[simp]

theorem BKAR.Forest.OrderedGrowth.branchIntegrand_nil {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (ts : List ℝ) : (nil F).branchIntegrand u ρ ts = ρ (F.standardInterp u)

@[simp]

theorem BKAR.Forest.OrderedGrowth.branchIntegral_nil {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (nil F).branchIntegral u ρ = ρ (F.standardInterp u)

theorem BKAR.Forest.OrderedGrowth.branchIntegrand_cons_cons {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (t : ℝ) (ts : List ℝ) : (cons step tail).branchIntegrand u ρ (t :: ts) = mixedPartialList (e :: order).reverse ρ (G.standardInterp (tail.params (step.extendParam u t) ts))

theorem BKAR.Forest.OrderedGrowth.branchIntegrand_cons_cons_eq_tail_partialDeriv {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (t : ℝ) (ts : List ℝ) : (cons step tail).branchIntegrand u ρ (t :: ts) = tail.branchIntegrand (step.extendParam u t) (partialDeriv e ρ) ts

theorem BKAR.Forest.OrderedGrowth.branchIntegrand_cons_nil_singleton {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} (step : F.EdgeExtension F' e) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (t : ℝ) : (cons step (nil F')).branchIntegrand u ρ [t] = partialDeriv e ρ (F'.standardInterp (step.extendParam u t))

@[simp]

theorem BKAR.Forest.OrderedGrowth.branchIntegralAux_nil {V : Type u_1} [Fintype V] [DecidableEq V] (top : ℝ) (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : branchIntegralAux top (nil F) u ρ = ρ (F.standardInterp u)

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

theorem BKAR.Forest.OrderedGrowth.branchIntegralAux_congr {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (top : ℝ) (h : F.OrderedGrowth order G) {u v : F.EdgeParam → ℝ} {ρ σ : (Edge V → ℝ) → ℝ} (hfg : ∀ (ts : List ℝ), h.branchIntegrand u ρ ts = h.branchIntegrand v σ ts) : branchIntegralAux top h u ρ = branchIntegralAux top h v σ

theorem BKAR.Forest.OrderedGrowth.branchIntegral_congr {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) {u v : F.EdgeParam → ℝ} {ρ σ : (Edge V → ℝ) → ℝ} (hfg : ∀ (ts : List ℝ), h.branchIntegrand u ρ ts = h.branchIntegrand v σ ts) : h.branchIntegral u ρ = h.branchIntegral v σ

theorem BKAR.Forest.OrderedGrowth.branchIntegralAux_congr_branchPoint {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (top : ℝ) (h : F.OrderedGrowth order G) (u v : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hpoint : ∀ (ts : List ℝ), h.branchPoint u ts = h.branchPoint v ts) : branchIntegralAux top h u ρ = branchIntegralAux top h v ρ

theorem BKAR.Forest.OrderedGrowth.branchIntegral_congr_branchPoint {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (u v : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hpoint : ∀ (ts : List ℝ), h.branchPoint u ts = h.branchPoint v ts) : h.branchIntegral u ρ = h.branchIntegral v ρ

theorem BKAR.Forest.OrderedGrowth.branchIntegralAux_cons {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : branchIntegralAux top (cons step tail) u ρ = ∫ (t : ℝ) in 0..top, orderedSimplexIntegralAux t order fun (ts : List ℝ) => (cons step tail).branchIntegrand u ρ (t :: ts)

theorem BKAR.Forest.OrderedGrowth.branchIntegralAux_cons_eq_integral_tail_partialDeriv {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : branchIntegralAux top (cons step tail) u ρ = ∫ (t : ℝ) in 0..top, branchIntegralAux t tail (step.extendParam u t) (partialDeriv e ρ)

theorem BKAR.Forest.OrderedGrowth.branchIntegralAux_cons_nil_eq_integral_partialDeriv_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} (step : F.EdgeExtension F' e) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : branchIntegralAux top (cons step (nil F')) u ρ = ∫ (t : ℝ) in 0..top, partialDeriv e ρ (F'.standardInterp (step.extendParam u t))

theorem BKAR.Forest.OrderedGrowth.branchIntegral_cons {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (cons step tail).branchIntegral u ρ = ∫ (t : ℝ) in 0..1, orderedSimplexIntegralAux t order fun (ts : List ℝ) => (cons step tail).branchIntegrand u ρ (t :: ts)

theorem BKAR.Forest.OrderedGrowth.branchIntegral_cons_eq_integral_tail_partialDeriv {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (cons step tail).branchIntegral u ρ = ∫ (t : ℝ) in 0..1, branchIntegralAux t tail (step.extendParam u t) (partialDeriv e ρ)

theorem BKAR.Forest.OrderedGrowth.branchIntegral_cons_nil_eq_integral_partialDeriv_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} (step : F.EdgeExtension F' e) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) : (cons step (nil F')).branchIntegral u ρ = ∫ (t : ℝ) in 0..1, partialDeriv e ρ (F'.standardInterp (step.extendParam u t))