Prepending an active extension to an ordered growth

The recursion step on growth certificates: consGrowth prepends a chosen active extension to an ordered growth of the extended forest, and the accompanying lemmas identify the first step, tail data, and branch integrals of the resulting growth. This is the combinatorial engine of the inductive proof of the BKAR forest interpolation formula (see BKAR.Formula).

def BKAR.Forest.ActiveExtension.consGrowth {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.ActiveExtension e) (tail : h.forest.OrderedGrowth order G) : F.OrderedGrowth (e :: order) G

Prepend a chosen active extension to an ordered growth from the extended forest.

Equations

• h.consGrowth tail = BKAR.Forest.OrderedGrowth.cons ⋯ tail

theorem BKAR.Forest.ActiveExtension.consGrowth_firstStep {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.ActiveExtension e) (tail : h.forest.OrderedGrowth order G) : ⋯ = ⋯

theorem BKAR.Forest.ActiveExtension.consGrowth_tailGrowth {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.ActiveExtension e) (tail : h.forest.OrderedGrowth order G) : (h.consGrowth tail).tailGrowth = tail

theorem BKAR.Forest.ActiveExtension.consGrowth_firstActiveExtension {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.ActiveExtension e) (tail : h.forest.OrderedGrowth order G) : (h.consGrowth tail).firstActiveExtension = h

theorem BKAR.Forest.ActiveExtension.consGrowth_tailForest {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.ActiveExtension e) (tail : h.forest.OrderedGrowth order G) : (h.consGrowth tail).tailForest = h.forest

theorem BKAR.Forest.ActiveExtension.singletonGrowth_eq_consGrowth_nil {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) : h.singletonGrowth = h.consGrowth (OrderedGrowth.nil h.forest)

theorem BKAR.Forest.ActiveExtension.consGrowth_params_first {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.ActiveExtension e) (tail : h.forest.OrderedGrowth order G) (u : F.EdgeParam → ℝ) (t : ℝ) (ts : List ℝ) : (h.consGrowth tail).params u (t :: ts) ⟨e, ⋯⟩ = t

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

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

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

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