Almost-everywhere disjointness of the ordered sectors

The measure-theoretic half of the unit-cube partition step: coordinate collision hyperplanes are Lebesgue-null, distinct ordered sectors meet only in collisions, hence the sectors are pairwise almost-everywhere disjoint and the integral of an integrable function over the unit cube is the sum of its sector integrals. This justifies folding the per-order sector integrals of the BKAR forest interpolation formula (see BKAR.Formula) into one cube integral.

theorem BKAR.OrderedSimplexParams.pairwise_ge {top : ℝ} {ts : List ℝ} : OrderedSimplexParams top ts → List.Pairwise (fun (t s : ℝ) => s ≤ t) ts

def BKAR.Forest.collisionPairs {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : Type u_1

Ordered pairs of distinct forest-edge parameters.

Equations

• F.collisionPairs = { p : F.EdgeParam × F.EdgeParam // p.1 ≠ p.2 }

@[instance_reducible]

instance BKAR.Forest.instFintypeCollisionPairs {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : Fintype F.collisionPairs

Equations

• F.instFintypeCollisionPairs = id inferInstance

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

The collision locus where two distinct forest-edge cube coordinates agree. This is the union of the codimension-one hyperplanes that form the overlaps of the closed ordered sectors.

Equations

• F.collisionSet = ⋃ (p : F.collisionPairs), {u : F.EdgeParam → ℝ | u (↑p).1 = u (↑p).2}

theorem BKAR.Forest.measure_coordinateCollision_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (a b : F.EdgeParam) (hne : a ≠ b) : MeasureTheory.volume {u : F.EdgeParam → ℝ | u a = u b} = 0

The coordinate-equality hyperplane attached to two distinct edge parameters is null.

theorem BKAR.Forest.measure_collisionSet_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : MeasureTheory.volume F.collisionSet = 0

The full finite collision locus has measure zero.

def BKAR.Forest.sectorOrderRel {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : Edge V → Edge V → Prop

Auxiliary relation used to compare sector orders. It agrees with descending parameter order on forest edges and only relates off-forest edges to themselves; this makes it globally antisymmetric once collisions are excluded.

Equations

• F.sectorOrderRel u e e' = (e = e' ∨ e ∈ F.edges ∧ e' ∈ F.edges ∧ F.paramValue u e' ≤ F.paramValue u e)

theorem BKAR.Forest.sectorOrderRel_isAntisymm_of_notMem_collisionSet {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {u : F.EdgeParam → ℝ} (hno : u ∉ F.collisionSet) : Std.Antisymm (F.sectorOrderRel u)

theorem BKAR.Forest.pairwise_sectorOrderRel_of_orderedSimplexParams {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (order : List (Edge V)) {top : ℝ} : (∀ e ∈ order, e ∈ F.edges) → OrderedSimplexParams top (List.map (F.paramValue u) order) → List.Pairwise (F.sectorOrderRel u) order

theorem BKAR.Forest.eq_of_mem_orderedCubeSimplex_of_notMem_collisionSet {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order₁ order₂ : List (Edge V)} (horder₁ : order₁ ∈ F.edgeOrders) (horder₂ : order₂ ∈ F.edgeOrders) {u : F.EdgeParam → ℝ} (hno : u ∉ F.collisionSet) (hu₁ : u ∈ F.orderedCubeSimplex order₁) (hu₂ : u ∈ F.orderedCubeSimplex order₂) : order₁ = order₂

Away from collision hyperplanes, membership in two closed ordered sectors forces the two canonical edge orders to be equal.

theorem BKAR.Forest.orderedCubeSimplex_inter_subset_collisionSet_of_ne {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order₁ order₂ : List (Edge V)} (horder₁ : order₁ ∈ F.edgeOrders) (horder₂ : order₂ ∈ F.edgeOrders) (hne : order₁ ≠ order₂) : F.orderedCubeSimplex order₁ ∩ F.orderedCubeSimplex order₂ ⊆ F.collisionSet

Distinct closed ordered cube sectors only overlap on the collision locus.

theorem BKAR.Forest.aedisjoint_orderedCubeSimplex_of_ne {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order₁ order₂ : List (Edge V)} (horder₁ : order₁ ∈ F.edgeOrders) (horder₂ : order₂ ∈ F.edgeOrders) (hne : order₁ ≠ order₂) : MeasureTheory.AEDisjoint MeasureTheory.volume (F.orderedCubeSimplex order₁) (F.orderedCubeSimplex order₂)

Distinct canonical ordered cube sectors are a.e. disjoint.

theorem BKAR.Forest.pairwise_aedisjoint_orderedCubeSimplex {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : Pairwise fun (order₁ order₂ : ↥F.edgeOrders) => MeasureTheory.AEDisjoint MeasureTheory.volume (F.orderedCubeSimplex ↑order₁) (F.orderedCubeSimplex ↑order₂)

The canonical ordered cube sectors are pairwise a.e. disjoint.

theorem BKAR.Forest.measurable_paramValue {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (e : Edge V) : Measurable fun (u : F.EdgeParam → ℝ) => F.paramValue u e

Coordinate lookup as a measurable function on the forest parameter cube.

theorem BKAR.Forest.measurableSet_unitCube {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : MeasurableSet F.unitCube

Measurability of the unit parameter cube.

theorem BKAR.Forest.isCompact_unitCube {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : IsCompact F.unitCube

The forest parameter cube is compact.

theorem BKAR.Forest.measurableSet_orderedSimplexParams_map_paramValue {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) {topFn : (F.EdgeParam → ℝ) → ℝ} : Measurable topFn → MeasurableSet {u : F.EdgeParam → ℝ | OrderedSimplexParams (topFn u) (List.map (F.paramValue u) order)}

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

Each closed ordered cube sector is measurable.

theorem BKAR.Forest.integral_unitCube_eq_tsum_orderedCubeSimplex {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (f : (F.EdgeParam → ℝ) → ℝ) (hfi : MeasureTheory.IntegrableOn f F.unitCube MeasureTheory.volume) : ∫ (u : F.EdgeParam → ℝ) in F.unitCube, f u = ∑' (order : ↥F.edgeOrders), ∫ (u : F.EdgeParam → ℝ) in F.orderedCubeSimplex ↑order, f u

Almost-disjoint integral partition of the unit cube: once the closed sectors are measurable and the integrand is integrable on the cube, the integral over the unit cube is the sum of the sector integrals. The a.e. disjointness comes from the collision-hyperplane theorem above.

theorem BKAR.Forest.integral_unitCube_eq_sum_orderedCubeSimplex {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (f : (F.EdgeParam → ℝ) → ℝ) (hfi : MeasureTheory.IntegrableOn f F.unitCube MeasureTheory.volume) : ∫ (u : F.EdgeParam → ℝ) in F.unitCube, f u = ∑ order : ↥F.edgeOrders, ∫ (u : F.EdgeParam → ℝ) in F.orderedCubeSimplex ↑order, f u

Finite-sum form of Forest.integral_unitCube_eq_tsum_orderedCubeSimplex.