Integrability of the boundary fibers

Under the global smoothness hypothesis, the local boundary support/order contributions are continuous and interval-integrable, and the boundary tree fibers satisfy the integrability certificates required to exchange integrals and finite sums in the telescoping argument. Produces the split form of the identity: ρ at the all-ones configuration equals ρ at zero plus the sum of the nonempty-support fibers.

theorem BKAR.BKARContDiff.localBoundarySupportOrderContribution_continuous {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (I : ForestIndex V) (order : List (Edge V)) : Continuous fun (top : ℝ) => Forest.localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ

The local support/order first-boundary fiber is continuous as a function of its outer upper bound.

theorem BKAR.BKARContDiff.localBoundarySupportOrderContribution_intervalIntegrable {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (I : ForestIndex V) (order : List (Edge V)) (a b : ℝ) : IntervalIntegrable (fun (top : ℝ) => Forest.localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ) MeasureTheory.volume a b

The local support/order first-boundary fiber is interval-integrable in its outer upper bound.

theorem BKAR.BKARContDiff.localBoundarySupportOrderContribution_continuous_comp {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) {X : Type u_2} [TopologicalSpace X] {tsPath : X → List ℝ} {topPath : X → ℝ} (hts : ListPathContinuous pref.length tsPath) (htop : Continuous topPath) (I : ForestIndex V) (order : List (Edge V)) : Continuous fun (x : X) => Forest.localBoundarySupportOrderContribution choices F pref (tsPath x) (topPath x) I order ρ

The local support/order first-boundary fiber is continuous along any fixed-length coordinatewise-continuous parameter-list path.

theorem BKAR.BKARContDiff.boundarySupportOrderTreeFiber_continuous_comp_of_order_length_eq_pref_length_add {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) (k : ℕ) (F : Forest V) (pref : List (Edge V)) {X : Type u_2} [TopologicalSpace X] {tsPath : X → List ℝ} {topPath : X → ℝ} : ListPathContinuous pref.length tsPath → Continuous topPath → ∀ (I : ForestIndex V) (order : List (Edge V)), order.length = pref.length + k → Continuous fun (x : X) => Forest.boundarySupportOrderTreeFiber choices F pref (tsPath x) (topPath x) I order ρ

Finite-depth continuity of folded support/order fibers along any recursively generated diagonal parameter-list path.

theorem BKAR.BKARContDiff.boundarySupportOrderTreeFiber_intervalIntegrable_of_order_length_eq_pref_length_add {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) (k : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (I : ForestIndex V) (order : List (Edge V)) (top : ℝ) (hprefixTs : prefixTs.length = pref.length) (hlen : order.length = pref.length + k) : IntervalIntegrable (fun (t : ℝ) => Forest.boundarySupportOrderTreeFiber choices F pref prefixTs t I order ρ) MeasureTheory.volume 0 top

Finite-depth interval-integrability of folded support/order fibers.

theorem BKAR.BKARContDiff.boundarySupportOrderTreeFiberNontrivialIntegrable_of_contDiff {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) : prefixTs.length = pref.length → Forest.boundarySupportOrderTreeFiberNontrivialIntegrable choices n F pref prefixTs top ρ

The narrowed nontrivial support/order fiber-integrability predicate follows from global C^∞ smoothness.

theorem BKAR.BKARContDiff.oneConfig_eq_zeroConfig_add_nonemptyTreeSum_of_contDiff_of_analytic {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) (hanalytic : Forest.allBranchesAnalytic choices (Forest.empty V).activeEdges.card (Forest.empty V) [] [] 1 ρ) : ρ oneConfig = ρ zeroConfig + ∑ I : ForestIndex V with I.edges ≠ ∅, ∑ order ∈ Forest.edgeSetOrders I.edges, Forest.boundarySupportOrderTreeFiber choices (Forest.empty V) [] [] 1 I order ρ

Final flattened root identity with the fiber-integrability obligation discharged by BKARContDiff. The remaining analytic input is the all-branches induction hypothesis.