Theorems · Theorem · measure theory
integral_re
∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
{f : X → 𝕜}, MeasureTheory.Integrable f μ → ∫ (x : X), RCLike.re (f x) ∂μ = RCLike.re (∫ (x : X), f x ∂μ)- Cited by
- 7 results in Mathlib
- Foundations
- Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpaceRCLike
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Realstatement · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- AddMonoidHomstatement · cited by 3,230
- RCLikestatement and proof · cited by 2,829
- MeasureTheory.integralstatement · cited by 1,779
- MeasureTheory.Integrablestatement and proof · cited by 1,367
- AddMonoid.toZerostatement · cited by 325
- RCLike.restatement · cited by 319
- ContinuousLinearMap.integral_comp_commproof · cited by 33
- RCLike.reCLMproof · cited by 20
Cited by7
Results whose statement or proof uses this declaration.
- integral_rpowproof · cited by 4
- ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_realproof · cited by 3
- hasSum_sq_fourierCoeffproof · cited by 2
- ProbabilityTheory.lintegral_betaPDF_eq_oneproof · cited by 1
- integral_exp_mul_Ioiproof · cited by 1
- UnitAddTorus.hasSum_sq_mFourierCoeffproof · cited by 0
- MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eqproof · cited by 0