Theorems · Theorem · measure theory
IntervalIntegrable.continuousOn_mul
∀ {A : Type u_7} [inst : NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → A},
IntervalIntegrable f μ a b → ContinuousOn g (Set.uIcc a b) → IntervalIntegrable (fun x => g x * f x) μ a b- Cited by
- 8 results in Mathlib
- Foundations
- Depth 220 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.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ContinuousOnstatement and proof · cited by 1,411
- NormedRingstatement and proof · cited by 924
- Set.uIccstatement and proof · cited by 393
- IntervalIntegrablestatement and proof · cited by 316
- measurableSet_Iocproof · cited by 65
- Set.Ioc_subset_Icc_selfproof · cited by 53
- intervalIntegrable_iffproof · cited by 29
- isCompact_uIccproof · cited by 17
- MeasureTheory.IntegrableOn.continuousOn_mul_of_subsetproof · cited by 2
Cited by8
Results whose statement or proof uses this declaration.
- IntervalIntegrable.const_mulproof · cited by 14
- Real.GammaIntegral_convergentproof · cited by 5
- intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_rightproof · cited by 2
- intervalIntegral.integral_deriv_mul_eq_sub_of_hasDeriv_rightproof · cited by 2
- Polynomial.Chebyshev.integrable_measureTproof · cited by 2
- CircleIntegrable.continuousOn_mulproof · cited by 2
- AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mulproof · cited by 1
- Complex.approx_Gamma_integral_tendsto_Gamma_integralproof · cited by 1