Discharging the analytic side conditions

Shows that the global smoothness hypothesis BKARContDiff implies the analytic side conditions allBranchesAnalytic at every node and depth, and concludes the two root identities of the ordered assembly: ρ at the all-ones configuration equals the sum of all root boundary support/order contributions, with or without the empty sector split off as ρ at the zero configuration.

theorem BKAR.BKARContDiff.allBranchesAnalytic_parameterBound_child {V : Type u_1} [Fintype V] [DecidableEq V] (choices : Forest.ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (htop : 0 ≤ top) (hbound : ∀ t ∈ Set.uIcc 0 top, ∀ (e : F.EdgeParam), t ≤ F.paramsOfOrder pref prefixTs e) (e : ↥F.activeEdges) {t : ℝ} (ht : t ∈ Set.uIcc 0 top) (s : ℝ) : s ∈ Set.uIcc 0 t → ∀ (e' : (choices F e).forest.EdgeParam), s ≤ (choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ [t]) e'

The ordered-parameter bound in allBranchesAnalytic propagates to a child node after appending the active edge parameter.

theorem BKAR.BKARContDiff.allBranchesAnalytic_smooth_obligations {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 ℝ) (top : ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) : (∀ t ∈ Set.uIcc 0 top, DifferentiableAt ℝ (BKAR.mixedPartialList pref.reverse ρ) (F.interpWithFill (F.paramsOfOrder pref prefixTs) t)) ∧ (∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => BKAR.mixedPartialList (e :: pref.reverse) ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) t)) MeasureTheory.volume 0 top) ∧ ∀ (e : ↥F.activeEdges), IntervalIntegrable (fun (t : ℝ) => BKAR.mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ [t])))) MeasureTheory.volume 0 top

The non-recursive smoothness/integrability side conditions in allBranchesAnalytic follow from global C^∞ smoothness of ρ.

theorem BKAR.BKARContDiff.allBranchesAnalytic_of_activeEdges_eq_empty {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 : ℝ) : F.activeEdges = ∅ → (∀ t ∈ Set.uIcc 0 top, ∀ (e : F.EdgeParam), t ≤ F.paramsOfOrder pref prefixTs e) → Forest.allBranchesAnalytic choices n F pref prefixTs top ρ

Terminal recursion nodes satisfy allBranchesAnalytic at every remaining fuel level once the order bound and global smoothness are available.

theorem BKAR.BKARContDiff.allBranchesAnalytic_child_recursive_sum_intervalIntegrable_of_terminalChild {V : Type u_1} [Fintype V] [DecidableEq V] (choices : Forest.ActiveExtensionChoice V) (F : Forest V) (e : ↥F.activeEdges) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hchild : (choices F e).forest.activeEdges = ∅) : IntervalIntegrable (fun (t : ℝ) => ∑ e' ∈ (choices F e).forest.activeEdges.attach, ∫ (s : ℝ) in 0..t, Forest.allBranchesBoundaryExpansion choices (choices (choices F e).forest e').forest.activeEdges.card (choices (choices F e).forest e').forest (pref ++ [↑e] ++ [↑e']) (prefixTs ++ [t] ++ [s]) s ρ) MeasureTheory.volume 0 top

The recursive child-sum integrability clause is automatic when the selected child is already terminal.

theorem BKAR.BKARContDiff.allBranchesBoundaryExpansion_continuous_comp {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) {X : Type u_2} [TopologicalSpace X] {tsPath : X → List ℝ} {topPath : X → ℝ} : ListPathContinuous pref.length tsPath → Continuous topPath → Continuous fun (x : X) => Forest.allBranchesBoundaryExpansion choices n F pref (tsPath x) (topPath x) ρ

The boundary-only all-branches expansion is continuous along any fixed-length coordinatewise-continuous parameter-list path.

theorem BKAR.BKARContDiff.allBranchesAnalytic_child_recursive_sum_intervalIntegrable {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) (F : Forest V) (e : ↥F.activeEdges) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (hprefixTs : prefixTs.length = pref.length) : IntervalIntegrable (fun (t : ℝ) => ∑ e' ∈ (choices F e).forest.activeEdges.attach, ∫ (s : ℝ) in 0..t, Forest.allBranchesBoundaryExpansion choices (choices (choices F e).forest e').forest.activeEdges.card (choices (choices F e).forest e').forest (pref ++ [↑e] ++ [↑e']) (prefixTs ++ [t] ++ [s]) s ρ) MeasureTheory.volume 0 top

The recursive child-sum integrability clause in allBranchesAnalytic follows from global smoothness of ρ.

theorem BKAR.BKARContDiff.allBranchesAnalytic_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 : ℝ) : pref.toFinset = F.edges → prefixTs.length = pref.length → 0 ≤ top → (∀ t ∈ Set.uIcc 0 top, ∀ (e : F.EdgeParam), t ≤ F.paramsOfOrder pref prefixTs e) → Forest.allBranchesAnalytic choices n F pref prefixTs top ρ

Global recursive discharge of the allBranchesAnalytic predicate from C^∞ smoothness of ρ and the ordered-parameter bound carried by the recursion node.

theorem BKAR.BKARContDiff.allBranchesAnalytic_empty_of_contDiff {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) : Forest.allBranchesAnalytic choices (Forest.empty V).activeEdges.card (Forest.empty V) [] [] 1 ρ

Root all-branches analytic hypothesis, discharged from BKARContDiff.

theorem BKAR.BKARContDiff.oneConfig_eq_zeroConfig_add_nonemptyTreeSum_of_contDiff {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) : ρ 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 both the analytic recursion predicate and the nontrivial fiber-integrability predicate discharged by BKARContDiff.

theorem BKAR.BKARContDiff.rho_oneConfig_eq_sum_rootBoundarySupportOrderContribution_of_contDiff {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) : ρ oneConfig = ∑ I : ForestIndex V, ∑ order ∈ Forest.edgeSetOrders I.edges, Forest.rootBoundarySupportOrderContribution choices ρ I order

Final-shaped root BKAR identity with the empty support/order sector packaged inside rootBoundarySupportOrderContribution.