The Vitali covering estimate to Young's inequality for integral…

TheoremThe Vitali covering estimate #

If every point of S is the centre of a ball of radius at most R on which ∫⁻ g is at least t times the measure of the ball, then t * μ S ≤ 4 ^ n * ∫⁻ g, with n the dimension of the space.

The factor 4 ^ n is the cost of passing from a pairwise disjoint subfamily of those balls to its fourfold enlargement, which still covers S.

TauCeti.mul_measure_le_of_forall_exists_ball.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E]
  {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {t : ENNReal} {S : Set E} {R : ℝ}
  {g : E → ENNReal}
  (hS :
    ∀ x ∈ S, ∃ r ∈ Set.Ioc 0 R, t * μ (Metric.ball x r) ≤ ∫⁻ (y : E) in Metric.ball x r, g y ∂μ) :
  t * μ S ≤ 4 ^ Module.finrank ℝ E * ∫⁻ (y : E), g y ∂μ

Lean

Formalized in Tau Ceti as TauCeti.mul_measure_le_of_forall_exists_ball.

Sources

LeanTauCeti.mul_measure_le_of_forall_exists_ball

Used by 1

Used byThe Hardy–Littlewood maximal inequality

TheoremWolff's lemma (`TauCeti.exists_circleLIntegral_sq_lt`)#

If 2 π times the plane integral of g ^ 2 is smaller than c * log (R / r), then some circle of radius ρ strictly between r and R has circleLIntegral g ζ ρ ^ 2 < c.

Since log (R / r) grows without bound as the annulus is made longer while the plane integral stays fixed, this makes the circle integral arbitrarily small at arbitrarily small radii: a weight of finite square integral cannot have a large circle integral on every circle about ζ.

TauCeti.exists_circleLIntegral_sq_lt {g : ℂ → ENNReal} (hg : Measurable g) (ζ : ℂ) {r R : ℝ}
  (hr : 0 < r) (hrR : r < R) {c : ENNReal}
  (hc :
    ENNReal.ofReal (2 * Real.pi) * ∫⁻ (z : ℂ), g z ^ 2 < c * ENNReal.ofReal (Real.log (R / r))) :
  ∃ ρ ∈ Set.Ioo r R, TauCeti.circleLIntegral g ζ ρ ^ 2 < c

Lean

Formalized in Tau Ceti as TauCeti.exists_circleLIntegral_sq_lt.

Other forms

Wolff's lemma in the limit: a weight of finite square integral has small circle integrals at arbitrarily small radii. Formalized in Tau Ceti as TauCeti.exists_circleLIntegral_lt_of_lintegral_sq_ne_top.

TauCeti.exists_circleLIntegral_lt_of_lintegral_sq_ne_top {g : ℂ → ENNReal} (hg : Measurable g)
  (hfin : ∫⁻ (z : ℂ), g z ^ 2 ≠ ⊤) (ζ : ℂ) {c : ENNReal} (hc : c ≠ 0) {R : ℝ} (hR : 0 < R) :
  ∃ ρ ∈ Set.Ioo 0 R, TauCeti.circleLIntegral g ζ ρ < c

Sources

LeanTauCeti.exists_circleLIntegral_sq_lt · TauCeti.exists_circleLIntegral_lt_of_lintegral_sq_ne_top

Uses 1 · Used by 3

Proof usesCauchy–Schwarz on a circle

Used byCarathéodory's continuity theorem, as a characterization · Wolff's lemma (TauCeti.exists_circleImageLength_sq_lt) · The bounded-image form of the small-Jordan-curve theorem

TheoremYoung's inequality for integral kernels #

Let 1 ≤ p ≤ q and let r be the exponent with 1/p + 1/r = 1 + 1/q. If the r-th powers of the kernel k have row integrals ∫⁻ y, k x y ^ r ∂ν at most A for almost every x and column integrals ∫⁻ x, k x y ^ r ∂μ at most B for almost every y, then the integral operator with kernel k satisfies ∫⁻ x, (∫⁻ y, k x y * g y ∂ν) ^ q ∂μ ≤ A ^ (q (1 - 1/p)) * B * (∫⁻ y, g y ^ p ∂ν) ^ (q / p).

The kernel need only be a.e. measurable: the proof applies the measurable case to a measurable modification of k, which agrees with k on almost every row and on almost every column. For p = q this is Schur's test, TauCeti.lintegral_rpow_lintegral_mul_le.

TauCeti.lintegral_rpow_lintegral_mul_le_of_inv_add_inv_eq.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  {k : α → β → ENNReal} (hk : AEMeasurable (Function.uncurry k) (μ.prod ν)) {g : β → ENNReal}
  (hg : AEMeasurable g ν) {p q r : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) (hr : p⁻¹ + r⁻¹ = 1 + q⁻¹)
  {A B : ENNReal} (hA : ∀ᵐ (x : α) ∂μ, ∫⁻ (y : β), k x y ^ r ∂ν ≤ A)
  (hB : ∀ᵐ (y : β) ∂ν, ∫⁻ (x : α), k x y ^ r ∂μ ≤ B) :
  ∫⁻ (x : α), (∫⁻ (y : β), k x y * g y ∂ν) ^ q ∂μ ≤
    A ^ (q * (1 - p⁻¹)) * B * (∫⁻ (y : β), g y ^ p ∂ν) ^ (q / p)