Theorems · Theorem · measure theory
MeasureTheory.Integrable.mul_const
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜] {f : α → 𝕜},
MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable (fun x => f x * c) μ- Cited by
- 17 results in Mathlib
- Foundations
- Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.Integrablestatement and proof · cited by 1,367
- NormedRingstatement and proof · cited by 924
- MulOpposite.opproof · cited by 520
- MeasureTheory.Integrable.smulproof · cited by 21
Cited by17
Results whose statement or proof uses this declaration.
- MeasureTheory.Integrable.convolution_integrandproof · cited by 6
- MeasureTheory.Integrable.div_constproof · cited by 4
- integrableOn_mul_sum_Iccproof · cited by 3
- HasCompactSupport.hasFDerivAt_convolution_rightproof · cited by 2
- BddAbove.continuous_convolution_right_of_integrableproof · cited by 2
- BddAbove.convolutionExistsAt'proof · cited by 2
- continuousOn_integral_bilinear_of_locally_integrable_of_compact_supportproof · cited by 2
- ProbabilityTheory.Kernel.HasSubgaussianMGF.add_compProdproof · cited by 1
- ProbabilityTheory.iteratedDeriv_two_cgf_eq_integralproof · cited by 1
- Real.integral_rpowIntegrand₀₁_eq_rpow_mul_constproof · cited by 1
- integral_pow_mul_le_of_le_of_pow_mul_leproof · cited by 1
- MeasureTheory.dist_convolution_le'proof · cited by 1