Theorems · Theorem · measure theory
MeasureTheory.integrable_comp_smul_iff
∀ {F : Type u_1} [inst : NormedAddCommGroup F] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
(f : E → F) {R : ℝ}, R ≠ 0 → (MeasureTheory.Integrable (fun x => f (R • x)) μ ↔ MeasureTheory.Integrable f μ)- Cited by
- 2 results in Mathlib
- Foundations
- Depth 256 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
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
- TopologicalSpaceproof · cited by 24,529
- NormedAddCommGroupstatement and proof · cited by 15,752
- MeasurableSpacestatement and proof · cited by 13,106
- NormedSpacestatement and proof · cited by 12,499
- MeasureTheory.Measurestatement and proof · cited by 10,939
- FiniteDimensionalstatement and proof · cited by 1,854
- Module.finrankproof · cited by 1,770
- BorelSpacestatement and proof · cited by 1,602
- one_smulproof · cited by 1,374
- MeasureTheory.Integrablestatement and proof · cited by 1,367
- SemigroupAction.mul_smulproof · cited by 291
Cited by2
Results whose statement or proof uses this declaration.
- MeasureTheory.integrable_comp_mul_left_iffproof · cited by 3
- MeasureTheory.Integrable.comp_smulproof · cited by 1