The unit cube and its ordered sectors

Defines the unit cube [0,1]^{E(F)} of a forest's edge parameters and, for each enumeration of the edge set, the closed ordered sector orderedCubeSimplex of parameter points whose coordinates decrease along that order. Proves that ordered-simplex parameter lists land in the matching sector and that the sectors cover the cube: the unit cube is the union of its canonical ordered sectors. This is the set-level part of the unit-cube partition step, which folds per-order sectors into the single cube integral of the BKAR forest interpolation formula (see BKAR.Formula).

def BKAR.Forest.unitCube {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : Set (F.EdgeParam → ℝ)

The parameter cube [0, 1]^{E(F)} for a forest. Parameters are indexed by the edge subtype F.EdgeParam.

Equations

• F.unitCube = Set.univ.pi fun (x : F.EdgeParam) => Set.Icc 0 1

theorem BKAR.Forest.mem_unitCube_iff {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : u ∈ F.unitCube ↔ ∀ (e : F.EdgeParam), 0 ≤ u e ∧ u e ≤ 1

def BKAR.Forest.orderedCubeSimplex {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) : Set (F.EdgeParam → ℝ)

The ordered simplex sector inside the unit cube attached to one edge order. For order = [e₁, ..., eₙ], this is the region 1 ≥ u(e₁) ≥ ... ≥ u(eₙ) ≥ 0, together with the ambient cube bounds.

Equations

• F.orderedCubeSimplex order = {u : F.EdgeParam → ℝ | u ∈ F.unitCube ∧ BKAR.OrderedSimplexParams 1 (List.map (F.paramValue u) order)}

theorem BKAR.Forest.mem_orderedCubeSimplex_iff {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) (u : F.EdgeParam → ℝ) : u ∈ F.orderedCubeSimplex order ↔ u ∈ F.unitCube ∧ OrderedSimplexParams 1 (List.map (F.paramValue u) order)

theorem BKAR.Forest.orderedCubeSimplex_subset_unitCube {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) : F.orderedCubeSimplex order ⊆ F.unitCube

theorem BKAR.Forest.orderedCubeSimplex_nil {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : F.orderedCubeSimplex [] = F.unitCube

theorem BKAR.Forest.paramsOfOrder_mem_unitCube_of_orderedSimplexParams {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) {ts : List ℝ} (hts : OrderedSimplexParams 1 ts) : F.paramsOfOrder order ts ∈ F.unitCube

Any ordered-simplex coordinate list gives a point of the unit cube through paramsOfOrder. Coordinates not represented in the list use the default 0.

theorem BKAR.Forest.map_paramValue_paramsOfOrder_eq_of_nodup_of_forall_mem {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) {ts : List ℝ} : order.Nodup → (∀ e ∈ order, e ∈ F.edges) → ts.length = order.length → List.map (F.paramValue (F.paramsOfOrder order ts)) order = ts

Reading back the parameters of a nodup order from paramsOfOrder recovers the original coordinate list, provided the list lengths match.

theorem BKAR.Forest.map_paramValue_paramsOfOrder_eq_of_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) {ts : List ℝ} (hlen : ts.length = order.length) : List.map (F.paramValue (F.paramsOfOrder order ts)) order = ts

For a canonical edge order, paramsOfOrder is a right inverse to the sector coordinate readback map.

theorem BKAR.Forest.paramsOfOrder_mem_orderedCubeSimplex_of_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) {ts : List ℝ} (hts : OrderedSimplexParams 1 ts) (hlen : ts.length = order.length) : F.paramsOfOrder order ts ∈ F.orderedCubeSimplex order

Set-level simplex-sector bridge: ordered-simplex coordinates, sent into cube coordinates by paramsOfOrder, land in the ordered cube sector for the same canonical edge order.

theorem BKAR.Forest.orderedSimplexParams_map_paramValue_of_pairwise_ge {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (order : List (Edge V)) (top : ℝ) : List.Pairwise (fun (e e' : Edge V) => F.paramValue u e' ≤ F.paramValue u e) order → (∀ e ∈ order, 0 ≤ F.paramValue u e) → (∀ e ∈ order, F.paramValue u e ≤ top) → OrderedSimplexParams top (List.map (F.paramValue u) order)

If an edge order is pairwise sorted in descending parameter value and every listed value lies in [0, top], then the readback value list is an ordered simplex.

theorem BKAR.Forest.exists_mem_edgeOrders_and_mem_orderedCubeSimplex_of_mem_unitCube {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {u : F.EdgeParam → ℝ} (hu : u ∈ F.unitCube) : ∃ order ∈ F.edgeOrders, u ∈ F.orderedCubeSimplex order

Set-level cube cover for the unit-cube partition step: every point of the unit cube lies in at least one ordered cube sector indexed by a canonical edge order.

theorem BKAR.Forest.unitCube_subset_iUnion_orderedCubeSimplex {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : F.unitCube ⊆ ⋃ (order : ↥F.edgeOrders), F.orderedCubeSimplex ↑order

The ordered cube sectors cover the unit cube.

theorem BKAR.Forest.iUnion_orderedCubeSimplex_subset_unitCube {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : ⋃ (order : ↥F.edgeOrders), F.orderedCubeSimplex ↑order ⊆ F.unitCube

Every ordered cube sector is contained in the unit cube.

theorem BKAR.Forest.unitCube_eq_iUnion_orderedCubeSimplex {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : F.unitCube = ⋃ (order : ↥F.edgeOrders), F.orderedCubeSimplex ↑order

Set-level partition cover: the unit cube is the union of its canonical ordered cube sectors. Pairwise disjointness only holds away from coordinate collision hyperplanes, which is the remaining measure-zero part of the unit-cube partition step.

noncomputable def BKAR.Forest.cubeContribution {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The usual unordered BKAR cube contribution for one Forest representative, using the mixed partial attached to F.edges.toList.

Equations

• F.cubeContribution ρ = ∫ (u : F.EdgeParam → ℝ) in F.unitCube, F.mixedPartial ρ (F.standardInterp u)

noncomputable def BKAR.Forest.orderedCubeSectorContribution {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The set-integral version of one ordered cube sector. The later cube-partition bridge identifies the sum of these sectors with cubeContribution; the ordered-simplex bridge identifies each sector with orderedContribution.

Equations

• F.orderedCubeSectorContribution order ρ = ∫ (u : F.EdgeParam → ℝ) in F.orderedCubeSimplex order, BKAR.mixedPartialList order.reverse ρ (F.standardInterp u)