Parameter transport along ordered growths

Transports simplex parameter lists along an ordered forest growth: params assembles the edge parameters of the grown forest from a list of interpolation times, and the lemmas locate the resulting values in [0, 1] and compare them under the ordered-simplex constraints. This is the parameter bookkeeping for the nested integrals in the ordered expansion of the BKAR forest interpolation formula (see BKAR.Formula).

theorem BKAR.Forest.EdgeExtension.extendParam_mem_Icc {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} (h : F.EdgeExtension F' e) (u : F.EdgeParam → ℝ) {s : ℝ} (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) (hs : 0 ≤ s ∧ s ≤ 1) (e' : F'.EdgeParam) : 0 ≤ h.extendParam u s e' ∧ h.extendParam u s e' ≤ 1

theorem BKAR.Forest.EdgeExtension.le_extendParam_of_le {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} (h : F.EdgeExtension F' e) (u : F.EdgeParam → ℝ) {s top : ℝ} (hst : s ≤ top) (hu : ∀ (e : F.EdgeParam), top ≤ u e) (e' : F'.EdgeParam) : s ≤ h.extendParam u s e'

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

Extend a starting forest parameter through an ordered growth certificate, reading newly added edge parameters from a list in growth order.

If the list is shorter than the order, the missing new parameters are filled with 0; extra parameters are ignored once the growth terminates.

Equations

• One or more equations did not get rendered due to their size.
• (BKAR.Forest.OrderedGrowth.nil F).params = fun (u : F.EdgeParam → ℝ) (x : List ℝ) => u

@[simp]

theorem BKAR.Forest.OrderedGrowth.params_nil {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ts : List ℝ) : (nil F).params u ts = u

@[simp]

theorem BKAR.Forest.OrderedGrowth.params_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).params u [] = tail.params (step.extendParam u 0) []

@[simp]

theorem BKAR.Forest.OrderedGrowth.params_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).params u (t :: ts) = tail.params (step.extendParam u t) ts

theorem BKAR.Forest.OrderedGrowth.params_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 → ℝ) (ts : List ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) (hts : ∀ t ∈ ts, 0 ≤ t ∧ t ≤ 1) (e : G.EdgeParam) : 0 ≤ h.params u ts e ∧ h.params u ts e ≤ 1

theorem BKAR.Forest.OrderedGrowth.params_mem_Icc_of_orderedSimplexParams {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 : G.EdgeParam) : 0 ≤ h.params u ts e ∧ h.params u ts e ≤ 1

theorem BKAR.Forest.OrderedGrowth.params_mem_Icc_of_orderedSimplexParams_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 : G.EdgeParam) : 0 ≤ h.params u ts e ∧ h.params u ts e ≤ 1

theorem BKAR.Forest.OrderedGrowth.firstStep_le_extendParam_of_orderedSimplexParams {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 → ℝ) {top t : ℝ} {ts : List ℝ} (hts : OrderedSimplexParams top (t :: ts)) (hu : ∀ (e : F.EdgeParam), top ≤ u e) (e' : h.tailForest.EdgeParam) : t ≤ ⋯.extendParam u t e'

theorem BKAR.Forest.OrderedGrowth.params_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.params u ts ⟨↑e, ⋯⟩ = u e

Ordered-growth parameters preserve every edge parameter already present at the start.

theorem BKAR.Forest.OrderedGrowth.params_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.params u (t :: ts) ⟨e, ⋯⟩ = t

The first simplex parameter is assigned to the first edge of a nonempty growth.