Threshold components for BKAR interpolation

This file packages the threshold-connected vertices of a BKAR forest as an actual finite partition. It is the combinatorial surface needed for component-form positivity arguments built on the BKAR forest interpolation formula (see BKAR.Formula): at threshold s, two vertices lie in the same partition cell exactly when they are connected by forest edges whose parameters are at least s.

theorem BKAR.Finpartition.sum_parts_indicator_pair {V : Type u_1} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) (r : ℝ) (z w : V) : (∑ c : ↥P.parts, if z ∈ ↑c ∧ w ∈ ↑c then r else 0) = if w ∈ P.part z then r else 0

Summing the indicator of “z and w lie in the same part” over the parts of a finite partition leaves exactly the indicator of the part containing z.

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

The Forest representative carried by the threshold edge set.

Equations

• F.thresholdForest u s = (Classical.choice ⋯).toForest

@[simp]

theorem BKAR.Forest.thresholdForest_edges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s : ℝ) : (F.thresholdForest u s).edges = F.thresholdEdges u s

theorem BKAR.Forest.thresholdConnected_iff_thresholdForest_inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s : ℝ) (i j : V) : F.thresholdConnected u s i j ↔ (F.thresholdForest u s).inSameComponent i j

Threshold connectivity agrees with the ordinary component relation in the threshold forest.

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

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

theorem BKAR.Forest.thresholdConnected_trans {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s : ℝ) {i j k : V} (hij : F.thresholdConnected u s i j) (hjk : F.thresholdConnected u s j k) : F.thresholdConnected u s i k

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

Threshold connectivity as a finite setoid on vertices.

Equations

• F.thresholdSetoid u s = { r := F.thresholdConnected u s, iseqv := ⋯ }

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

The finite partition of vertices into threshold-connected components.

Equations

• F.thresholdPartition u s = Finpartition.ofSetoid (F.thresholdSetoid u s)

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

The threshold component containing a given vertex.

Equations

• F.thresholdComponent u s i = (F.thresholdPartition u s).part i

@[simp]

theorem BKAR.Forest.mem_thresholdComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s : ℝ) (i j : V) : j ∈ F.thresholdComponent u s i ↔ F.thresholdConnected u s i j

theorem BKAR.Forest.self_mem_thresholdComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s : ℝ) (i : V) : i ∈ F.thresholdComponent u s i

theorem BKAR.Forest.le_standardInterp_iff_mem_thresholdComponent {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 ↔ e.right ∈ F.thresholdComponent u s e.left

Positive-threshold layer-set form of the BKAR interpolation value: the edge value is above s exactly when the endpoints lie in the same threshold component.

theorem BKAR.Forest.sum_thresholdPartition_parts_indicator_pair {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (s r : ℝ) (z w : V) : (∑ c : ↥(F.thresholdPartition u s).parts, if z ∈ ↑c ∧ w ∈ ↑c then r else 0) = if w ∈ F.thresholdComponent u s z then r else 0

At a fixed threshold, summing over threshold partition cells gives the component indicator of the threshold component containing z.