Path-minimum forest interpolation

The interpolation scheme at the heart of the BKAR forest interpolation formula (see BKAR.Formula). For a forest F with edge parameters u : F.EdgeParam → ℝ, the interpolation point standardInterp (the point x^F(u)) assigns to an edge {i, j} the minimum of u along the unique forest path joining i to j when both lie in the same component of F, and 0 otherwise. Also provides the constant, zero, and all-ones edge configurations, the extended parameter reading paramValue, the path minimum pathMin, the one-parameter family interpWithFill driving the inductive proof, and one-edge extensions EdgeExtension with their parameter transport.

def BKAR.constantConfig {V : Type u_1} (t : ℝ) : Edge V → ℝ

The constant BKAR configuration.

Equations

• BKAR.constantConfig t x✝ = t

def BKAR.zeroConfig {V : Type u_1} : Edge V → ℝ

The zero BKAR configuration.

Equations

• BKAR.zeroConfig = BKAR.constantConfig 0

def BKAR.oneConfig {V : Type u_1} : Edge V → ℝ

The all-one BKAR configuration.

Equations

• BKAR.oneConfig = BKAR.constantConfig 1

@[reducible, inline]

abbrev BKAR.Forest.EdgeParam {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) : Type u_2

Edge parameters attached only to the edge set of a forest.

Equations

• F.EdgeParam = ↥F.edges

def BKAR.Forest.emptyParam {V : Type u_2} [Fintype V] [DecidableEq V] : (empty V).EdgeParam → ℝ

The unique edge-parameter function on the empty forest.

Equations

• BKAR.Forest.emptyParam e = ⋯.elim

theorem BKAR.Forest.emptyParam_unique {V : Type u_2} [Fintype V] [DecidableEq V] (u : (empty V).EdgeParam → ℝ) : u = emptyParam

def BKAR.Forest.paramValue {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (e : Edge V) : ℝ

Look up the value of an edge parameter, with default value 1 off the forest.

Equations

• F.paramValue u e = if he : e ∈ F.edges then u ⟨e, he⟩ else 1

@[simp]

theorem BKAR.Forest.paramValue_of_mem {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {e : Edge V} (he : e ∈ F.edges) : F.paramValue u e = u ⟨e, he⟩

def BKAR.Forest.pathMinAux {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : ℝ → List (Edge V) → ℝ

Auxiliary minimum, seeded by the first edge of a nonempty path.

Equations

• F.pathMinAux u x✝ [] = x✝
• F.pathMinAux u x✝ (e :: γ) = F.pathMinAux u (min x✝ (F.paramValue u e)) γ

def BKAR.Forest.pathMin {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : List (Edge V) → ℝ

Minimum of forest parameters along a path, with empty path convention 1.

Equations

• F.pathMin u [] = 1
• F.pathMin u (e :: γ) = F.pathMinAux u (F.paramValue u e) γ

@[simp]

theorem BKAR.Forest.pathMin_nil {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : F.pathMin u [] = 1

@[simp]

theorem BKAR.Forest.pathMin_cons {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (e : Edge V) (γ : List (Edge V)) : F.pathMin u (e :: γ) = F.pathMinAux u (F.paramValue u e) γ

theorem BKAR.Forest.pathMin_singleton {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {e : Edge V} (he : e ∈ F.edges) : F.pathMin u [e] = u ⟨e, he⟩

theorem BKAR.Forest.paramValue_mem_Icc {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) (e : Edge V) : 0 ≤ F.paramValue u e ∧ F.paramValue u e ≤ 1

theorem BKAR.Forest.pathMinAux_mem_Icc {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) {a : ℝ} : 0 ≤ a ∧ a ≤ 1 → ∀ (γ : List (Edge V)), 0 ≤ F.pathMinAux u a γ ∧ F.pathMinAux u a γ ≤ 1

theorem BKAR.Forest.pathMin_mem_Icc {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) (γ : List (Edge V)) : 0 ≤ F.pathMin u γ ∧ F.pathMin u γ ≤ 1

noncomputable def BKAR.Forest.standardInterp {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : Edge V → ℝ

The standard BKAR interpolation point x^F(u).

Equations

• F.standardInterp u e = if h : F.inSameComponent e.left e.right then F.pathMin u (F.pathInF e.left e.right h) else 0

noncomputable def BKAR.Forest.interpWithFill {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (t : ℝ) : Edge V → ℝ

The one-parameter family W^F(u; t) used in the iterative proof.

Equations

• F.interpWithFill u t e = if h : F.inSameComponent e.left e.right then F.pathMin u (F.pathInF e.left e.right h) else t

theorem BKAR.Forest.interpWithFill_zero {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : F.interpWithFill u 0 = F.standardInterp u

theorem BKAR.Forest.standardInterp_of_not_inSameComponent {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {e : Edge V} (he : ¬F.inSameComponent e.left e.right) : F.standardInterp u e = 0

theorem BKAR.Forest.interpWithFill_of_not_inSameComponent {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (t : ℝ) {e : Edge V} (he : ¬F.inSameComponent e.left e.right) : F.interpWithFill u t e = t

theorem BKAR.Forest.standardInterp_of_mem {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {e : Edge V} (he : e ∈ F.edges) : F.standardInterp u e = u ⟨e, he⟩

theorem BKAR.Forest.interpWithFill_of_mem {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (t : ℝ) {e : Edge V} (he : e ∈ F.edges) : F.interpWithFill u t e = u ⟨e, he⟩

theorem BKAR.Forest.standardInterp_mem_Icc {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) (e : Edge V) : 0 ≤ F.standardInterp u e ∧ F.standardInterp u e ≤ 1

theorem BKAR.Forest.interpWithFill_mem_Icc {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) {t : ℝ} (ht : 0 ≤ t ∧ t ≤ 1) (e : Edge V) : 0 ≤ F.interpWithFill u t e ∧ F.interpWithFill u t e ≤ 1

theorem BKAR.Forest.empty_standardInterp {V : Type u_2} [Fintype V] [DecidableEq V] (u : (empty V).EdgeParam → ℝ) : (empty V).standardInterp u = zeroConfig

theorem BKAR.Forest.empty_interpWithFill {V : Type u_2} [Fintype V] [DecidableEq V] (u : (empty V).EdgeParam → ℝ) (t : ℝ) : (empty V).interpWithFill u t = constantConfig t

theorem BKAR.Forest.empty_interpWithFill_one {V : Type u_2} [Fintype V] [DecidableEq V] (u : (empty V).EdgeParam → ℝ) : (empty V).interpWithFill u 1 = oneConfig

theorem BKAR.Forest.emptyParam_standardInterp {V : Type u_2} [Fintype V] [DecidableEq V] : (empty V).standardInterp emptyParam = zeroConfig

theorem BKAR.Forest.emptyParam_interpWithFill {V : Type u_2} [Fintype V] [DecidableEq V] (t : ℝ) : (empty V).interpWithFill emptyParam t = constantConfig t

theorem BKAR.Forest.emptyParam_interpWithFill_one {V : Type u_2} [Fintype V] [DecidableEq V] : (empty V).interpWithFill emptyParam 1 = oneConfig

theorem BKAR.Forest.pathMinAux_eq_of_forall {V : Type u_2} [Fintype V] [DecidableEq V] (F G : Forest V) (u : F.EdgeParam → ℝ) (v : G.EdgeParam → ℝ) {a b : ℝ} : a = b → ∀ (γ : List (Edge V)), (∀ e ∈ γ, F.paramValue u e = G.paramValue v e) → F.pathMinAux u a γ = G.pathMinAux v b γ

theorem BKAR.Forest.pathMin_eq_of_forall {V : Type u_2} [Fintype V] [DecidableEq V] (F G : Forest V) (u : F.EdgeParam → ℝ) (v : G.EdgeParam → ℝ) (γ : List (Edge V)) : (∀ e ∈ γ, F.paramValue u e = G.paramValue v e) → F.pathMin u γ = G.pathMin v γ

theorem BKAR.Forest.standardInterp_eq_of_edges_eq {V : Type u_2} [Fintype V] [DecidableEq V] (F G : Forest V) (u : F.EdgeParam → ℝ) (v : G.EdgeParam → ℝ) (hedges : F.edges = G.edges) (hparam : ∀ (e : Edge V), F.paramValue u e = G.paramValue v e) : F.standardInterp u = G.standardInterp v

The standard BKAR interpolation point only depends on the underlying edge set and the ambient edge-parameter values, not on the particular path data stored in a Forest.

theorem BKAR.Forest.pathMinAux_le_seed {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (a : ℝ) (γ : List (Edge V)) : F.pathMinAux u a γ ≤ a

theorem BKAR.Forest.le_pathMinAux_of_forall {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {s a : ℝ} : s ≤ a → ∀ (γ : List (Edge V)), (∀ e ∈ γ, s ≤ F.paramValue u e) → s ≤ F.pathMinAux u a γ

theorem BKAR.Forest.le_pathMin_of_mem_forall {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {s : ℝ} {e₀ : Edge V} {γ : List (Edge V)} : e₀ ∈ γ → (∀ e ∈ γ, s ≤ F.paramValue u e) → s ≤ F.pathMin u γ

theorem BKAR.Forest.pathMinAux_le_of_mem_eq {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {s : ℝ} {e₀ : Edge V} {a : ℝ} (γ : List (Edge V)) : e₀ ∈ γ → F.paramValue u e₀ = s → F.pathMinAux u a γ ≤ s

theorem BKAR.Forest.pathMin_le_of_mem_eq {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {s : ℝ} {e₀ : Edge V} {γ : List (Edge V)} : e₀ ∈ γ → F.paramValue u e₀ = s → F.pathMin u γ ≤ s

def BKAR.Forest.EdgeExtension.extendParam {V : Type u_2} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) (s : ℝ) : F'.EdgeParam → ℝ

Extend forest-edge parameters to a one-edge extension.

Equations

• h.extendParam u s e = if he : ↑e = e₀ then s else u ⟨↑e, ⋯⟩

theorem BKAR.Forest.EdgeExtension.extendParam_new {V : Type u_2} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) (s : ℝ) : h.extendParam u s ⟨e₀, ⋯⟩ = s

theorem BKAR.Forest.EdgeExtension.extendParam_old {V : Type u_2} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) (s : ℝ) {e : Edge V} (he : e ∈ F.edges) : h.extendParam u s ⟨e, ⋯⟩ = u ⟨e, he⟩

theorem BKAR.Forest.EdgeExtension.paramValue_extend_new {V : Type u_2} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) (s : ℝ) : F'.paramValue (h.extendParam u s) e₀ = s

theorem BKAR.Forest.EdgeExtension.paramValue_extend_old {V : Type u_2} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) (s : ℝ) {e : Edge V} (he : e ∈ F.edges) : F'.paramValue (h.extendParam u s) e = F.paramValue u e

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

theorem BKAR.Forest.EdgeExtension.paramValue_extend_le {V : Type u_2} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) {s : ℝ} (hu : ∀ (e : F.EdgeParam), s ≤ u e) {e : Edge V} (he : e ∈ F'.edges) : s ≤ F'.paramValue (h.extendParam u s) e

theorem BKAR.Forest.EdgeExtension.interpWithFill_extend_eq {V : Type u_2} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) {s : ℝ} (hu : ∀ (e : F.EdgeParam), s ≤ u e) : F.interpWithFill u s = F'.interpWithFill (h.extendParam u s) s

Ordered-step reinterpretation: if the newly-added edge receives the current global parameter s, and all old forest parameters are at least s, then the old and extended fill-parameter configurations agree at s.