Documentation

TauCeti.MeasureTheory.Integral.CalderonZygmund.StandardKernel

Standard Calderón–Zygmund kernels satisfy Hörmander's condition #

The Calderón–Zygmund theorem (ContinuousLinearMap.mul_volume_lt_enorm_le_of_hormander) asks of the kernel K of a singular integral operator only Hörmander's condition

∫_{dist x y' > 2 dist y y'} ‖K x y - K x y'‖ dx ≤ B for all y, y'.

The kernels met in practice (the Hilbert and Riesz transforms, the second derivatives of the Newtonian kernel) are instead known to satisfy the pointwise standard smoothness estimate

‖K x y - K x y'‖ ≤ C dist y y' ^ δ / dist x y' ^ (n + δ) whenever dist x y' > 2 dist y y',

for some δ > 0. This file shows that the pointwise estimate implies Hörmander's condition with B = C A 2ⁿ / (2^δ - 1), in any metric measure space whose balls satisfy the growth bound μ (closedBall y r) ≤ A rⁿ (TauCeti.setLIntegral_enorm_sub_le_of_norm_sub_le_mul_rpow). The exponent n need not be an integer. On ℝⁿ = ι → ℝ with Lebesgue measure, where closed balls are cubes of volume (2r)ⁿ, this gives B = 4ⁿ C / (2^δ - 1) (TauCeti.setLIntegral_enorm_sub_le_of_norm_sub_le_mul_rpow_pi), and so the Calderón–Zygmund theorem for operators with a standard kernel: they are of weak type (1, 1) as soon as they are bounded on L² (ContinuousLinearMap.mul_volume_lt_enorm_le_of_norm_sub_le_mul_rpow). The same bound is the hypothesis of the strong type (p, p) theorem for 1 < p < 2 (ContinuousLinearMap.eLpNorm_le_of_hormander).

The proof integrates the pointwise estimate against the tail bound ∫_{dist x y' > R} dist x y' ^ (-s) dx ≤ A 2ⁿ R ^ (n - s) / (1 - 2 ^ (n - s)) for s > n (TauCeti.setLIntegral_ofReal_dist_rpow_neg_le). Taking R = 2 dist y y' and s = n + δ gives Hörmander's condition, with a bound independent of y and y'.

The smoothness estimate is sometimes only available when dist x y' > c dist y y' for some c > 2, for instance after comparing two equivalent distances. Together with the size estimate ‖K x y‖ ≤ C₀ dist x y ^ (-n) it then holds with the factor 2 and a larger constant (TauCeti.norm_sub_le_mul_rpow_of_norm_le_mul_rpow), since for 2 dist y y' < dist x y' ≤ c dist y y' both terms are bounded by the size estimate.

Main declarations #

References #

theorem TauCeti.norm_sub_le_mul_rpow_of_norm_le_mul_rpow {X : Type u_1} {G : Type u_2} [PseudoMetricSpace X] [SeminormedAddGroup G] {K : X → X → G} {n δ : ℝ} (hn : 0 ≤ n) (hnδ : 0 ≤ n + δ) {c C₀ C : NNReal} (hc : 2 ≤ c) (hsize : ∀ (x y : X), 0 < dist x y → ‖K x y‖ ≤ ↑C₀ * dist x y ^ (-n)) (hK : ∀ (x y y' : X), ↑c * dist y y' < dist x y' → ‖K x y - K x y'‖ ≤ ↑C * (dist y y' ^ δ * dist x y' ^ (-(n + δ)))) {x y y' : X} (h : 2 * dist y y' < dist x y') :
‖K x y - K x y'‖ ≤ ↑(C + 2 * C₀ * c ^ (n + δ)) * (dist y y' ^ δ * dist x y' ^ (-(n + δ)))

The size estimate lowers the factor in the smoothness estimate. Let K satisfy the size estimate ‖K x y‖ ≤ C₀ dist x y ^ (-n) with 0 ≤ n and, for some c ≥ 2 and some δ with 0 ≤ n + δ, the smoothness estimate

‖K x y - K x y'‖ ≤ C dist y y' ^ δ dist x y' ^ (-(n + δ)) whenever dist x y' > c dist y y'.

Then the smoothness estimate holds whenever dist x y' > 2 dist y y', with the constant C + 2 C₀ c ^ (n + δ).

theorem TauCeti.setLIntegral_enorm_sub_le_of_norm_sub_le_mul_rpow {X : Type u_1} {G : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [SeminormedAddGroup G] {K : X → X → G} {y y' : X} {A : ENNReal} {n : ℝ} (hμ : ∀ (r : ℝ), 0 < r → μ (Metric.closedBall y' r) ≤ A * ENNReal.ofReal (r ^ n)) (hn : 0 ≤ n) {C : NNReal} {δ : ℝ} (hδ : 0 < δ) (hK : ∀ (x : X), 2 * dist y y' < dist x y' → ‖K x y - K x y'‖ ≤ ↑C * (dist y y' ^ δ * dist x y' ^ (-(n + δ)))) :
∫⁻ (x : X) in {x : X | 2 * dist y y' < dist x y'}, ‖K x y - K x y'‖ₑ ∂μ ≤ ↑C * A * ENNReal.ofReal (2 ^ n / (2 ^ δ - 1))

The standard smoothness estimate implies Hörmander's condition. Let the closed balls about y' satisfy the growth bound μ (closedBall y' r) ≤ A rⁿ with 0 ≤ n, and let K satisfy the standard smoothness estimate with exponent δ > 0,

‖K x y - K x y'‖ ≤ C dist y y' ^ δ dist x y' ^ (-(n + δ)) whenever dist x y' > 2 dist y y'.

Then ∫_{dist x y' > 2 dist y y'} ‖K x y - K x y'‖ dx ≤ C A 2ⁿ / (2^δ - 1).

theorem TauCeti.setLIntegral_enorm_sub_le_of_norm_sub_le_mul_rpow_pi {ι : Type u_1} {G : Type u_2} [Fintype ι] [SeminormedAddGroup G] {K : (ι → ℝ) → (ι → ℝ) → G} {y y' : ι → ℝ} {C : NNReal} {δ : ℝ} (hδ : 0 < δ) (hK : ∀ (x : ι → ℝ), 2 * dist y y' < dist x y' → ‖K x y - K x y'‖ ≤ ↑C * (dist y y' ^ δ * dist x y' ^ (-(↑(Fintype.card ι) + δ)))) :
∫⁻ (x : ι → ℝ) in {x : ι → ℝ | 2 * dist y y' < dist x y'}, ‖K x y - K x y'‖ₑ ≤ ↑C * ENNReal.ofReal (4 ^ Fintype.card ι / (2 ^ δ - 1))

The standard smoothness estimate implies Hörmander's condition on ℝⁿ = ι → ℝ, with the sup norm and Lebesgue measure. If δ > 0 and

‖K x y - K x y'‖ ≤ C dist y y' ^ δ dist x y' ^ (-(n + δ)) whenever dist x y' > 2 dist y y',

then ∫_{dist x y' > 2 dist y y'} ‖K x y - K x y'‖ dx ≤ 4ⁿ C / (2^δ - 1).

theorem ContinuousLinearMap.mul_volume_lt_enorm_le_of_norm_sub_le_mul_rpow {ι : Type u_1} [Fintype ι] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (T : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)) {K : (ι → ℝ) → (ι → ℝ) → E →L[ℝ] F} (hKm : MeasureTheory.StronglyMeasurable (Function.uncurry K)) {C : NNReal} {δ : ℝ} (hδ : 0 < δ) (hK : ∀ (x y y' : ι → ℝ), 2 * dist y y' < dist x y' → ‖K x y - K x y'‖ ≤ ↑C * (dist y y' ^ δ * dist x y' ^ (-(↑(Fintype.card ι) + δ)))) (hrep : ∀ (b : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (y : ι → ℝ) (r : ℝ), (∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑b x = 0) → ∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑(T b) x = ∫ (z : ι → ℝ), (K x z) (↑↑b z)) (f : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (t : ENNReal) :
t * MeasureTheory.volume {x : ι → ℝ | t < ‖↑↑(T f) x‖ₑ} ≤ (2 ^ Fintype.card ι * (4 * ‖T‖ₑ ^ 2 + 1) + 4 * (↑C * ENNReal.ofReal (4 ^ Fintype.card ι / (2 ^ δ - 1)))) * ∫⁻ (x : ι → ℝ), ‖↑↑f x‖ₑ

The Calderón–Zygmund theorem for an operator with a standard kernel. Let T be a bounded linear operator on L²(ℝⁿ) such that T b x = ∫ K x y (b y) dy for almost every x off any closed ball outside which b vanishes, where for some δ > 0 the kernel K satisfies the standard smoothness estimate

‖K x y - K x y'‖ ≤ C dist y y' ^ δ dist x y' ^ (-(n + δ)) whenever dist x y' > 2 dist y y'.

Then for every f ∈ L² and every t,

t · |{‖T f‖ > t}| ≤ (2ⁿ (4 ‖T‖² + 1) + 4 · 4ⁿ C / (2^δ - 1)) ‖f‖₁.