Finite layer-cake decomposition for BKAR threshold components

This file proves the scalar combinatorial layer behind component-form arguments for the BKAR forest interpolation formula (see BKAR.Formula). For a BKAR forest point lambda = F.standardInterp u, the finitely many values of lambda, together with 0 and 1, determine a finite set of threshold levels. The jumps between consecutive levels form nonnegative weights, and the weighted sum of threshold-component indicators recovers the BKAR interpolation value.

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

The finite set of scalar levels needed for the layer-cake decomposition of a BKAR interpolation point.

Equations

• F.interpolationLevels u = insert 0 (insert 1 (Finset.image (fun (e : BKAR.Edge V) => F.standardInterp u e) Finset.univ))

@[simp]

theorem BKAR.Forest.zero_mem_interpolationLevels {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : 0 ∈ F.interpolationLevels u

@[simp]

theorem BKAR.Forest.one_mem_interpolationLevels {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : 1 ∈ F.interpolationLevels u

theorem BKAR.Forest.standardInterp_mem_interpolationLevels {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (e : Edge V) : F.standardInterp u e ∈ F.interpolationLevels u

theorem BKAR.Forest.interpolationLevels_subset_Icc {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) {x : ℝ} (hx : x ∈ F.interpolationLevels u) : 0 ≤ x ∧ x ≤ 1

theorem BKAR.Forest.one_lt_interpolationLevels_card {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : 1 < (F.interpolationLevels u).card

theorem BKAR.Forest.interpolationLevels_card_pos {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : 0 < (F.interpolationLevels u).card

theorem BKAR.Forest.interpolationLevels_min_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) : (F.interpolationLevels u).min' ⋯ = 0

theorem BKAR.Forest.interpolationLevels_max_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) : (F.interpolationLevels u).max' ⋯ = 1

noncomputable def BKAR.Forest.interpolationLevel {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (i : Fin (F.interpolationLevels u).card) : ℝ

The ith level, in increasing order.

Equations

• F.interpolationLevel u i = ((F.interpolationLevels u).orderEmbOfFin ⋯) i

theorem BKAR.Forest.interpolationLevel_zero {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) : F.interpolationLevel u ⟨0, ⋯⟩ = 0

theorem BKAR.Forest.interpolationLevel_last {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) : F.interpolationLevel u ⟨(F.interpolationLevels u).card - 1, ⋯⟩ = 1

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

The threshold level attached to the ith layer.

Equations

• F.interpolationLayerThreshold u i = if hi : i < (F.interpolationLevels u).card - 1 then F.interpolationLevel u ⟨i + 1, ⋯⟩ else 0

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

The jump between consecutive sorted interpolation levels.

Equations

• F.interpolationGap u i = if hi : i < (F.interpolationLevels u).card - 1 then F.interpolationLayerThreshold u i - F.interpolationLevel u ⟨i, ⋯⟩ else 0

theorem BKAR.Forest.interpolationLayerThreshold_of_lt {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {i : ℕ} (hi : i < (F.interpolationLevels u).card - 1) : F.interpolationLayerThreshold u i = F.interpolationLevel u ⟨i + 1, ⋯⟩

theorem BKAR.Forest.interpolationGap_of_lt {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {i : ℕ} (hi : i < (F.interpolationLevels u).card - 1) : F.interpolationGap u i = F.interpolationLevel u ⟨i + 1, ⋯⟩ - F.interpolationLevel u ⟨i, ⋯⟩

theorem BKAR.Forest.interpolationGap_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {i : ℕ} (hi : i < (F.interpolationLevels u).card - 1) : 0 ≤ F.interpolationGap u i

theorem BKAR.Forest.interpolationLayerThreshold_pos {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) {i : ℕ} (hi : i < (F.interpolationLevels u).card - 1) : 0 < F.interpolationLayerThreshold u i

theorem BKAR.Forest.interpolationLayerThreshold_le_one {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) {i : ℕ} (hi : i < (F.interpolationLevels u).card - 1) : F.interpolationLayerThreshold u i ≤ 1

theorem BKAR.Forest.sum_interpolationGap_range_eq_interpolationLevel {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {n : ℕ} (hn : n < (F.interpolationLevels u).card) : ∑ i ∈ Finset.range n, F.interpolationGap u i = F.interpolationLevel u ⟨n, hn⟩ - F.interpolationLevel u ⟨0, ⋯⟩

theorem BKAR.Forest.sum_interpolationGap_range_eq_interpolationLevel_of_zero {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) {n : ℕ} (hn : n < (F.interpolationLevels u).card) : ∑ i ∈ Finset.range n, F.interpolationGap u i = F.interpolationLevel u ⟨n, hn⟩

theorem BKAR.Forest.sum_interpolationGap_le_eq_of_mem_interpolationLevels {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) {x : ℝ} (hx : x ∈ F.interpolationLevels u) : (∑ i ∈ Finset.range ((F.interpolationLevels u).card - 1), if F.interpolationLayerThreshold u i ≤ x then F.interpolationGap u i else 0) = x

theorem BKAR.Forest.sum_interpolationGap_range_last_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) : ∑ i ∈ Finset.range ((F.interpolationLevels u).card - 1), F.interpolationGap u i = 1

theorem BKAR.Forest.sum_interpolationGap_thresholdComponent_edge_eq_standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) (e : Edge V) : (∑ i ∈ Finset.range ((F.interpolationLevels u).card - 1), if e.right ∈ F.thresholdComponent u (F.interpolationLayerThreshold u i) e.left then F.interpolationGap u i else 0) = F.standardInterp u e

Layer-cake identity for a BKAR edge value, expressed using threshold components.

theorem BKAR.Forest.sum_interpolationGap_thresholdComponent_diag_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (hu : ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1) (z : V) : (∑ i ∈ Finset.range ((F.interpolationLevels u).card - 1), if z ∈ F.thresholdComponent u (F.interpolationLayerThreshold u i) z then F.interpolationGap u i else 0) = 1

Diagonal layer-cake identity: every threshold component contains its base point.