Beurling–Ahlfors transform

DefinitionLarger of an exponent and its conjugate#✓fully proved

For a real number \(p\), \(p^* = \max(p, p/(p-1))\), with division by zero taken to be \(0\) (so \(p^* = 1\) at \(p = 1\)). For \(p > 1\) this is the larger of \(p\) and its conjugate exponent \(p/(p-1)\).

noncomputable def pstar (p : ℝ) : ℝ :=
  max p (p / (p - 1))

Used by 4

Used byBañuelos–Janakiraman upper bound for the Beurling–Ahlfors transform · Beurling–Ahlfors constant · Iwaniec's conjecture · Lehto's lower bound for the Beurling–Ahlfors transform

DefinitionTruncated Beurling–Ahlfors integral#✓fully proved

For a real number \(\varepsilon\), a function \(f : \mathbb{C} \to \mathbb{C}\) and \(z \in \mathbb{C}\), the truncated Beurling–Ahlfors integral at cutoff \(\varepsilon\) is \(-\frac{1}{\pi} \int_{|w - z| > \varepsilon} \frac{f(w)}{(z - w)^2} \, dw\), the integral being with respect to Lebesgue measure on \(\mathbb{C}\) and taken to be \(0\) when the integrand is not integrable.

noncomputable def beurlingTrunc (ε : ℝ) (f : ℂ → ℂ) (z : ℂ) : ℂ :=
  -(1 / ((Real.pi : ℝ) : ℂ)) * ∫ w in { w : ℂ | ε < ‖w - z‖ }, f w / (z - w) ^ 2

Used by 1

Used byBeurling–Ahlfors transform

DefinitionBeurling–Ahlfors transform#✓fully proved

For \(f : \mathbb{C} \to \mathbb{C}\) and \(z \in \mathbb{C}\), \(Bf(z)\) is the limit as \(\varepsilon \to 0^+\) of the truncated Beurling–Ahlfors integrals \(-\frac{1}{\pi} \int_{|w - z| > \varepsilon} \frac{f(w)}{(z - w)^2} \, dw\) (each taken to be \(0\) when its integrand is not integrable). Where this limit does not exist, \(Bf(z)\) is an unspecified complex number.

For \(f \in L^p\) with \(1 < p < \infty\) the limit exists almost everywhere.

noncomputable def beurlingTransform (f : ℂ → ℂ) (z : ℂ) : ℂ :=
  Filter.limUnder (𝓝[Set.Ioi 0] 0) fun ε => beurlingTrunc ε f z

Uses 1 · Used by 1

Statement usesTruncated Beurling–Ahlfors integral

Used byAdmissible bounds for the Beurling–Ahlfors transform

DefinitionAdmissible bounds for the Beurling–Ahlfors transform#✓fully proved

For real numbers \(p\) and \(C\), \(C\) is an admissible \(L^p\) bound constant for the Beurling–Ahlfors transform \(B\) when \(\|Bf\|_q \le \max(C, 0) \, \|f\|_q\) for every almost everywhere strongly measurable function \(f : \mathbb{C} \to \mathbb{C}\), where \(q = \max(p, 0)\) and \(\|\cdot\|_q\) is the extended \(L^q\) norm with respect to Lebesgue measure (identically \(0\) when \(q = 0\)), with values in \([0, \infty]\) and the convention \(0 \cdot \infty = 0\).

def IsBound (p C : ℝ) : Prop :=
  ∀ f : ℂ → ℂ, AEStronglyMeasurable f volume →
    eLpNorm (beurlingTransform f) (ENNReal.ofReal p) volume ≤
      ENNReal.ofReal C * eLpNorm f (ENNReal.ofReal p) volume

Uses 1 · Used by 3

Statement usesBeurling–Ahlfors transform

Used byBañuelos–Janakiraman upper bound for the Beurling–Ahlfors transform · Norm of the Beurling–Ahlfors transform · Nonnegative admissible bounds bound the Beurling–Ahlfors norm

DefinitionNorm of the Beurling–Ahlfors transform#✓fully proved

For a real number \(p\), the norm \(\|B\|_p\) of the Beurling–Ahlfors transform \(B\) is the infimum of the real numbers \(C \ge 0\) that are admissible \(L^p\) bound constants for \(B\), and is \(0\) when there is no such \(C\). In particular an upper bound on \(\|B\|_p\) alone does not imply that \(B\) is bounded on \(L^p\).

noncomputable def beurlingNorm (p : ℝ) : ℝ :=
  sInf { C : ℝ | 0 ≤ C ∧ IsBound p C }

Uses 1 · Used by 5

Statement usesAdmissible bounds for the Beurling–Ahlfors transform

Used byBeurling–Ahlfors constant · Nonnegative admissible bounds bound the Beurling–Ahlfors norm · Iwaniec's conjecture · The Beurling–Ahlfors transform has \(L^2\) norm \(1\) · Lehto's lower bound for the Beurling–Ahlfors transform

TheoremNonnegative admissible bounds bound the Beurling–Ahlfors norm#✓fully proved

Let \(p\) and \(C\) be real numbers with \(C \ge 0\), and let \(\|B\|_p\) be the infimum of the nonnegative admissible \(L^p\) bound constants for the Beurling–Ahlfors transform \(B\) (\(0\) if there are none). If \(C\) is an admissible \(L^p\) bound constant for \(B\), then \(\|B\|_p \le C\).

theorem beurlingNorm_le_of_isBound {p C : ℝ} (hC : 0 ≤ C) (h : IsBound p C) :
    beurlingNorm p ≤ C

Uses 2

Statement usesAdmissible bounds for the Beurling–Ahlfors transform · Norm of the Beurling–Ahlfors transform

DefinitionBeurling–Ahlfors constant#✓fully proved

The Beurling–Ahlfors constant is the supremum, over real numbers \(p > 1\), of \(\|B\|_p / (p^* - 1)\), where \(B\) is the Beurling–Ahlfors transform, \(\|B\|_p\) is the infimum of the real numbers \(C \ge 0\) that are admissible \(L^p\) bound constants for \(B\) (and \(0\) if there is no such \(C\)), and \(p^* = \max(p, p/(p-1))\). The supremum is taken in \(\mathbb{R}\), so it is \(0\) when these ratios are not bounded above.

noncomputable def beurlingAhlforsConstant : ℝ :=
  sSup { r : ℝ | ∃ p : ℝ, 1 < p ∧ r = beurlingNorm p / (pstar p - 1) }

Uses 2

Statement usesNorm of the Beurling–Ahlfors transform · Larger of an exponent and its conjugate

DefinitionIwaniec's conjecture#✓fully proved

For every real number \(p > 1\), the \(L^p\) norm of the Beurling–Ahlfors transform \(B\) satisfies \(\|B\|_p = p^* - 1\), where \(p^* = \max(p, p/(p-1))\).

Given Lehto's lower bound \(\|B\|_p \ge p^* - 1\), this is equivalent to the Beurling–Ahlfors constant being equal to \(1\).

def IwaniecConjecture : Prop :=
  ∀ p : ℝ, 1 < p → beurlingNorm p = pstar p - 1

Uses 2

Statement usesNorm of the Beurling–Ahlfors transform · Larger of an exponent and its conjugate

TheoremLehto's lower bound for the Beurling–Ahlfors transform#●ready to prove

For a function \(f : \mathbb{C} \to \mathbb{C}\) let \(Bf(z)\) be the limit as \(\varepsilon \to 0^+\) of \(-\frac{1}{\pi} \int_{|w - z| > \varepsilon} \frac{f(w)}{(z - w)^2} \, dA(w)\), where \(dA\) is Lebesgue area measure (a junk value where the limit does not exist). For real \(p > 1\) let \(p^* = \max(p, p/(p - 1))\) and let \(\|B\|_p\) be the infimum of the constants \(C \ge 0\) such that \(\|Bf\|_{L^p} \le C\,\|f\|_{L^p}\) in \([0, \infty]\) for every almost everywhere strongly measurable \(f : \mathbb{C} \to \mathbb{C}\), taken to be \(0\) when there is no such \(C\). Then \(p^* - 1 \le \|B\|_p\) for every real \(p > 1\).

Because \(\|B\|_p\) is \(0\) when no such \(C\) exists, this also asserts that \(B\) has an admissible \(L^p\) bound for every \(p > 1\).

theorem_wanted lehtoLowerBound_wanted :
    ∀ p : ℝ, 1 < p → pstar p - 1 ≤ beurlingNorm p

Sources

• Lehto (1965): ‖B‖ₚ ≥ p* - 1 for all 1 < p.

Uses 2

Statement usesNorm of the Beurling–Ahlfors transform · Larger of an exponent and its conjugate

TheoremBañuelos–Janakiraman upper bound for the Beurling–Ahlfors transform#●ready to prove

For a function \(f : \mathbb{C} \to \mathbb{C}\) let \(Bf(z)\) be the limit as \(\varepsilon \to 0^+\) of \(-\frac{1}{\pi} \int_{|w - z| > \varepsilon} \frac{f(w)}{(z - w)^2} \, dA(w)\), where \(dA\) is Lebesgue area measure (a junk value where the limit does not exist), and for real \(p > 1\) let \(p^* = \max(p, p/(p - 1))\). For every real \(p > 1\) and every almost everywhere strongly measurable \(f : \mathbb{C} \to \mathbb{C}\), \(\|Bf\|_{L^p} \le 1.575\,(p^* - 1)\,\|f\|_{L^p}\), with the \(L^p\) norms taken in \([0, \infty]\).

theorem_wanted banuelosJanakiramanUpperBound_wanted :
    ∀ p : ℝ, 1 < p → IsBound p ((1575 / 1000 : ℝ) * (pstar p - 1))

Sources

• Bañuelos and Janakiraman, Lp-bounds for the Beurling--Ahlfors transform, Trans. Amer. Math. Soc. 360 (2008): ‖B‖ₚ ≤ 1.575 (p* - 1) for all 1 < p. Stated as the actual finite exponential bound (an admissible L^p bound constant), not as an inequality for the totalized infimum; combined with beurlingNorm_le_of_isBound (and 0 ≤ 1.575 * (pstar p - 1), from two_le_pstar) it yields beurlingNorm p ≤ 1.575 * (pstar p - 1).

Uses 2

Statement usesAdmissible bounds for the Beurling–Ahlfors transform · Larger of an exponent and its conjugate

TheoremThe Beurling–Ahlfors transform has \(L^2\) norm \(1\)#●ready to prove

For a function \(f : \mathbb{C} \to \mathbb{C}\) let \(Bf(z)\) be the limit as \(\varepsilon \to 0^+\) of \(-\frac{1}{\pi} \int_{|w - z| > \varepsilon} \frac{f(w)}{(z - w)^2} \, dA(w)\), where \(dA\) is Lebesgue area measure (a junk value where the limit does not exist). The infimum \(\|B\|_2\) of the constants \(C \ge 0\) such that \(\|Bf\|_{L^2} \le C\,\|f\|_{L^2}\) in \([0, \infty]\) for every almost everywhere strongly measurable \(f : \mathbb{C} \to \mathbb{C}\) (taken to be \(0\) when there is no such \(C\)) equals \(1\).

theorem_wanted l2Norm_wanted :
    beurlingNorm 2 = 1

Sources

• the L² isometry recorded in Bañuelos--Janakiraman (2008), introduction: ‖B‖₂ = 1.

Uses 1

Statement usesNorm of the Beurling–Ahlfors transform

8 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.