The Calderón–Zygmund decomposition

Let f : (ι → ℝ) → E be integrable on ℝⁿ, n ≥ 1, and let t > 0. The Calderón–Zygmund decomposition of f at height t writes

f = g + ∑_Q b_Q,

where the sum runs over a countable family of pairwise disjoint dyadic cubes Q, the Calderón–Zygmund cubes, such that

• t < ⨍_Q ‖f‖ ≤ 2ⁿ t on each cube, and t |⋃ Q| ≤ ∫_{⋃ Q} ‖f‖;
• the good part g is f off the cubes and the average of f on each cube, so that ‖g‖ ≤ 2ⁿ t almost everywhere and ‖g‖₁ ≤ ‖f‖₁;
• each bad part b_Q is supported on Q, has integral zero, and ‖b_Q‖₁ ≤ 2 ∫_Q ‖f‖; if f ∈ Lᵖ for a finite p, the series ∑_Q b_Q converges to f - g in Lᵖ.

It is the device that turns L² bounds for singular integral operators into weak type (1, 1) bounds (ContinuousLinearMap.mul_volume_lt_enorm_le_of_setLIntegral_compl_closedBall_le): the good part is bounded, hence in L² with ‖g‖₂² ≤ 2ⁿ t ‖f‖₁, while the bad parts have mean zero on small cubes, where the smoothness of the kernel makes them nearly cancel. Together with Marcinkiewicz interpolation this gives Lᵖ boundedness for 1 < p < 2; the range 2 < p < ∞ then follows by applying the corresponding bounds to the adjoint and using duality.

The cubes are the maximal dyadic cubes on which the average of ‖f‖ exceeds t (TauCeti.calderonZygmundCubes). They exist because averages over large cubes are small, which is where integrability and positive dimension enter; and ‖f‖ ≤ t almost everywhere off them by the Lebesgue differentiation theorem along dyadic cubes. The selection of the cubes is stated for an arbitrary g : (ι → ℝ) → ℝ≥0∞ in place of ‖f‖ₑ.

Main declarations

• TauCeti.calderonZygmundCubes: the Calderón–Zygmund cubes of g at height t, with TauCeti.lt_setLAverage_of_mem_calderonZygmundCubes, TauCeti.setLAverage_le_of_mem_calderonZygmundCubes, TauCeti.mul_volume_lt_volume_inter_of_mem_calderonZygmundCubes_indicator, TauCeti.volume_inter_le_mul_volume_of_mem_calderonZygmundCubes_indicator, TauCeti.pairwiseDisjoint_calderonZygmundCubes, TauCeti.dyadicCube_subset_of_mem_calderonZygmundCubes_of_le, TauCeti.exists_mem_calderonZygmundCubes_of_lt_setLAverage, TauCeti.biUnion_calderonZygmundCubes_subset, TauCeti.ae_le_of_forall_notMem_calderonZygmundCubes and TauCeti.mul_volume_biUnion_calderonZygmundCubes_le.
• TauCeti.calderonZygmundBad, TauCeti.calderonZygmundGood: the bad parts and the good part, with TauCeti.calderonZygmundGood_add_tsum_calderonZygmundBad (the decomposition), TauCeti.integral_calderonZygmundBad, TauCeti.lintegral_enorm_calderonZygmundBad_le, TauCeti.ae_enorm_calderonZygmundGood_le and TauCeti.lintegral_enorm_calderonZygmundGood_le.
• TauCeti.sq_eLpNorm_calderonZygmundGood_le, TauCeti.memLp_two_calderonZygmundGood: the good part is in L², with ‖g‖₂² ≤ 2ⁿ t ‖f‖₁.
• TauCeti.hasSum_toLp_calderonZygmundBad: in Lᵖ, p < ∞, the bad parts sum to f - g.

References

• A. P. Calderón and A. Zygmund, On the existence of certain singular integrals, Acta Math. 88 (1952), 85–139.
• E. Stein, Singular Integrals and Differentiability Properties of Functions, Chapter I, §4.
• L. Grafakos, Classical Fourier Analysis, Section 5.3.1.

def TauCeti.calderonZygmundCubes {ι : Type u_1} [Fintype ι] (g : (ι → ℝ) → ENNReal) (t : ENNReal) : Set (ℤ × (ι → ℤ))

The Calderón–Zygmund cubes of g at height t: the dyadic cubes, recorded by level and position, on which the average of g exceeds t while it is at most t on every dyadic cube of higher level containing them. These are the maximal dyadic cubes on which the average of g exceeds t.

theorem TauCeti.mem_calderonZygmundCubes {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} {q : ℤ × (ι → ℤ)} : q ∈ calderonZygmundCubes g t ↔ t < ⨍⁻ (x : ι → ℝ) in dyadicCube q.1 q.2, g x ∧ ∀ (j : ℤ) (m : ι → ℤ), q.1 < j → dyadicCube q.1 q.2 ⊆ dyadicCube j m → ⨍⁻ (x : ι → ℝ) in dyadicCube j m, g x ≤ t

theorem TauCeti.lt_setLAverage_of_mem_calderonZygmundCubes {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} {q : ℤ × (ι → ℤ)} (hq : q ∈ calderonZygmundCubes g t) : t < ⨍⁻ (x : ι → ℝ) in dyadicCube q.1 q.2, g x

The average over a Calderón–Zygmund cube exceeds the height.

theorem TauCeti.mul_volume_lt_setLIntegral_of_mem_calderonZygmundCubes {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} {q : ℤ × (ι → ℤ)} (hq : q ∈ calderonZygmundCubes g t) : t * MeasureTheory.volume (dyadicCube q.1 q.2) < ∫⁻ (x : ι → ℝ) in dyadicCube q.1 q.2, g x

The integral over a Calderón–Zygmund cube exceeds the height times its volume.

theorem TauCeti.setLAverage_le_of_mem_calderonZygmundCubes {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} {q : ℤ × (ι → ℤ)} (hq : q ∈ calderonZygmundCubes g t) : ⨍⁻ (x : ι → ℝ) in dyadicCube q.1 q.2, g x ≤ 2 ^ Fintype.card ι * t

The average over a Calderón–Zygmund cube is at most 2ⁿ times the height: the average over its parent cube is at most the height, and the parent is 2ⁿ times larger.

theorem TauCeti.dyadicCube_subset_of_mem_calderonZygmundCubes_indicator {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} {q q₀ : ℤ × (ι → ℤ)} (ht : ⨍⁻ (x : ι → ℝ) in dyadicCube q₀.1 q₀.2, g x ≤ t) (hq : q ∈ calderonZygmundCubes ((dyadicCube q₀.1 q₀.2).indicator g) t) : dyadicCube q.1 q.2 ⊆ dyadicCube q₀.1 q₀.2

Localization. The Calderón–Zygmund cubes of g restricted to a dyadic cube Q₀, at a height t at least the average of g over Q₀, lie inside Q₀: by the nesting of dyadic cubes, any other dyadic cube is either disjoint from Q₀ or contains it, and so has average at most t.

theorem TauCeti.mul_volume_lt_volume_inter_of_mem_calderonZygmundCubes_indicator {ι : Type u_1} [Fintype ι] {t : ENNReal} {q : ℤ × (ι → ℤ)} {A : Set (ι → ℝ)} (hA : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hq : q ∈ calderonZygmundCubes (A.indicator 1) t) : t * MeasureTheory.volume (dyadicCube q.1 q.2) < MeasureTheory.volume (A ∩ dyadicCube q.1 q.2)

A Calderón–Zygmund cube Q of the indicator of A at height t meets A in more than a t fraction of its volume: t |Q| < |A ∩ Q|.

theorem TauCeti.volume_inter_le_mul_volume_of_mem_calderonZygmundCubes_indicator {ι : Type u_1} [Fintype ι] {t : ENNReal} {q : ℤ × (ι → ℤ)} {A : Set (ι → ℝ)} (hA : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hq : q ∈ calderonZygmundCubes (A.indicator 1) t) {j : ℤ} {m : ι → ℤ} (hj : q.1 < j) (hsub : dyadicCube q.1 q.2 ⊆ dyadicCube j m) : MeasureTheory.volume (A ∩ dyadicCube j m) ≤ t * MeasureTheory.volume (dyadicCube j m)

A dyadic cube P of higher level containing a Calderón–Zygmund cube of the indicator of A at height t meets A in at most a t fraction of its volume: |A ∩ P| ≤ t |P|.

theorem TauCeti.pairwiseDisjoint_calderonZygmundCubes {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} : (calderonZygmundCubes g t).PairwiseDisjoint fun (q : ℤ × (ι → ℤ)) => dyadicCube q.1 q.2

Distinct Calderón–Zygmund cubes are disjoint.

theorem TauCeti.dyadicCube_subset_of_mem_calderonZygmundCubes_of_le {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} {q : ℤ × (ι → ℤ)} {t' : ENNReal} (htt' : t ≤ t') {p : ℤ × (ι → ℤ)} (hp : p ∈ calderonZygmundCubes g t') (hq : q ∈ calderonZygmundCubes g t) (hpq : (dyadicCube p.1 p.2 ∩ dyadicCube q.1 q.2).Nonempty) : dyadicCube p.1 p.2 ⊆ dyadicCube q.1 q.2

Nesting across heights. A Calderón–Zygmund cube at a height t' that meets a Calderón–Zygmund cube at a height t ≤ t' lies inside it: by maximality, every dyadic cube strictly containing the lower cube has average at most t.

theorem TauCeti.exists_mem_calderonZygmundCubes_of_lt_setLAverage {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} [Nonempty ι] (hg : ∫⁻ (x : ι → ℝ), g x ≠ ⊤) (ht : t ≠ 0) {k : ℤ} {m : ι → ℤ} (h : t < ⨍⁻ (x : ι → ℝ) in dyadicCube k m, g x) : ∃ q ∈ calderonZygmundCubes g t, k ≤ q.1 ∧ dyadicCube k m ⊆ dyadicCube q.1 q.2

In positive dimension, every dyadic cube on which the average of an integrable g exceeds a positive height t lies in a Calderón–Zygmund cube of g at height t.

theorem TauCeti.biUnion_calderonZygmundCubes_subset {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} [Nonempty ι] (hg : ∫⁻ (x : ι → ℝ), g x ≠ ⊤) (ht : t ≠ 0) {t' : ENNReal} (htt' : t ≤ t') : ⋃ q ∈ calderonZygmundCubes g t', dyadicCube q.1 q.2 ⊆ ⋃ q ∈ calderonZygmundCubes g t, dyadicCube q.1 q.2

In positive dimension, the union of the Calderón–Zygmund cubes of an integrable g shrinks as the height grows: for 0 < t ≤ t', each cube at height t' has average above t, so it lies in a cube at height t.

theorem TauCeti.ae_le_of_forall_notMem_calderonZygmundCubes {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} [Nonempty ι] (hg : AEMeasurable g MeasureTheory.volume) (hg' : ∫⁻ (x : ι → ℝ), g x ≠ ⊤) (ht : t ≠ 0) : ∀ᵐ (x : ι → ℝ), (∀ q ∈ calderonZygmundCubes g t, x ∉ dyadicCube q.1 q.2) → g x ≤ t

In positive dimension, an integrable g is at most t almost everywhere off its Calderón–Zygmund cubes at a positive height t.

theorem TauCeti.measurableSet_biUnion_calderonZygmundCubes {ι : Type u_1} [Fintype ι] (g : (ι → ℝ) → ENNReal) (t : ENNReal) : MeasurableSet (⋃ q ∈ calderonZygmundCubes g t, dyadicCube q.1 q.2)

The union of the Calderón–Zygmund cubes is measurable.

theorem TauCeti.mul_volume_biUnion_calderonZygmundCubes_le {ι : Type u_1} [Fintype ι] {g : (ι → ℝ) → ENNReal} {t : ENNReal} : t * MeasureTheory.volume (⋃ q ∈ calderonZygmundCubes g t, dyadicCube q.1 q.2) ≤ ∫⁻ (x : ι → ℝ) in ⋃ q ∈ calderonZygmundCubes g t, dyadicCube q.1 q.2, g x

The Calderón–Zygmund measure estimate: t times the measure of the union of the Calderón–Zygmund cubes of g at height t is at most the integral of g over that union.

noncomputable def TauCeti.calderonZygmundBad {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ) → E) (q : ℤ × (ι → ℤ)) : (ι → ℝ) → E

The bad part of f on the dyadic cube q: f minus its average over the cube, on the cube, and 0 off it.

@[simp]

theorem TauCeti.calderonZygmundBad_of_mem {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {q : ℤ × (ι → ℤ)} {x : ι → ℝ} (hx : x ∈ dyadicCube q.1 q.2) : calderonZygmundBad f q x = f x - ⨍ (y : ι → ℝ) in dyadicCube q.1 q.2, f y

@[simp]

theorem TauCeti.calderonZygmundBad_of_notMem {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {q : ℤ × (ι → ℤ)} {x : ι → ℝ} (hx : x ∉ dyadicCube q.1 q.2) : calderonZygmundBad f q x = 0

noncomputable def TauCeti.calderonZygmundGood {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ) → E) (t : ENNReal) : (ι → ℝ) → E

The good part of the Calderón–Zygmund decomposition of f at height t: f minus its bad parts on the Calderón–Zygmund cubes of ‖f‖ₑ at height t. It is the average of f on each of these cubes (TauCeti.calderonZygmundGood_of_mem) and f off them (TauCeti.calderonZygmundGood_of_forall_notMem).

theorem TauCeti.calderonZygmundGood_add_tsum_calderonZygmundBad {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ) → E) (t : ENNReal) (x : ι → ℝ) : calderonZygmundGood f t x + ∑' (q : ↑(calderonZygmundCubes (fun (x : ι → ℝ) => ‖f x‖ₑ) t)), calderonZygmundBad f (↑q) x = f x

The Calderón–Zygmund decomposition: f is its good part plus the sum of its bad parts on the Calderón–Zygmund cubes. At each point at most one bad part is nonzero.

theorem TauCeti.calderonZygmundGood_of_mem {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {t : ENNReal} {q : ℤ × (ι → ℤ)} {x : ι → ℝ} (hq : q ∈ calderonZygmundCubes (fun (x : ι → ℝ) => ‖f x‖ₑ) t) (hx : x ∈ dyadicCube q.1 q.2) : calderonZygmundGood f t x = ⨍ (y : ι → ℝ) in dyadicCube q.1 q.2, f y

On a Calderón–Zygmund cube, the good part is the average of f over the cube.

theorem TauCeti.calderonZygmundGood_of_forall_notMem {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {t : ENNReal} {x : ι → ℝ} (hx : ∀ q ∈ calderonZygmundCubes (fun (x : ι → ℝ) => ‖f x‖ₑ) t, x ∉ dyadicCube q.1 q.2) : calderonZygmundGood f t x = f x

Off the Calderón–Zygmund cubes, the good part is f.

theorem TauCeti.integrable_calderonZygmundBad {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (q : ℤ × (ι → ℤ)) : MeasureTheory.Integrable (calderonZygmundBad f q) MeasureTheory.volume

The bad parts of an integrable function are integrable.

@[simp]

theorem TauCeti.integral_calderonZygmundBad {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : (ι → ℝ) → E) (q : ℤ × (ι → ℤ)) : ∫ (x : ι → ℝ), calderonZygmundBad f q x = 0

Each bad part has integral zero.

theorem TauCeti.lintegral_enorm_calderonZygmundBad_le {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ) → E) (q : ℤ × (ι → ℤ)) : ∫⁻ (x : ι → ℝ), ‖calderonZygmundBad f q x‖ₑ ≤ 2 * ∫⁻ (x : ι → ℝ) in dyadicCube q.1 q.2, ‖f x‖ₑ

Each bad part has L¹ norm at most twice the integral of ‖f‖ over its cube.

theorem TauCeti.ae_enorm_calderonZygmundGood_le {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {t : ENNReal} [Nonempty ι] (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ht : t ≠ 0) : ∀ᵐ (x : ι → ℝ), ‖calderonZygmundGood f t x‖ₑ ≤ 2 ^ Fintype.card ι * t

In positive dimension, the good part of an integrable f at a positive height t is bounded by 2ⁿ t almost everywhere.

theorem TauCeti.lintegral_enorm_calderonZygmundGood_le {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ) → E) (t : ENNReal) : ∫⁻ (x : ι → ℝ), ‖calderonZygmundGood f t x‖ₑ ≤ ∫⁻ (x : ι → ℝ), ‖f x‖ₑ

The good part has L¹ norm at most that of f.

theorem TauCeti.aestronglyMeasurable_calderonZygmundGood {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (t : ENNReal) : MeasureTheory.AEStronglyMeasurable (calderonZygmundGood f t) MeasureTheory.volume

The good part of an almost everywhere strongly measurable f is almost everywhere strongly measurable: it is constant on each Calderón–Zygmund cube and equal to f off them.

theorem TauCeti.integrable_calderonZygmundGood {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (t : ENNReal) : MeasureTheory.Integrable (calderonZygmundGood f t) MeasureTheory.volume

The good part of an integrable f is integrable.

theorem TauCeti.memLp_calderonZygmundBad {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {p : ENNReal} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (q : ℤ × (ι → ℤ)) : MeasureTheory.MemLp (calderonZygmundBad f q) p MeasureTheory.volume

The bad parts of a function in Lᵖ are in Lᵖ.

theorem TauCeti.sq_eLpNorm_calderonZygmundGood_le {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {t : ENNReal} [Nonempty ι] (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ht : t ≠ 0) : MeasureTheory.eLpNorm (calderonZygmundGood f t) 2 MeasureTheory.volume ^ 2 ≤ 2 ^ Fintype.card ι * t * ∫⁻ (x : ι → ℝ), ‖f x‖ₑ

In positive dimension, the square of the L² norm of the good part of an integrable f at a positive height t is at most 2ⁿ t ‖f‖₁: the good part is bounded by 2ⁿ t and has L¹ norm at most ‖f‖₁.

theorem TauCeti.memLp_two_calderonZygmundGood {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {t : ENNReal} [Nonempty ι] (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ht : t ≠ 0) (ht' : t ≠ ⊤) : MeasureTheory.MemLp (calderonZygmundGood f t) 2 MeasureTheory.volume

In positive dimension, the good part of an integrable f at a finite positive height is in L².

theorem TauCeti.subsingleton_support_calderonZygmundBad {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ) → E) (t : ENNReal) (x : ι → ℝ) : (Function.support fun (q : ↑(calderonZygmundCubes (fun (x : ι → ℝ) => ‖f x‖ₑ) t)) => calderonZygmundBad f (↑q) x).Subsingleton

At each point at most one bad part is nonzero.

theorem TauCeti.hasSum_toLp_calderonZygmundBad {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {t p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hg : MeasureTheory.MemLp (calderonZygmundGood f t) p MeasureTheory.volume) : HasSum (fun (q : ↑(calderonZygmundCubes (fun (x : ι → ℝ) => ‖f x‖ₑ) t)) => MeasureTheory.MemLp.toLp (calderonZygmundBad f ↑q) ⋯) (MeasureTheory.MemLp.toLp (f - calderonZygmundGood f t) ⋯)

If f and its good part at height t are in Lᵖ for a finite p ≥ 1, then the bad parts sum in Lᵖ to f minus the good part.