Ordered coordinate equivalences

For each enumeration of a forest's edge set, constructs the measurable, measure-preserving equivalence between the forest's edge-parameter space and Fin n → ℝ that reads coordinates in the given order, and defines the standard ordered simplex orderedFinSimplex in Fin n → ℝ. The ordered cube sector is the preimage of the standard ordered simplex under this equivalence — the change of variables underlying the simplex-sector conversion.

def BKAR.Forest.edgeParamEquivOrderSubtype {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) : { e : Edge V // e ∈ order } ≃ F.EdgeParam

A canonical edge order lists exactly the same support as the forest edge parameter subtype.

Equations

• F.edgeParamEquivOrderSubtype horder = { toFun := fun (e : { e : BKAR.Edge V // e ∈ order }) => ⟨↑e, ⋯⟩, invFun := fun (e : F.EdgeParam) => ⟨↑e, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def BKAR.Forest.edgeParamFinEquivOfOrder {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) : Fin order.length ≃ F.EdgeParam

The finite coordinate equivalence attached to a canonical edge order. Its ith coordinate is the ith edge in the order.

Equations

• F.edgeParamFinEquivOfOrder horder = (List.Nodup.getEquiv order ⋯).trans (F.edgeParamEquivOrderSubtype horder)

@[simp]

theorem BKAR.Forest.edgeParamFinEquivOfOrder_apply_val {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (i : Fin order.length) : ↑((F.edgeParamFinEquivOfOrder horder) i) = order.get i

def BKAR.Forest.orderMeasurableEquivOfOrder {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) : (F.EdgeParam → ℝ) ≃ᵐ (Fin order.length → ℝ)

The measurable equivalence reading forest edge parameters in a canonical order as ordinary Fin order.length coordinates.

Equations

• F.orderMeasurableEquivOfOrder horder = (MeasurableEquiv.piCongrLeft (fun (x : F.EdgeParam) => ℝ) (F.edgeParamFinEquivOfOrder horder)).symm

theorem BKAR.Forest.measurePreserving_orderMeasurableEquivOfOrder {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) : MeasureTheory.MeasurePreserving (⇑(F.orderMeasurableEquivOfOrder horder)) MeasureTheory.volume MeasureTheory.volume

theorem BKAR.Forest.orderMeasurableEquivOfOrder_apply_edgeParam {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (u : F.EdgeParam → ℝ) (i : Fin order.length) : (F.orderMeasurableEquivOfOrder horder) u i = u ((F.edgeParamFinEquivOfOrder horder) i)

The ordered coordinate equivalence is, definitionally, readback along the order equivalence.

theorem BKAR.Forest.orderMeasurableEquivOfOrder_apply {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (u : F.EdgeParam → ℝ) (i : Fin order.length) : (F.orderMeasurableEquivOfOrder horder) u i = F.paramValue u (order.get i)

The ordered coordinate equivalence reads back the parameter of order.get i.

theorem BKAR.Forest.orderMeasurableEquivOfOrder_symm_apply {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (ts : Fin order.length → ℝ) (p : F.EdgeParam) : (F.orderMeasurableEquivOfOrder horder).symm ts p = ts ((F.edgeParamFinEquivOfOrder horder).symm p)

theorem BKAR.Forest.continuous_orderMeasurableEquivOfOrder_symm {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) : Continuous fun (ts : Fin order.length → ℝ) => (F.orderMeasurableEquivOfOrder horder).symm ts

The inverse ordered-coordinate equivalence is continuous.

theorem BKAR.Forest.paramsOfOrder_ofFn_eq_orderMeasurableEquiv_symm {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (ts : Fin order.length → ℝ) : F.paramsOfOrder order (List.ofFn ts) = (F.orderMeasurableEquivOfOrder horder).symm ts

The inverse coordinate equivalence is the same point of the forest cube as paramsOfOrder, when the coordinate list is formed from the Fin tuple.

def BKAR.Forest.orderedFinSimplex (n : ℕ) : Set (Fin n → ℝ)

The ordered finite simplex in Fin n coordinates, including the ambient closed cube bounds. This is the coordinate target for arbitrary canonical orders.

Equations

• BKAR.Forest.orderedFinSimplex n = {ts : Fin n → ℝ | (∀ (i : Fin n), 0 ≤ ts i ∧ ts i ≤ 1) ∧ BKAR.OrderedSimplexParams 1 (List.ofFn ts)}

theorem BKAR.Forest.mem_orderedFinSimplex_iff {n : ℕ} (ts : Fin n → ℝ) : ts ∈ orderedFinSimplex n ↔ (∀ (i : Fin n), 0 ≤ ts i ∧ ts i ≤ 1) ∧ OrderedSimplexParams 1 (List.ofFn ts)

theorem BKAR.Forest.map_paramValue_eq_ofFn_orderMeasurableEquiv {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (u : F.EdgeParam → ℝ) : List.map (F.paramValue u) order = List.ofFn ((F.orderMeasurableEquivOfOrder horder) u)

Reading an arbitrary cube point in canonical order gives the corresponding ofFn list.

theorem BKAR.Forest.orderedCubeSimplex_eq_orderMeasurableEquiv_preimage_orderedFinSimplex {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) : F.orderedCubeSimplex order = ⇑(F.orderMeasurableEquivOfOrder horder) ⁻¹' orderedFinSimplex order.length

Set-level arbitrary-order simplex-sector bridge: a canonical ordered cube sector is the preimage of the standard ordered finite simplex under the ordered coordinate equivalence.

theorem BKAR.Forest.setIntegral_orderedCubeSimplex_orderMeasurableEquiv_eq_orderedFinSimplex {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (g : (Fin order.length → ℝ) → ℝ) : ∫ (u : F.EdgeParam → ℝ) in F.orderedCubeSimplex order, g ((F.orderMeasurableEquivOfOrder horder) u) = ∫ (ts : Fin order.length → ℝ) in orderedFinSimplex order.length, g ts

Measure transport for arbitrary canonical orders, for integrands already written in ordered finite coordinates.