Hörmander's condition from the tail of an integrable kernel

For an integrable function f on a normed additive group with a right-invariant measure, translating by h maps {‖x‖ > 2 ‖h‖} into {‖x‖ > ‖h‖}, so

∫_{‖x‖ > 2 ‖h‖} ‖f (x - h) - f x‖ dx ≤ 2 ∫_{‖x‖ > ‖h‖} ‖f x‖ dx.

This is the crude form of Hörmander's condition for the convolution kernel f, used at the scales where its tail is small: in the proof of the Mihlin–Hörmander multiplier theorem it handles the Littlewood–Paley pieces of frequency 2 ^ j > ‖h‖⁻¹.

Main declarations

• MeasureTheory.Integrable.setIntegral_norm_comp_sub_le: the translate of f on {‖x‖ > 2 ‖h‖} is controlled by the tail of f on {‖x‖ > ‖h‖}.
• MeasureTheory.Integrable.setIntegral_norm_comp_sub_sub_le: Hörmander's condition bounded by twice the tail.

References

• L. Grafakos, Classical Fourier Analysis, 3rd ed., Section 6.2 (proof of Theorem 6.2.7).

theorem MeasureTheory.Integrable.setIntegral_norm_comp_sub_le {G : Type u_1} {E : Type u_2} [NormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup E] {μ : Measure G} [μ.IsAddRightInvariant] {f : G → E} (hf : Integrable f μ) (h : G) : ∫ (x : G) in {x : G | 2 * ‖h‖ < ‖x‖}, ‖f (x - h)‖ ∂μ ≤ ∫ (x : G) in {x : G | ‖h‖ < ‖x‖}, ‖f x‖ ∂μ

Translating by h maps {‖x‖ > 2 ‖h‖} into {‖x‖ > ‖h‖}, so the integral of ‖f (x - h)‖ over the first set is at most that of ‖f x‖ over the second.

theorem MeasureTheory.Integrable.setIntegral_norm_comp_sub_sub_le {G : Type u_1} {E : Type u_2} [NormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup E] {μ : Measure G} [μ.IsAddRightInvariant] {f : G → E} (hf : Integrable f μ) (h : G) : ∫ (x : G) in {x : G | 2 * ‖h‖ < ‖x‖}, ‖f (x - h) - f x‖ ∂μ ≤ 2 * ∫ (x : G) in {x : G | ‖h‖ < ‖x‖}, ‖f x‖ ∂μ

Hörmander's condition from the tail of the kernel. On {‖x‖ > 2 ‖h‖}, the difference f (x - h) - f x is controlled by twice the tail of f on {‖x‖ > ‖h‖}.