Theorems · Definition · measure theory

MeasureTheory.integral

{α : Type u_6} →
  {G : Type u_7} →
    [inst : NormedAddCommGroup G] → [NormedSpace ℝ G] → {x : MeasurableSpace α} → MeasureTheory.Measure α → (α → G) → G

The Bochner integral

Defined in: Mathlib.MeasureTheory.Integral.Bochner.Basic
Cited by: 1,779 results in Mathlib
Foundations: Depth 249 from the axioms, rests on 6,411 definitions · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup NormedSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
NormedAddCommGroupstatement · cited by 15,752
MeasurableSpacestatement · cited by 13,106
NormedSpacestatement · cited by 12,499
MeasureTheory.Measurestatement · cited by 10,939

Cited by1,819

Results whose statement or proof uses this declaration.

intervalIntegralproof · cited by 546
ProbabilityTheory.mgfproof · cited by 113
MeasureTheory.integral_congr_aestatement · cited by 110
ProbabilityTheory.covarianceproof · cited by 96
MeasureTheory.averageproof · cited by 87
MeasureTheory.charFunproof · cited by 84
intervalIntegral.integral_of_lestatement and proof · cited by 83
MeasureTheory.integral_conststatement and proof · cited by 75
MeasureTheory.integral_mapstatement and proof · cited by 67
MeasureTheory.convolutionproof · cited by 65
MeasureTheory.charFunDualproof · cited by 59
MeasureTheory.integral_zerostatement · cited by 59

Showing the 200 most cited of 1,819.