The cube contribution of a forest index

Defines ForestIndex.cubeContribution, the ordinary cube contribution attached to an abstract forest index — the integral over [0,1]^{E(F)} of the forest mixed partial at the interpolated point — realized through a canonical grown forest and independent of the active-extension choice system used to realize it. This is the right-hand side of the flagship form of the BKAR forest interpolation formula (see BKAR.Formula).

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

The ordinary cube contribution attached to an abstract forest index.

The value is independent of the active-extension choice system used to realize the support as a Forest representative. Such a system exists for every finite vertex type.

Equations

• I.cubeContribution ρ = (BKAR.Forest.canonicalGrownForestForSupport (Classical.choice ⋯) I).cubeContribution ρ

theorem BKAR.ForestIndex.cubeContribution_eq_canonicalGrownForestForSupport {V : Type u_1} [Fintype V] [DecidableEq V] (I : ForestIndex V) (choices : Forest.ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : I.cubeContribution ρ = (Forest.canonicalGrownForestForSupport choices I).cubeContribution ρ

Any concrete active-extension choice system realizes the same abstract forest-index cube contribution.