Threshold subforests for BKAR interpolation

This file records the finite graph fact behind the component representation of BKAR interpolation points: threshold connectivity in a forest is equivalent to the path-min inequality along the unique forest path.

noncomputable def BKAR.Forest.thresholdEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s : ℝ) : Finset (Edge V)

Edges of a forest whose parameter is at least the threshold s.

Equations

• F.thresholdEdges u s = {e ∈ F.edges | s ≤ F.paramValue u e}

@[simp]

theorem BKAR.Forest.mem_thresholdEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s : ℝ) (e : Edge V) : e ∈ F.thresholdEdges u s ↔ e ∈ F.edges ∧ s ≤ F.paramValue u e

noncomputable def BKAR.Forest.thresholdIndex {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s : ℝ) : ForestIndex V

The threshold edge set is again an acyclic forest index.

Equations

• F.thresholdIndex u s = { edges := F.thresholdEdges u s, acyclic := ⋯ }

def BKAR.Forest.thresholdConnected {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s : ℝ) (i j : V) : Prop

Two vertices are threshold-connected when a simple forest path joins them using only edges whose parameter is at least s.

Equations

• F.thresholdConnected u s i j = ∃ (γ : List (BKAR.Edge V)), BKAR.IsSimplePath F γ i j ∧ ∀ e ∈ γ, s ≤ F.paramValue u e

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

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

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

theorem BKAR.Forest.thresholdConnected_iff_exists_le_pathMin {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {s : ℝ} (hs : s ≤ 1) (i j : V) : F.thresholdConnected u s i j ↔ ∃ (h : F.inSameComponent i j), s ≤ F.pathMin u (F.pathInF i j h)

Threshold connectivity is the same as being in the original forest component with path minimum at least s.

theorem BKAR.Forest.le_standardInterp_iff_thresholdConnected {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (e : Edge V) : s ≤ F.standardInterp u e ↔ F.thresholdConnected u s e.left e.right

For positive thresholds, the standard BKAR edge value is above threshold exactly when its endpoints are threshold-connected.