Simplex-sector conversion: arbitrary order

The general case of the simplex-sector conversion. Develops the standard ordered simplices in Fin n → ℝ (measurability, compactness, head/tail decomposition), transports set integrals over ordered cube sectors through the ordered coordinate equivalences, proves that for continuous integrands the recursive nested simplex integral equals the set integral over the closed finite ordered simplex, and concludes that under the global smoothness hypothesis every recursive ordered contribution equals the corresponding closed ordered cube-sector contribution.

theorem BKAR.Forest.measurableSet_orderedSimplexParams_map {α : Type u_2} [MeasurableSpace α] (fs : List (α → ℝ)) {topFn : α → ℝ} : Measurable topFn → (∀ f ∈ fs, Measurable f) → MeasurableSet {x : α | OrderedSimplexParams (topFn x) (List.map (fun (f : α → ℝ) => f x) fs)}

Generic measurability of an ordered-simplex predicate evaluated on a finite list of measurable real-valued coordinate functions.

theorem BKAR.Forest.isClosed_orderedSimplexParams_map {α : Type u_2} [TopologicalSpace α] (fs : List (α → ℝ)) {topFn : α → ℝ} : Continuous topFn → (∀ f ∈ fs, Continuous f) → IsClosed {x : α | OrderedSimplexParams (topFn x) (List.map (fun (f : α → ℝ) => f x) fs)}

Closedness of an ordered-simplex predicate evaluated on a finite list of continuous real-valued coordinate functions.

theorem BKAR.Forest.measurableSet_orderedSimplexParams_ofFn (n : ℕ) : MeasurableSet {ts : Fin n → ℝ | OrderedSimplexParams 1 (List.ofFn ts)}

The ordered-simplex predicate on Fin n coordinate tuples is measurable.

def BKAR.Forest.orderedFinSimplexWithTop (top : ℝ) (n : ℕ) : Set (Fin n → ℝ)

The finite ordered simplex with a variable upper bound. This is the induction invariant for the ordered-simplex/Fubini bridge.

Equations

• BKAR.Forest.orderedFinSimplexWithTop top n = {ts : Fin n → ℝ | BKAR.OrderedSimplexParams top (List.ofFn ts)}

theorem BKAR.Forest.measurableSet_orderedFinSimplexWithTop (top : ℝ) (n : ℕ) : MeasurableSet (orderedFinSimplexWithTop top n)

Variable-top finite ordered simplexes are measurable.

theorem BKAR.Forest.isClosed_orderedFinSimplexWithTop (top : ℝ) (n : ℕ) : IsClosed (orderedFinSimplexWithTop top n)

Variable-top finite ordered simplexes are closed.

theorem BKAR.Forest.orderedFinSimplexWithTop_subset_pi_Icc (top : ℝ) (n : ℕ) : orderedFinSimplexWithTop top n ⊆ Set.univ.pi fun (x : Fin n) => Set.Icc 0 top

A variable-top finite ordered simplex is contained in the coordinate box [0, top]^n.

theorem BKAR.Forest.isCompact_orderedFinSimplexWithTop (top : ℝ) (n : ℕ) : IsCompact (orderedFinSimplexWithTop top n)

Variable-top finite ordered simplexes are compact.

theorem BKAR.Forest.integrableOn_orderedFinSimplexWithTop_of_continuous {top : ℝ} {n : ℕ} {G : (Fin n → ℝ) → ℝ} (hG : Continuous G) : MeasureTheory.IntegrableOn G (orderedFinSimplexWithTop top n) MeasureTheory.volume

Continuous functions are integrable on variable-top finite ordered simplexes.

theorem BKAR.Forest.orderedFinSimplex_eq_orderedFinSimplexWithTop_one (n : ℕ) : orderedFinSimplex n = orderedFinSimplexWithTop 1 n

The original finite sector is the variable-top simplex with top 1.

theorem BKAR.Forest.mem_orderedFinSimplexWithTop_succ_iff (top : ℝ) {n : ℕ} (ts : Fin (n + 1) → ℝ) : ts ∈ orderedFinSimplexWithTop top (n + 1) ↔ 0 ≤ ts 0 ∧ ts 0 ≤ top ∧ Fin.tail ts ∈ orderedFinSimplexWithTop (ts 0) n

Head-tail membership characterization for the variable-top finite simplex.

def BKAR.Forest.orderedFinSimplexHeadTail (top : ℝ) (n : ℕ) : Set (ℝ × (Fin n → ℝ))

The head-tail form of the variable-top ordered simplex in product coordinates. The first coordinate is the outer simplex variable and the second coordinate is the tail tuple.

Equations

• BKAR.Forest.orderedFinSimplexHeadTail top n = {z : ℝ × (Fin n → ℝ) | z.1 ∈ Set.Icc 0 top ∧ z.2 ∈ BKAR.Forest.orderedFinSimplexWithTop z.1 n}

theorem BKAR.Forest.measurableSet_orderedFinSimplexHeadTail (top : ℝ) (n : ℕ) : MeasurableSet (orderedFinSimplexHeadTail top n)

The head-tail ordered simplex sector is measurable.

theorem BKAR.Forest.orderedFinSimplexWithTop_succ_eq_piFinSuccAbove_preimage_headTail (top : ℝ) (n : ℕ) : orderedFinSimplexWithTop top (n + 1) = ⇑(MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => ℝ) 0) ⁻¹' orderedFinSimplexHeadTail top n

The piFinSuccAbove coordinate split identifies the (n+1)-dimensional ordered simplex with its head-tail product-coordinate sector.

theorem BKAR.Forest.setIntegral_orderedFinSimplexWithTop_succ_eq_headTail (top : ℝ) (n : ℕ) (f : (Fin (n + 1) → ℝ) → ℝ) : ∫ (ts : Fin (n + 1) → ℝ) in orderedFinSimplexWithTop top (n + 1), f ts = ∫ (z : ℝ × (Fin n → ℝ)) in orderedFinSimplexHeadTail top n, f ((MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => ℝ) 0).symm z)

Measure transport from the (n+1)-coordinate finite simplex to its explicit head-tail sector.

theorem BKAR.Forest.setIntegral_orderedFinSimplexHeadTail_eq_iterated_Icc (top : ℝ) (n : ℕ) (f : ℝ × (Fin n → ℝ) → ℝ) (hf : MeasureTheory.IntegrableOn f (orderedFinSimplexHeadTail top n) MeasureTheory.volume) : ∫ (z : ℝ × (Fin n → ℝ)) in orderedFinSimplexHeadTail top n, f z = ∫ (t : ℝ) in Set.Icc 0 top, ∫ (us : Fin n → ℝ) in orderedFinSimplexWithTop t n, f (t, us)

Fubini split for the head-tail finite ordered simplex sector.

theorem BKAR.Forest.piFinSuccAbove_zero_symm_apply {n : ℕ} (t : ℝ) (us : Fin n → ℝ) : (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => ℝ) 0).symm (t, us) = Fin.cons t us

At coordinate 0, the inverse head-tail split is just Fin.cons.

theorem BKAR.Forest.setIntegral_orderedFinSimplexWithTop_succ_eq_iterated_Icc (top : ℝ) (n : ℕ) (f : (Fin (n + 1) → ℝ) → ℝ) (hf : MeasureTheory.IntegrableOn f (orderedFinSimplexWithTop top (n + 1)) MeasureTheory.volume) : ∫ (ts : Fin (n + 1) → ℝ) in orderedFinSimplexWithTop top (n + 1), f ts = ∫ (t : ℝ) in Set.Icc 0 top, ∫ (us : Fin n → ℝ) in orderedFinSimplexWithTop t n, f (Fin.cons t us)

Fubini split for the finite ordered simplex in (n+1) coordinates.

theorem BKAR.Forest.setIntegral_orderedFinSimplexWithTop_succ_eq_iterated_interval {top : ℝ} (htop : 0 ≤ top) (n : ℕ) (f : (Fin (n + 1) → ℝ) → ℝ) (hf : MeasureTheory.IntegrableOn f (orderedFinSimplexWithTop top (n + 1)) MeasureTheory.volume) : ∫ (ts : Fin (n + 1) → ℝ) in orderedFinSimplexWithTop top (n + 1), f ts = ∫ (t : ℝ) in 0..top, ∫ (us : Fin n → ℝ) in orderedFinSimplexWithTop t n, f (Fin.cons t us)

Interval-integral form of the one-step finite ordered-simplex Fubini split.

theorem BKAR.Forest.measurableSet_orderedFinSimplex (n : ℕ) : MeasurableSet (orderedFinSimplex n)

The finite ordered simplex sector in coordinate space is measurable.

theorem BKAR.Forest.ofFn_getD_eq_of_length {n : ℕ} (ts : List ℝ) (hlen : ts.length = n) : (List.ofFn fun (i : Fin n) => ts.getD (↑i) 0) = ts

A list of the right length is recovered from its getD finite tuple.

theorem BKAR.Forest.finCons_getD_cons_of_length {n : ℕ} (t : ℝ) (ts : List ℝ) (hlen : ts.length = n) : (fun (i : Fin (n + 1)) => (t :: ts).getD (↑i) 0) = Fin.cons t fun (i : Fin n) => ts.getD (↑i) 0

A consed list, read through getD, is the corresponding Fin.cons tuple.

theorem BKAR.Forest.paramsOfOrder_eq_orderMeasurableEquiv_symm_getD_of_length {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (ts : List ℝ) (hlen : ts.length = order.length) : F.paramsOfOrder order ts = (F.orderMeasurableEquivOfOrder horder).symm fun (i : Fin order.length) => ts.getD (↑i) 0

For parameter lists of the correct length, paramsOfOrder is exactly the inverse ordered-coordinate map applied to the corresponding Fin tuple.

theorem BKAR.Forest.orderedContribution_eq_orderedSimplexIntegral_orderMeasurableEquiv_symm {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (ρ : (Edge V → ℝ) → ℝ) : F.orderedContribution order ρ = orderedSimplexIntegral order fun (ts : List ℝ) => mixedPartialList order.reverse ρ (F.standardInterp ((F.orderMeasurableEquivOfOrder horder).symm fun (i : Fin order.length) => ts.getD (↑i) 0))

Recursive ordered contributions, rewritten with the same finite coordinates used on the cube-sector side.

theorem BKAR.Forest.setIntegral_orderedCubeSimplex_eq_orderedFinSimplex_symm {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (g : (F.EdgeParam → ℝ) → ℝ) : ∫ (u : F.EdgeParam → ℝ) in F.orderedCubeSimplex order, g u = ∫ (ts : Fin order.length → ℝ) in orderedFinSimplex order.length, g ((F.orderMeasurableEquivOfOrder horder).symm ts)

Measure transport for arbitrary canonical orders, now for integrands written on forest cube coordinates. This is the sector-side form needed by the final simplex-sector conversion theorem.

theorem BKAR.Forest.orderedCubeSectorContribution_eq_orderedFinSimplexIntegral {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (ρ : (Edge V → ℝ) → ℝ) : F.orderedCubeSectorContribution order ρ = ∫ (ts : Fin order.length → ℝ) in orderedFinSimplex order.length, mixedPartialList order.reverse ρ (F.standardInterp ((F.orderMeasurableEquivOfOrder horder).symm ts))

Arbitrary-order cube-sector contribution in finite ordered coordinates.

theorem BKAR.Forest.integrableOn_orderedFinSimplex_orderedCubeSectorIntegrand {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : MeasureTheory.IntegrableOn (fun (ts : Fin order.length → ℝ) => mixedPartialList order.reverse ρ (F.standardInterp ((F.orderMeasurableEquivOfOrder horder).symm ts))) (orderedFinSimplex order.length) MeasureTheory.volume

The actual BKAR sector integrand is integrable on the finite ordered simplex under the global smoothness hypothesis.

theorem BKAR.Forest.orderedSimplexIntegralAux_eq_setIntegral_orderedFinSimplexWithTop_of_continuous {V : Type u_1} {top : ℝ} (htop : 0 ≤ top) (order : List (Edge V)) (G : (Fin order.length → ℝ) → ℝ) : Continuous G → (orderedSimplexIntegralAux top order fun (ts : List ℝ) => G fun (i : Fin order.length) => ts.getD (↑i) 0) = ∫ (xs : Fin order.length → ℝ) in orderedFinSimplexWithTop top order.length, G xs

Finite-dimensional analytic core of the simplex-sector conversion: for continuous integrands, the recursive ordered simplex integral is the set integral over the closed finite ordered simplex with the same top bound.

theorem BKAR.Forest.orderedSimplexIntegral_eq_setIntegral_orderedFinSimplex_of_continuous {V : Type u_1} (order : List (Edge V)) (G : (Fin order.length → ℝ) → ℝ) (hG : Continuous G) : (orderedSimplexIntegral order fun (ts : List ℝ) => G fun (i : Fin order.length) => ts.getD (↑i) 0) = ∫ (xs : Fin order.length → ℝ) in orderedFinSimplex order.length, G xs

Unit-bound finite-dimensional analytic core of the simplex-sector conversion.

theorem BKAR.Forest.orderedContribution_eq_orderedCubeSectorContribution_of_contDiff {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : F.orderedContribution order ρ = F.orderedCubeSectorContribution order ρ

Arbitrary finite-order simplex-sector conversion: under the global BKAR smoothness hypothesis, the recursive ordered contribution equals the corresponding closed ordered cube-sector contribution.