Composition of a Step Sum with a Zero-Preserving Function

This finite-sum lemma states that a function fixing zero commutes with the step sum associated with a strictly increasing partition.

Let $\pi:\operatorname{Fin}(M+1)\to\mathbb R$ be strictly monotone, let $f:\operatorname{Fin}(M)\to\mathbb R$, let $s\in\mathbb R$, and let $g:\mathbb R\to\mathbb R$ satisfy $g(0)=0$. Then

Because the partition is strictly increasing, at most one step is active. The lemma is useful for passing powers and other zero-preserving operations through elementary-integrand evaluations.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.

theorem comp_sum_ite {M : ℕ} {π : Fin (M + 1) → ℝ} (hπ : StrictMono π)
    (f : Fin M → ℝ) (s : ℝ) (g : ℝ → ℝ) (hg0 : g 0 = 0) :
    g (∑ j : Fin M, if π j.castSucc < s ∧ s ≤ π j.succ then f j else 0)
      = ∑ j : Fin M, if π j.castSucc < s ∧ s ≤ π j.succ then g (f j) else 0

Module navigation

Module: LevyStochCalc/Brownian/ItoFourthMomentLintegral.

Next: abs_clamp_sub_le.

Source excerpt, lines 27–30 · Frozen source 408915f.