Theorems · Definition · measure theory

intervalIntegral

{E : Type u_5} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E) → ℝ → ℝ → MeasureTheory.Measure ℝ → E

The interval integral ∫ x in a..b, f x ∂μ is defined as ∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ. If a ≤ b, then it equals ∫ x in Ioc a b, f x ∂μ, otherwise it equals -∫ x in Ioc b a, f x ∂μ.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

546 results in Mathlib

Foundations

Depth 250 from the axioms, rests on 6,412 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace