Canonicalizing the sector integrands

Rewrites each root support/order fiber as the closed ordered cube-sector integral of the forest grown by that order, and shows that the sector integrand depends only on the canonical data of the support: the grown-forest sector contributions agree with those of the canonical representative.

theorem BKAR.Forest.OrderedGrowth.orderedCubeSectorContribution_eq_integral_branchIntegrand_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] {G : Forest V} {order : List (Edge V)} (growth : (empty V).OrderedGrowth order G) (ρ : (Edge V → ℝ) → ℝ) : G.orderedCubeSectorContribution order ρ = ∫ (ts : Fin order.length → ℝ) in orderedFinSimplex order.length, growth.branchIntegrand emptyParam ρ (List.ofFn ts)

An empty-start ordered-growth sector can be read directly as a finite ordered simplex integral of the branch integrand carried by the growth certificate.

theorem BKAR.Forest.orderedSectorContribution_eq_integral_branchIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ρ : (Edge V → ℝ) → ℝ) : (grownForestForSupportOrder choices I order).orderedCubeSectorContribution (↑order) ρ = ∫ (ts : Fin (↑order).length → ℝ) in orderedFinSimplex (↑order).length, (grownForestForSupportOrderGrowth choices I order).branchIntegrand emptyParam ρ (List.ofFn ts)

Finite-sector normal form for the grown support/order forest, expressed via its concrete chosen-growth branch integrand.

theorem BKAR.Forest.orderedSectorContribution_eq_orderedFinSimplexIntegral {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ρ : (Edge V → ℝ) → ℝ) : (grownForestForSupportOrder choices I order).orderedCubeSectorContribution (↑order) ρ = ∫ (ts : Fin (↑order).length → ℝ) in orderedFinSimplex (↑order).length, mixedPartialList (↑order).reverse ρ ((grownForestForSupportOrder choices I order).standardInterp (((grownForestForSupportOrder choices I order).orderMeasurableEquivOfOrder ⋯).symm ts))

Finite-coordinate form of the grown support/order cube sector, written directly with the grown forest's ordered-sector integrand.

theorem BKAR.Forest.rootContribution_eq_orderedSectorContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : rootBoundarySupportOrderContribution choices ρ I ↑order = (grownForestForSupportOrder choices I order).orderedCubeSectorContribution (↑order) ρ

Per-sector simplex-to-cube-sector bridge for the root support/order fiber: the recursive ordered simplex contribution is the corresponding closed cube-sector integral of the Forest representative grown by following that same support order.

theorem BKAR.Forest.canonicalSectorContribution_eq_integral_branchIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : (canonicalGrownForestForSupport choices I).orderedCubeSectorContribution (↑I.canonicalOrder) ρ = ∫ (ts : Fin (↑I.canonicalOrder).length → ℝ) in orderedFinSimplex (↑I.canonicalOrder).length, (canonicalGrownForestForSupportGrowth choices I).branchIntegrand emptyParam ρ (List.ofFn ts)

Finite-sector normal form for the canonical grown representative in its canonical order.

theorem BKAR.Forest.canonicalSectorContribution_eq_orderedFinSimplexIntegral {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ρ : (Edge V → ℝ) → ℝ) : (canonicalGrownForestForSupport choices I).orderedCubeSectorContribution (↑order) ρ = ∫ (ts : Fin (↑order).length → ℝ) in orderedFinSimplex (↑order).length, mixedPartialList (↑order).reverse ρ ((canonicalGrownForestForSupport choices I).standardInterp (((canonicalGrownForestForSupport choices I).orderMeasurableEquivOfOrder ⋯).symm ts))

Finite-coordinate form of the canonical grown representative's sector for an arbitrary order of the same support.

theorem BKAR.Forest.grownForestForSupportOrder_standardInterp_orderMeasurableEquiv_symm_eq_canonical {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ts : Fin (↑order).length → ℝ) : (grownForestForSupportOrder choices I order).standardInterp (((grownForestForSupportOrder choices I order).orderMeasurableEquivOfOrder ⋯).symm ts) = (canonicalGrownForestForSupport choices I).standardInterp (((canonicalGrownForestForSupport choices I).orderMeasurableEquivOfOrder ⋯).symm ts)

The grown forest for a support/order and the canonical grown representative have the same finite-coordinate interpolation point on that support/order sector.

theorem BKAR.Forest.grownForestForSupportOrder_orderedFinSectorIntegrand_eq_canonical {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ρ : (Edge V → ℝ) → ℝ) (ts : Fin (↑order).length → ℝ) : mixedPartialList (↑order).reverse ρ ((grownForestForSupportOrder choices I order).standardInterp (((grownForestForSupportOrder choices I order).orderMeasurableEquivOfOrder ⋯).symm ts)) = mixedPartialList (↑order).reverse ρ ((canonicalGrownForestForSupport choices I).standardInterp (((canonicalGrownForestForSupport choices I).orderMeasurableEquivOfOrder ⋯).symm ts))

Pointwise finite-sector integrands agree after replacing the support/order grown forest by the canonical grown representative.

theorem BKAR.Forest.grownForestForSupportOrder_orderedCubeSectorContribution_eq_canonical {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : ↥(edgeSetOrders I.edges)) (ρ : (Edge V → ℝ) → ℝ) : (grownForestForSupportOrder choices I order).orderedCubeSectorContribution (↑order) ρ = (canonicalGrownForestForSupport choices I).orderedCubeSectorContribution (↑order) ρ

Sectorwise canonicalization: the closed cube-sector contribution of the Forest representative grown by a support/order equals the same ordered sector of the canonical grown representative for that support.