One-edge growths and their branch integrals

A base case of the ordered recursion: the one-edge ordered growth singletonGrowth determined by a chosen active extension, and the identification of its branch integral with a single interval integral of the partial derivative along the interpolation family, when the extended forest has no active edges left.

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

The one-edge ordered growth determined by a chosen active extension.

Equations

• h.singletonGrowth = BKAR.Forest.OrderedGrowth.cons ⋯ (BKAR.Forest.OrderedGrowth.nil h.forest)

theorem BKAR.Forest.ActiveExtension.singletonGrowth_firstStep {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) : ⋯ = ⋯

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

theorem BKAR.Forest.ActiveExtension.singleton_branchIntegralAux_eq_integral_partialDeriv_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : h.forest.activeEdges = ∅) : OrderedGrowth.branchIntegralAux top h.singletonGrowth u ρ = ∫ (t : ℝ) in 0..top, partialDeriv e ρ (h.forest.interpWithFill (⋯.extendParam u t) t)

theorem BKAR.Forest.ActiveExtension.integral_partialDeriv_eq_singleton_branchIntegralAux_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (top : ℝ) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : h.forest.activeEdges = ∅) : ∫ (t : ℝ) in 0..top, partialDeriv e ρ (h.forest.interpWithFill (⋯.extendParam u t) t) = OrderedGrowth.branchIntegralAux top h.singletonGrowth u ρ

theorem BKAR.Forest.ActiveExtension.singleton_branchIntegral_eq_integral_partialDeriv_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : h.forest.activeEdges = ∅) : h.singletonGrowth.branchIntegral u ρ = ∫ (t : ℝ) in 0..1, partialDeriv e ρ (h.forest.interpWithFill (⋯.extendParam u t) t)

theorem BKAR.Forest.ActiveExtension.integral_partialDeriv_eq_singleton_branchIntegral_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : h.forest.activeEdges = ∅) : ∫ (t : ℝ) in 0..1, partialDeriv e ρ (h.forest.interpWithFill (⋯.extendParam u t) t) = h.singletonGrowth.branchIntegral u ρ