From cube contributions to ordered sector contributions

Under the global smoothness hypothesis, the integrand of a forest's cube contribution is continuous, hence integrable on the compact unit cube, and the unit-cube partition step applies: the order-free cube contribution of the BKAR forest interpolation formula (see BKAR.Formula) equals the finite sum of its closed ordered sector contributions, with sector overlaps null by the collision-hyperplane theorem.

theorem BKAR.Forest.continuous_cubeContributionIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : Continuous fun (u : F.EdgeParam → ℝ) => F.mixedPartial ρ (F.standardInterp u)

Continuity of the usual unordered cube integrand under the BKAR smoothness hypothesis.

theorem BKAR.Forest.integrableOn_cubeContributionIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : MeasureTheory.IntegrableOn (fun (u : F.EdgeParam → ℝ) => F.mixedPartial ρ (F.standardInterp u)) F.unitCube MeasureTheory.volume

Integrability of the usual unordered cube integrand on the forest parameter cube.

theorem BKAR.Forest.cubeContribution_eq_sum_orderedCubeSimplex_mixedPartial {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : F.cubeContribution ρ = ∑ order : ↥F.edgeOrders, ∫ (u : F.EdgeParam → ℝ) in F.orderedCubeSimplex ↑order, F.mixedPartial ρ (F.standardInterp u)

The unit-cube partition step for the usual unordered forest contribution: the integral over [0,1]^{E(F)} is the finite sum of its closed ordered sectors; sector overlaps are null by the collision-hyperplane theorem.

theorem BKAR.Forest.continuous_orderedCubeSectorIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : Continuous fun (u : F.EdgeParam → ℝ) => mixedPartialList order.reverse ρ (F.standardInterp u)

Continuity of an ordered-sector integrand under the BKAR smoothness hypothesis.

theorem BKAR.Forest.integrableOn_orderedCubeSectorIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : MeasureTheory.IntegrableOn (fun (u : F.EdgeParam → ℝ) => mixedPartialList order.reverse ρ (F.standardInterp u)) F.unitCube MeasureTheory.volume

Integrability of an ordered-sector integrand on the forest parameter cube.

theorem BKAR.Forest.orderedCubeSectorContribution_eq_integral_mixedPartial {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : F.orderedCubeSectorContribution order ρ = ∫ (u : F.EdgeParam → ℝ) in F.orderedCubeSimplex order, F.mixedPartial ρ (F.standardInterp u)

On a canonical ordered sector, the order-specific recursive mixed partial is the same as the unordered forest mixed partial. This is the analytic half of the sector-to-cube bridge.

theorem BKAR.Forest.cubeContribution_eq_sum_orderedCubeSectorContribution {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : F.cubeContribution ρ = ∑ order ∈ F.edgeOrders, F.orderedCubeSectorContribution order ρ

The unit-cube partition step plus mixed-partial order independence: the usual unordered cube contribution is the sum of the order-specific closed cube-sector contributions.