Simplex-sector conversion: one edge

The one-dimensional case of the simplex-sector conversion: for a forest with a single edge, the recursive ordered contribution is the set integral over [0, 1] in the unique cube coordinate, identified through the funUnique measure-preserving equivalence, and hence equals the closed ordered cube-sector contribution.

theorem BKAR.Forest.edges_eq_singleton_of_singleton_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (horder : [e] ∈ F.edgeOrders) : F.edges = {e}

@[reducible]

def BKAR.Forest.uniqueEdgeParamOfEdgesSingleton {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (hedges : F.edges = {e}) : Unique F.EdgeParam

The unique edge parameter when the forest consists of the specified single edge.

Equations

• F.uniqueEdgeParamOfEdgesSingleton hedges = { default := ⟨e, ⋯⟩, uniq := ⋯ }

theorem BKAR.Forest.paramsOfOrder_singleton_eq_funUnique_symm {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (hedges : F.edges = {e}) (t : ℝ) : F.paramsOfOrder [e] [t] = (MeasurableEquiv.funUnique F.EdgeParam ℝ).symm t

theorem BKAR.Forest.orderedCubeSimplex_singleton_eq_funUnique_preimage_Icc {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (hedges : F.edges = {e}) : F.orderedCubeSimplex [e] = ⇑(MeasurableEquiv.funUnique F.EdgeParam ℝ) ⁻¹' Set.Icc 0 1

theorem BKAR.Forest.measurePreserving_funUnique_edgeParam_singleton {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (hedges : F.edges = {e}) : MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.funUnique F.EdgeParam ℝ)) MeasureTheory.volume MeasureTheory.volume

theorem BKAR.Forest.orderedSimplexIntegral_singleton_eq_setIntegral_Icc {V : Type u_1} (e : Edge V) (f : ℝ → ℝ) : (orderedSimplexIntegral [e] fun (ts : List ℝ) => f (ts.getD 0 0)) = ∫ (t : ℝ) in Set.Icc 0 1, f t

The one-dimensional ordered simplex integral is the set integral over [0, 1].

theorem BKAR.Forest.orderedContribution_singleton_eq_setIntegral_Icc_funUnique {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (hedges : F.edges = {e}) (ρ : (Edge V → ℝ) → ℝ) : F.orderedContribution [e] ρ = ∫ (t : ℝ) in Set.Icc 0 1, mixedPartialList [e].reverse ρ (F.standardInterp ((MeasurableEquiv.funUnique F.EdgeParam ℝ).symm t))

First step of the simplex-sector conversion for one edge: the recursive ordered contribution is the ordinary set integral over the one-dimensional simplex coordinate. The remaining singleton sector bridge is exactly the funUnique measure-preserving identification of that coordinate with the one-edge cube.

theorem BKAR.Forest.orderedContribution_singleton_eq_orderedCubeSectorContribution {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (horder : [e] ∈ F.edgeOrders) (ρ : (Edge V → ℝ) → ℝ) : F.orderedContribution [e] ρ = F.orderedCubeSectorContribution [e] ρ

The simplex-sector conversion in the first nontrivial dimension: the nested ordered-simplex integral for a one-edge canonical order is exactly the set integral over the corresponding closed ordered cube sector.