Nested integrals over ordered simplices

Defines the nested interval integral orderedSimplexIntegral over the ordered simplex 0 ≤ tₙ ≤ … ≤ t₂ ≤ t₁ ≤ top attached to a list of edges, and the predicate OrderedSimplexParams describing its parameter lists. These nested one-dimensional integrals are the raw form in which the ordered expansion of the BKAR forest interpolation formula (see BKAR.Formula) first produces its remainder terms.

def BKAR.orderedSimplexIntegralAux {V : Type u_1} (top : ℝ) : List (Edge V) → (List ℝ → ℝ) → ℝ

Nested interval integral over the ordered simplex associated to an edge order.

The list of real parameters supplied to the integrand is in the same order as the edge list. If order = [e₁, e₂, ...], then the bounds are 0 ≤ tₙ ≤ ... ≤ t₂ ≤ t₁ ≤ top.

Equations

• BKAR.orderedSimplexIntegralAux top [] x✝ = x✝ []
• BKAR.orderedSimplexIntegralAux top (head :: order) x✝ = ∫ (t : ℝ) in 0..top, BKAR.orderedSimplexIntegralAux t order fun (ts : List ℝ) => x✝ (t :: ts)

noncomputable def BKAR.orderedSimplexIntegral {V : Type u_1} (order : List (Edge V)) (f : List ℝ → ℝ) : ℝ

Nested interval integral over the ordered simplex with outer bound 1.

Equations

• BKAR.orderedSimplexIntegral order f = BKAR.orderedSimplexIntegralAux 1 order f

def BKAR.OrderedSimplexParams : ℝ → List ℝ → Prop

Predicate saying that a parameter list lies in the ordered simplex with outer bound top: 0 ≤ tₙ ≤ ... ≤ t₂ ≤ t₁ ≤ top.

Equations

• BKAR.OrderedSimplexParams x✝ [] = True
• BKAR.OrderedSimplexParams x✝ (t :: ts) = (0 ≤ t ∧ t ≤ x✝ ∧ BKAR.OrderedSimplexParams t ts)

@[simp]

theorem BKAR.orderedSimplexIntegralAux_nil {V : Type u_1} (top : ℝ) (f : List ℝ → ℝ) : orderedSimplexIntegralAux top [] f = f []

@[simp]

theorem BKAR.orderedSimplexIntegralAux_cons {V : Type u_1} (top : ℝ) (e : Edge V) (order : List (Edge V)) (f : List ℝ → ℝ) : orderedSimplexIntegralAux top (e :: order) f = ∫ (t : ℝ) in 0..top, orderedSimplexIntegralAux t order fun (ts : List ℝ) => f (t :: ts)

@[simp]

theorem BKAR.orderedSimplexIntegral_nil {V : Type u_1} (f : List ℝ → ℝ) : orderedSimplexIntegral [] f = f []

@[simp]

theorem BKAR.orderedSimplexIntegral_cons {V : Type u_1} (e : Edge V) (order : List (Edge V)) (f : List ℝ → ℝ) : orderedSimplexIntegral (e :: order) f = ∫ (t : ℝ) in 0..1, orderedSimplexIntegralAux t order fun (ts : List ℝ) => f (t :: ts)

theorem BKAR.orderedSimplexIntegral_singleton {V : Type u_1} (e : Edge V) (f : List ℝ → ℝ) : orderedSimplexIntegral [e] f = ∫ (t : ℝ) in 0..1, f [t]

theorem BKAR.orderedSimplexIntegral_pair {V : Type u_1} (e₁ e₂ : Edge V) (f : List ℝ → ℝ) : orderedSimplexIntegral [e₁, e₂] f = ∫ (t₁ : ℝ) in 0..1, ∫ (t₂ : ℝ) in 0..t₁, f [t₁, t₂]

@[simp]

theorem BKAR.orderedSimplexParams_nil (top : ℝ) : OrderedSimplexParams top []

@[simp]

theorem BKAR.orderedSimplexParams_cons (top t : ℝ) (ts : List ℝ) : OrderedSimplexParams top (t :: ts) ↔ 0 ≤ t ∧ t ≤ top ∧ OrderedSimplexParams t ts

theorem BKAR.OrderedSimplexParams.head_nonneg {top t : ℝ} {ts : List ℝ} (h : OrderedSimplexParams top (t :: ts)) : 0 ≤ t

theorem BKAR.OrderedSimplexParams.head_le_top {top t : ℝ} {ts : List ℝ} (h : OrderedSimplexParams top (t :: ts)) : t ≤ top

theorem BKAR.OrderedSimplexParams.tail {top t : ℝ} {ts : List ℝ} (h : OrderedSimplexParams top (t :: ts)) : OrderedSimplexParams t ts

theorem BKAR.OrderedSimplexParams.nonneg_of_mem {top : ℝ} {ts : List ℝ} {t : ℝ} : OrderedSimplexParams top ts → t ∈ ts → 0 ≤ t

theorem BKAR.OrderedSimplexParams.le_top_of_mem {top : ℝ} {ts : List ℝ} {t : ℝ} : OrderedSimplexParams top ts → t ∈ ts → t ≤ top

theorem BKAR.OrderedSimplexParams.le_head_of_mem_tail {top t s : ℝ} {ts : List ℝ} (h : OrderedSimplexParams top (t :: ts)) (hs : s ∈ ts) : s ≤ t

theorem BKAR.orderedSimplexIntegralAux_congr {V : Type u_1} (top : ℝ) (order : List (Edge V)) {f g : List ℝ → ℝ} : (∀ (ts : List ℝ), f ts = g ts) → orderedSimplexIntegralAux top order f = orderedSimplexIntegralAux top order g

theorem BKAR.orderedSimplexIntegral_congr {V : Type u_1} {order : List (Edge V)} {f g : List ℝ → ℝ} (hfg : ∀ (ts : List ℝ), f ts = g ts) : orderedSimplexIntegral order f = orderedSimplexIntegral order g

theorem BKAR.orderedSimplexIntegralAux_congr_of_length {V : Type u_1} (top : ℝ) (order : List (Edge V)) {f g : List ℝ → ℝ} : (∀ (ts : List ℝ), ts.length = order.length → f ts = g ts) → orderedSimplexIntegralAux top order f = orderedSimplexIntegralAux top order g

Congruence for nested simplex integrals when the integrands agree on parameter lists whose length matches the remaining edge order.

theorem BKAR.orderedSimplexIntegral_congr_of_length {V : Type u_1} {order : List (Edge V)} {f g : List ℝ → ℝ} (hfg : ∀ (ts : List ℝ), ts.length = order.length → f ts = g ts) : orderedSimplexIntegral order f = orderedSimplexIntegral order g

Unit-bound version of orderedSimplexIntegralAux_congr_of_length.