Continuity of sector parametrizations

Continuity and integrability facts for the cube-coordinate parametrization paramsOfOrder of ordered sectors: continuity in the simplex parameters, continuity after appending one edge, and interval-integrability of the mixed-partial integrand along the appended coordinate. Analytic input for converting nested simplex integrals into sector set integrals.

theorem BKAR.Forest.paramsOfOrder_continuous_of_listPathContinuous {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (order : List (Edge V)) {X : Type u_2} [TopologicalSpace X] {n : ℕ} {tsPath : X → List ℝ} (hts : ListPathContinuous n tsPath) : Continuous fun (x : X) => F.paramsOfOrder order (tsPath x)

theorem BKAR.Forest.EdgeExtension.paramsOfOrder_append_singleton_continuous {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} (h : F.EdgeExtension F' e) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) : Continuous fun (t : ℝ) => F'.paramsOfOrder (pref ++ [e]) (prefixTs ++ [t])

theorem BKAR.BKARContDiff.mixedPartialList_standardInterp_paramsOfOrder_append_singleton_intervalIntegrable {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} {F F' : Forest V} {e : Edge V} (hρ : BKARContDiff ρ) (es : List (Edge V)) (h : F.EdgeExtension F' e) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => BKAR.mixedPartialList es ρ (F'.standardInterp (F'.paramsOfOrder (pref ++ [e]) (prefixTs ++ [t])))) MeasureTheory.volume a b