integralSum — Mathlib

English

If f =Θ[l] g then f ∘ Prod.snd = Θ[l' ×ˢ l] g ∘ Prod.snd.

Русский

Если f =Θ[l] g, то f ∘ Prod.snd = Θ[l' ×ˢ l] g ∘ Prod.snd.

LaTeX

$$$\forall f,g:\; f =Θ[l] g \Rightarrow (f \circ Prod.snd) =Θ[l' \timesˢ l] (g \circ Prod.snd)$$$

Lean4

/-- The integral sum of `f : ℝⁿ → E` over a tagged prepartition `π` w.r.t. box-additive volume `vol`
with codomain `E →L[ℝ] F` is the sum of `vol J (f (π.tag J))` over all boxes of `π`. -/
def integralSum (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I) : F :=
  ∑ J ∈ π.boxes, vol J (f (π.tag J))

Похожие утверждения