Theorems · Theorem · abstract harmonic analysis

MeasureTheory.convolution_mono_right

∀ {G : Type uG} {x : G} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddGroup G] {f g g' : G → ℝ},
  MeasureTheory.ConvolutionExistsAt f g x (ContinuousLinearMap.lsmul ℝ ℝ) μ →
    MeasureTheory.ConvolutionExistsAt f g' x (ContinuousLinearMap.lsmul ℝ ℝ) μ →
      (∀ (x : G), 0 ≤ f x) →
        (∀ (x : G), g x ≤ g' x) →
          MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ x ≤
            MeasureTheory.convolution f g' (ContinuousLinearMap.lsmul ℝ ℝ) μ x

Defined in: Mathlib.Analysis.Convolution
Cited by: 1 results in Mathlib
Foundations: Depth 255 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace AddGroup

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.

Realstatement and proof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
AddGroupstatement and proof · cited by 4,410
mul_le_mul_of_nonneg_leftproof · cited by 361
ContinuousLinearMap.lsmulstatement and proof · cited by 66
MeasureTheory.convolutionstatement · cited by 65
MeasureTheory.ConvolutionExistsAtstatement and proof · cited by 18
MeasureTheory.integral_monoproof · cited by 17

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.convolution_mono_right_of_nonnegproof · cited by 1