Theorems · Theorem · measure theory

MeasureTheory.Integrable.comp_sub_right

∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : AddGroup G] [MeasurableAdd G] {f : G → F} [μ.IsAddRightInvariant],
  MeasureTheory.Integrable f μ → ∀ (g : G), MeasureTheory.Integrable (fun t => f (t - g)) μ

Defined in: Mathlib.MeasureTheory.Group.Integral
Cited by: 4 results in Mathlib
Foundations: Depth 212 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace NormedAddCommGroup AddGroup MeasurableAdd MeasureTheory.Measure.IsAddRightInvariant

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

NormedAddCommGroupstatement and proof · cited by 15,752
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
AddGroupstatement and proof · cited by 4,410
MeasureTheory.Integrablestatement and proof · cited by 1,367
sub_eq_add_negproof · cited by 1,023
MeasurableAddstatement and proof · cited by 78
MeasureTheory.Measure.IsAddRightInvariantstatement and proof · cited by 59
MeasureTheory.Integrable.comp_add_rightproof · cited by 2

Cited by4

Results whose statement or proof uses this declaration.

MeasureTheory.Integrable.convolution_integrandproof · cited by 6
ProbabilityTheory.integrable_gaussianPDFRealproof · cited by 4
MeasureTheory.integral_convolutionproof · cited by 1
GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_Iproof · cited by 1