The Calderón–Zygmund theorem to The Riesz–Thorin interpolation…

TheoremThe Calderón–Zygmund theorem#

The Calderón–Zygmund theorem for an operator given by a kernel, strong type (p, p) for 1 < p < 2. 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 the kernel K satisfies Hörmander's condition ∫_{dist x y' > 2 dist y y'} ‖K x y - K x y'‖ dx ≤ B for all y, y'. Then for every 1 < p < 2 and every f ∈ L²,

‖T f‖_p ≤ (p / (p - 1) · 2 (2ⁿ (4 ‖T‖² + 1) + 4 B) + p / (2 - p) · 4 ‖T‖²) ^ (1 / p) ‖f‖_p.

ContinuousLinearMap.eLpNorm_le_of_hormander.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] [Nonempty ι]
  {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ENNReal} [CompleteSpace F]
  (T :
    ↥(MeasureTheory.Lp E 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume))
  {K : (ι → ℝ) → (ι → ℝ) → E →L[ℝ] F} (hK : MeasureTheory.StronglyMeasurable (Function.uncurry K))
  {B : ENNReal}
  (hB : ∀ (y y' : ι → ℝ), ∫⁻ (x : ι → ℝ) in {x | 2 * dist y y' < dist x y'}, ‖K x y - K x y'‖ₑ ≤ B)
  (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))
  (hp : 1 < p) (hp₂ : p < 2) (f : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) :
  MeasureTheory.eLpNorm (↑↑(T f)) p MeasureTheory.volume ≤
    (ENNReal.ofReal (p.toReal / (p.toReal - 1)) *
            (2 * (2 ^ Fintype.card ι * (4 * ‖T‖ₑ ^ 2 + 1) + 4 * B)) +
          ENNReal.ofReal (p.toReal / (2 - p.toReal)) * (4 * ‖T‖ₑ ^ 2)) ^
        (1 / p.toReal) *
      MeasureTheory.eLpNorm (↑↑f) p MeasureTheory.volume
Lean

Formalized in Tau Ceti as ContinuousLinearMap.eLpNorm_le_of_hormander.

Other forms

The Calderón–Zygmund theorem. Formalized in Tau Ceti as ContinuousLinearMap.eLpNorm_le_of_hormander_adjoint.

ContinuousLinearMap.eLpNorm_le_of_hormander_adjoint.{u_1, u_4, u_5} {ι : Type u_1} [Fintype ι]
  [Nonempty ι] {p : ENNReal} {H : Type u_4} {K : Type u_5} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℝ K]
  [CompleteSpace K]
  (T :
    ↥(MeasureTheory.Lp H 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp K 2 MeasureTheory.volume))
  {k : (ι → ℝ) → (ι → ℝ) → K →L[ℝ] H} (hk : MeasureTheory.StronglyMeasurable (Function.uncurry k))
  {B : ENNReal}
  (hB : ∀ (y y' : ι → ℝ), ∫⁻ (x : ι → ℝ) in {x | 2 * dist y y' < dist x y'}, ‖k x y - k x y'‖ₑ ≤ B)
  (hrep :
    ∀ (b : ↥(MeasureTheory.Lp K 2 MeasureTheory.volume)) (y : ι → ℝ) (r : ℝ),
      (∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑b x = 0) →
        ∀ᵐ (x : ι → ℝ),
          x ∉ Metric.closedBall y r →
            ↑↑((ContinuousLinearMap.adjoint T) b) x = ∫ (z : ι → ℝ), (k x z) (↑↑b z))
  (hp : 2 < p) (hp_top : p ≠ ⊤) (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) :
  MeasureTheory.eLpNorm (↑↑(T f)) p MeasureTheory.volume ≤
    (ENNReal.ofReal p.toReal * (2 * (2 ^ Fintype.card ι * (4 * ‖T‖ₑ ^ 2 + 1) + 4 * B)) +
          ENNReal.ofReal (p.toReal / (p.toReal - 2)) * (4 * ‖T‖ₑ ^ 2)) ^
        (1 - 1 / p.toReal) *
      MeasureTheory.eLpNorm (↑↑f) p MeasureTheory.volume

The Calderón–Zygmund theorem, strong type (p, p) for 2 < p < ∞. Formalized in Tau Ceti as ContinuousLinearMap.eLpNorm_le_of_setLIntegral_compl_closedBall_adjoint_le.

ContinuousLinearMap.eLpNorm_le_of_setLIntegral_compl_closedBall_adjoint_le.{u_1, u_4, u_5}
  {ι : Type u_1} [Fintype ι] [Nonempty ι] {p : ENNReal} {H : Type u_4} {K : Type u_5}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℝ K] [CompleteSpace K]
  (T :
    ↥(MeasureTheory.Lp H 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp K 2 MeasureTheory.volume))
  {B : ENNReal} {c : ℝ}
  (hT :
    ∀ (b : ↥(MeasureTheory.Lp K 2 MeasureTheory.volume)) (y : ι → ℝ) (r : ℝ),
      (∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑b x = 0) →
        ∫ (x : ι → ℝ), ↑↑b x = 0 →
          ∫⁻ (x : ι → ℝ) in (Metric.closedBall y (c * r))ᶜ,
              ‖↑↑((ContinuousLinearMap.adjoint T) b) x‖ₑ ≤
            B * ∫⁻ (x : ι → ℝ), ‖↑↑b x‖ₑ)
  (hp : 2 < p) (hp_top : p ≠ ⊤) (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) :
  MeasureTheory.eLpNorm (↑↑(T f)) p MeasureTheory.volume ≤
    (ENNReal.ofReal p.toReal *
            (2 *
              (2 ^ Fintype.card ι * (4 * ‖T‖ₑ ^ 2) + ENNReal.ofReal c ^ Fintype.card ι + 4 * B)) +
          ENNReal.ofReal (p.toReal / (p.toReal - 2)) * (4 * ‖T‖ₑ ^ 2)) ^
        (1 - 1 / p.toReal) *
      MeasureTheory.eLpNorm (↑↑f) p MeasureTheory.volume

The Calderón–Zygmund theorem, strong type (p, p) for 1 < p < 2. Formalized in Tau Ceti as ContinuousLinearMap.eLpNorm_le_of_setLIntegral_compl_closedBall_le.

ContinuousLinearMap.eLpNorm_le_of_setLIntegral_compl_closedBall_le.{u_1, u_2, u_3} {ι : Type u_1}
  [Fintype ι] [Nonempty ι] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ENNReal}
  (T :
    ↥(MeasureTheory.Lp E 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume))
  {B : ENNReal} {c : ℝ}
  (hT :
    ∀ (b : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (y : ι → ℝ) (r : ℝ),
      (∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑b x = 0) →
        ∫ (x : ι → ℝ), ↑↑b x = 0 →
          ∫⁻ (x : ι → ℝ) in (Metric.closedBall y (c * r))ᶜ, ‖↑↑(T b) x‖ₑ ≤
            B * ∫⁻ (x : ι → ℝ), ‖↑↑b x‖ₑ)
  (hp : 1 < p) (hp₂ : p < 2) (f : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) :
  MeasureTheory.eLpNorm (↑↑(T f)) p MeasureTheory.volume ≤
    (ENNReal.ofReal (p.toReal / (p.toReal - 1)) *
            (2 *
              (2 ^ Fintype.card ι * (4 * ‖T‖ₑ ^ 2) + ENNReal.ofReal c ^ Fintype.card ι + 4 * B)) +
          ENNReal.ofReal (p.toReal / (2 - p.toReal)) * (4 * ‖T‖ₑ ^ 2)) ^
        (1 / p.toReal) *
      MeasureTheory.eLpNorm (↑↑f) p MeasureTheory.volume

The Calderón–Zygmund theorem for an operator given by a kernel. Formalized in Tau Ceti as ContinuousLinearMap.mul_volume_lt_enorm_le_of_hormander.

ContinuousLinearMap.mul_volume_lt_enorm_le_of_hormander.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι]
  {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [Nonempty ι] [CompleteSpace F]
  (T :
    ↥(MeasureTheory.Lp E 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume))
  {K : (ι → ℝ) → (ι → ℝ) → E →L[ℝ] F} (hK : MeasureTheory.StronglyMeasurable (Function.uncurry K))
  {B : ENNReal}
  (hB : ∀ (y y' : ι → ℝ), ∫⁻ (x : ι → ℝ) in {x | 2 * dist y y' < dist x y'}, ‖K x y - K x y'‖ₑ ≤ B)
  (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 * B) * ∫⁻ (x : ι → ℝ), ‖↑↑f x‖ₑ

The Calderón–Zygmund theorem for an operator with a standard kernel. Formalized in Tau Ceti as ContinuousLinearMap.mul_volume_lt_enorm_le_of_norm_sub_le_mul_rpow.

ContinuousLinearMap.mul_volume_lt_enorm_le_of_norm_sub_le_mul_rpow.{u_1, u_2, u_3} {ι : Type u_1}
  [Fintype ι] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [Nonempty ι]
  (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, weak type (1, 1). Formalized in Tau Ceti as ContinuousLinearMap.mul_volume_lt_enorm_le_of_setLIntegral_compl_closedBall_le.

ContinuousLinearMap.mul_volume_lt_enorm_le_of_setLIntegral_compl_closedBall_le.{u_1, u_2, u_3}
  {ι : Type u_1} [Fintype ι] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [Nonempty ι]
  (T :
    ↥(MeasureTheory.Lp E 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume))
  {B : ENNReal} {c : ℝ}
  (hT :
    ∀ (b : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (y : ι → ℝ) (r : ℝ),
      (∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑b x = 0) →
        ∫ (x : ι → ℝ), ↑↑b x = 0 →
          ∫⁻ (x : ι → ℝ) in (Metric.closedBall y (c * r))ᶜ, ‖↑↑(T b) x‖ₑ ≤
            B * ∫⁻ (x : ι → ℝ), ‖↑↑b x‖ₑ)
  (f : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (t : ENNReal) :
  t * MeasureTheory.volume {x | t < ‖↑↑(T f) x‖ₑ} ≤
    (2 ^ Fintype.card ι * (4 * ‖T‖ₑ ^ 2) + ENNReal.ofReal c ^ Fintype.card ι + 4 * B) *
      ∫⁻ (x : ι → ℝ), ‖↑↑f x‖ₑ

The Calderón–Zygmund theorem. Formalized in Tau Ceti as TauCeti.exists_eLpNorm_le_of_setLIntegral_compl_closedBall_le.

TauCeti.exists_eLpNorm_le_of_setLIntegral_compl_closedBall_le.{u_1, u_2, u_3} {ι : Type u_1}
  [Fintype ι] [Nonempty ι] {H : Type u_2} {K : Type u_3} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℝ K]
  [CompleteSpace K] {p : ENNReal} (c : ℝ) {M B B' : ENNReal} (hM : M ≠ ⊤) (hB : B ≠ ⊤)
  (hB' : B' ≠ ⊤) (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀
      (T :
        ↥(MeasureTheory.Lp H 2 MeasureTheory.volume) →L[ℝ]
          ↥(MeasureTheory.Lp K 2 MeasureTheory.volume)),
      ‖T‖ₑ ≤ M →
        (∀ (b : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (y : ι → ℝ) (r : ℝ),
            (∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑b x = 0) →
              ∫ (x : ι → ℝ), ↑↑b x = 0 →
                ∫⁻ (x : ι → ℝ) in (Metric.closedBall y (c * r))ᶜ, ‖↑↑(T b) x‖ₑ ≤
                  B * ∫⁻ (x : ι → ℝ), ‖↑↑b x‖ₑ) →
          (∀ (b : ↥(MeasureTheory.Lp K 2 MeasureTheory.volume)) (y : ι → ℝ) (r : ℝ),
              (∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑b x = 0) →
                ∫ (x : ι → ℝ), ↑↑b x = 0 →
                  ∫⁻ (x : ι → ℝ) in (Metric.closedBall y (c * r))ᶜ,
                      ‖↑↑((ContinuousLinearMap.adjoint T) b) x‖ₑ ≤
                    B' * ∫⁻ (x : ι → ℝ), ‖↑↑b x‖ₑ) →
            ∀ (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)),
              MeasureTheory.eLpNorm (↑↑(T f)) p MeasureTheory.volume ≤
                ↑C * MeasureTheory.eLpNorm (↑↑f) p MeasureTheory.volume

The Calderón–Zygmund theorem on an inner product space, strong type (p, p) for 1 < p < ∞. Formalized in Tau Ceti as ContinuousLinearMap.exists_eLpNorm_le_of_norm_sub_le_mul_rpow.

ContinuousLinearMap.exists_eLpNorm_le_of_norm_sub_le_mul_rpow.{u_1, u_4, u_5} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V]
  [FiniteDimensional ℝ V] {H : Type u_4} {K : Type u_5} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℝ K]
  [CompleteSpace K] {p : ENNReal} [Nontrivial V]
  (T :
    ↥(MeasureTheory.Lp H 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp K 2 MeasureTheory.volume))
  {k : V → V → H →L[ℝ] K} (hkm : MeasureTheory.StronglyMeasurable (Function.uncurry k))
  {k' : V → V → K →L[ℝ] H} (hk'm : MeasureTheory.StronglyMeasurable (Function.uncurry k'))
  {C₀ C C₀' C' : NNReal} {δ δ' : ℝ} (hδ : 0 < δ) (hδ' : 0 < δ')
  (hsize : ∀ (x y : V), x ≠ y → ‖k x y‖ ≤ ↑C₀ * dist x y ^ (-↑(Module.finrank ℝ V)))
  (hsize' : ∀ (x y : V), x ≠ y → ‖k' x y‖ ≤ ↑C₀' * dist x y ^ (-↑(Module.finrank ℝ V)))
  (hk :
    ∀ (x y y' : V),
      2 * dist y y' < dist x y' →
        ‖k x y - k x y'‖ ≤ ↑C * (dist y y' ^ δ * dist x y' ^ (-(↑(Module.finrank ℝ V) + δ))))
  (hk' :
    ∀ (x y y' : V),
      2 * dist y y' < dist x y' →
        ‖k' x y - k' x y'‖ ≤ ↑C' * (dist y y' ^ δ' * dist x y' ^ (-(↑(Module.finrank ℝ V) + δ'))))
  (hrep :
    ∀ (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (s : Set V),
      IsCompact s →
        (∀ᵐ (x : V), x ∉ s → ↑↑f x = 0) →
          ∀ᵐ (x : V), x ∉ s → ↑↑(T f) x = ∫ (z : V), (k x z) (↑↑f z))
  (hrep' :
    ∀ (f : ↥(MeasureTheory.Lp K 2 MeasureTheory.volume)) (s : Set V),
      IsCompact s →
        (∀ᵐ (x : V), x ∉ s → ↑↑f x = 0) →
          ∀ᵐ (x : V), x ∉ s → ↑↑((ContinuousLinearMap.adjoint T) f) x = ∫ (z : V), (k' x z) (↑↑f z))
  (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)),
      MeasureTheory.eLpNorm (↑↑(T f)) p MeasureTheory.volume ≤
        ↑C * MeasureTheory.eLpNorm (↑↑f) p MeasureTheory.volume

The Calderón–Zygmund theorem on an inner product space, weak type (1, 1). Formalized in Tau Ceti as ContinuousLinearMap.exists_mul_volume_lt_enorm_le_of_norm_sub_le_mul_rpow.

ContinuousLinearMap.exists_mul_volume_lt_enorm_le_of_norm_sub_le_mul_rpow.{u_1, u_2, u_3}
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V]
  [FiniteDimensional ℝ V] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [Nontrivial V]
  (T :
    ↥(MeasureTheory.Lp E 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume))
  {k : V → V → E →L[ℝ] F} (hkm : MeasureTheory.StronglyMeasurable (Function.uncurry k))
  {C₀ C : NNReal} {δ : ℝ} (hδ : 0 < δ)
  (hsize : ∀ (x y : V), x ≠ y → ‖k x y‖ ≤ ↑C₀ * dist x y ^ (-↑(Module.finrank ℝ V)))
  (hk :
    ∀ (x y y' : V),
      2 * dist y y' < dist x y' →
        ‖k x y - k x y'‖ ≤ ↑C * (dist y y' ^ δ * dist x y' ^ (-(↑(Module.finrank ℝ V) + δ))))
  (hrep :
    ∀ (f : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (s : Set V),
      IsCompact s →
        (∀ᵐ (x : V), x ∉ s → ↑↑f x = 0) →
          ∀ᵐ (x : V), x ∉ s → ↑↑(T f) x = ∫ (z : V), (k x z) (↑↑f z)) :
  ∃ A,
    ∀ (f : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (t : ENNReal),
      t * MeasureTheory.volume {x | t < ‖↑↑(T f) x‖ₑ} ≤ ↑A * ∫⁻ (x : V), ‖↑↑f x‖ₑ

The Calderón–Zygmund theorem on an inner product space under Hörmander's condition. Formalized in Tau Ceti as TauCeti.exists_eLpNorm_le_of_hormander.

TauCeti.exists_eLpNorm_le_of_hormander.{u_1, u_4, u_5} {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {H : Type u_4}
  {K : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℝ K] [CompleteSpace K] {p : ENNReal} [Nontrivial V]
  {M B B' : ENNReal} (hM : M ≠ ⊤) (hB : B ≠ ⊤) (hB' : B' ≠ ⊤) (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀
      (T :
        ↥(MeasureTheory.Lp H 2 MeasureTheory.volume) →L[ℝ]
          ↥(MeasureTheory.Lp K 2 MeasureTheory.volume))
      (k : V → V → H →L[ℝ] K) (k' : V → V → K →L[ℝ] H),
      ‖T‖ₑ ≤ M →
        MeasureTheory.StronglyMeasurable (Function.uncurry k) →
          MeasureTheory.StronglyMeasurable (Function.uncurry k') →
            (∀ (y y' : V), ∫⁻ (x : V) in {x | 2 * dist y y' < dist x y'}, ‖k x y - k x y'‖ₑ ≤ B) →
              (∀ (y y' : V),
                  ∫⁻ (x : V) in {x | 2 * dist y y' < dist x y'}, ‖k' x y - k' x y'‖ₑ ≤ B') →
                (∀ (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (s : Set V),
                    IsCompact s →
                      (∀ᵐ (x : V), x ∉ s → ↑↑f x = 0) →
                        ∀ᵐ (x : V), x ∉ s → ↑↑(T f) x = ∫ (z : V), (k x z) (↑↑f z)) →
                  (∀ (f : ↥(MeasureTheory.Lp K 2 MeasureTheory.volume)) (s : Set V),
                      IsCompact s →
                        (∀ᵐ (x : V), x ∉ s → ↑↑f x = 0) →
                          ∀ᵐ (x : V),
                            x ∉ s →
                              ↑↑((ContinuousLinearMap.adjoint T) f) x =
                                ∫ (z : V), (k' x z) (↑↑f z)) →
                    ∀ (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)),
                      MeasureTheory.eLpNorm (↑↑(T f)) p MeasureTheory.volume ≤
                        ↑C * MeasureTheory.eLpNorm (↑↑f) p MeasureTheory.volume

The Calderón–Zygmund theorem on an inner product space under Hörmander's condition. Formalized in Tau Ceti as TauCeti.exists_mul_volume_lt_enorm_le_of_hormander.

TauCeti.exists_mul_volume_lt_enorm_le_of_hormander.{u_1, u_2, u_3} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V]
  [FiniteDimensional ℝ V] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [Nontrivial V]
  {M B : ENNReal} (hM : M ≠ ⊤) (hB : B ≠ ⊤) :
  ∃ A,
    ∀
      (T :
        ↥(MeasureTheory.Lp E 2 MeasureTheory.volume) →L[ℝ]
          ↥(MeasureTheory.Lp F 2 MeasureTheory.volume))
      (k : V → V → E →L[ℝ] F),
      ‖T‖ₑ ≤ M →
        MeasureTheory.StronglyMeasurable (Function.uncurry k) →
          (∀ (y y' : V), ∫⁻ (x : V) in {x | 2 * dist y y' < dist x y'}, ‖k x y - k x y'‖ₑ ≤ B) →
            (∀ (f : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (s : Set V),
                IsCompact s →
                  (∀ᵐ (x : V), x ∉ s → ↑↑f x = 0) →
                    ∀ᵐ (x : V), x ∉ s → ↑↑(T f) x = ∫ (z : V), (k x z) (↑↑f z)) →
              ∀ (f : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (t : ENNReal),
                t * MeasureTheory.volume {x | t < ‖↑↑(T f) x‖ₑ} ≤ ↑A * ∫⁻ (x : V), ‖↑↑f x‖ₑ
Sources
LeanContinuousLinearMap.eLpNorm_le_of_hormander · ContinuousLinearMap.eLpNorm_le_of_hormander_adjoint · ContinuousLinearMap.eLpNorm_le_of_setLIntegral_compl_closedBall_adjoint_le · ContinuousLinearMap.eLpNorm_le_of_setLIntegral_compl_closedBall_le · ContinuousLinearMap.mul_volume_lt_enorm_le_of_hormander · ContinuousLinearMap.mul_volume_lt_enorm_le_of_norm_sub_le_mul_rpow · ContinuousLinearMap.mul_volume_lt_enorm_le_of_setLIntegral_compl_closedBall_le · TauCeti.exists_eLpNorm_le_of_setLIntegral_compl_closedBall_le · ContinuousLinearMap.exists_eLpNorm_le_of_norm_sub_le_mul_rpow · ContinuousLinearMap.exists_mul_volume_lt_enorm_le_of_norm_sub_le_mul_rpow · TauCeti.exists_eLpNorm_le_of_hormander · TauCeti.exists_mul_volume_lt_enorm_le_of_hormander
Uses 2 · Used by 3
Proof usesHölder's inequality for the integral of a product · Lebesgue's differentiation theorem along dyadic cubes
Used byThe Calderón–Zygmund estimate ‖D²u‖_p ≤ C ‖Δu‖_p · The Mihlin–Hörmander multiplier theorem on Lᵖ · The full strong-type Calderón–Zygmund theorem

TheoremCauchy–Schwarz on a circle#

The square of the circle integral of g is at most 2 π ρ — for ρ > 0 the circumference of the circle — times the circle integral of g ^ 2.

Only the angular trace of g along the circle at hand need be measurable; nothing is assumed of g off that circle. Both sides vanish for a nonpositive radius, so no positivity is assumed.

TauCeti.circleLIntegral_sq_le {g : ℂ → ENNReal} (ζ : ℂ) (ρ : ℝ)
  (hg :
    AEMeasurable (fun θ => g (circleMap ζ ρ θ))
      (MeasureTheory.volume.restrict (Set.Ioo (-Real.pi) Real.pi))) :
  TauCeti.circleLIntegral g ζ ρ ^ 2 ≤
    ENNReal.ofReal (2 * Real.pi * ρ) * TauCeti.circleLIntegral (fun z => g z ^ 2) ζ ρ
Lean

Formalized in Tau Ceti as TauCeti.circleLIntegral_sq_le.

Sources
LeanTauCeti.circleLIntegral_sq_le
Uses 1 · Used by 1
Proof usesHölder's inequality for the integral of a product
Used byWolff's lemma (TauCeti.exists_circleLIntegral_sq_lt)

TheoremThe divergence theorem on a half-space (TauCeti.setIntegral_setOf_inner_lt_trace_fderiv)#

For a unit vector ν and a compactly supported C¹ vector field φ, the integral of the divergence tr (Dφ) over the half-space {x | ⟪x, ν⟫ < c} is the flux ∫ ⟪φ, ν⟫ of φ through the boundary hyperplane {x | ⟪x, ν⟫ = c} against (n - 1)-dimensional Hausdorff measure.

TauCeti.setIntegral_setOf_inner_lt_trace_fderiv.{u_1} {F : Type u_1} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] {ν : F} [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F]
  (hν : ‖ν‖ = 1) (c : ℝ) {φ : F → F} (hφ : ContDiff ℝ 1 φ) (hφc : HasCompactSupport φ) :
  ∫ (x : F) in {x | inner ℝ x ν < c}, (LinearMap.trace ℝ F) ↑(fderiv ℝ φ x) =
    ∫ (x : F) in {x | inner ℝ x ν = c},
      inner ℝ (φ x) ν ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ F - 1)
Lean

Formalized in Tau Ceti as TauCeti.setIntegral_setOf_inner_lt_trace_fderiv.

Other forms

The divergence theorem on a half-space, directional form. Formalized in Tau Ceti as TauCeti.setIntegral_setOf_inner_lt_fderiv_apply.

TauCeti.setIntegral_setOf_inner_lt_fderiv_apply.{u_1} {F : Type u_1} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] {ν : F} [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F]
  (hν : ‖ν‖ = 1) (c : ℝ) {g : F → ℝ} (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (v : F) :
  ∫ (x : F) in {x | inner ℝ x ν < c}, (fderiv ℝ g x) v =
    inner ℝ v ν *
      ∫ (x : F) in {x | inner ℝ x ν = c},
        g x ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ F - 1)
Sources
LeanTauCeti.setIntegral_setOf_inner_lt_trace_fderiv · TauCeti.setIntegral_setOf_inner_lt_fderiv_apply
Uses 1
Proof usesThe divergence theorem on a half-space (TauCeti.setIntegral_normalHalfSpace_fderiv_apply)

TheoremThe divergence theorem on an affine parallelepiped#

Let A u = p + L u and let F be a flux field continuous on the parallelepiped A '' [0, 1]ⁿ⁺¹, differentiable with derivatives F' i at A u for every interior point u of the unit cube off a countable set, and with u ↦ div F (A u) integrable on the unit cube. Then det L times the integral of div F ∘ A over the unit cube is the boundary sum of the cofactor pullback H = L.affineFluxPullback p F: the sum over j of the integral of H j over the front face u j = 1 minus that over the back face u j = 0. The determinant is signed.

ContinuousLinearEquiv.integral_divergence_affineFluxPullback.{u_2} {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : (Fin (n + 1) → ℝ) ≃L[ℝ] Fin (n + 1) → ℝ)
  (p : Fin (n + 1) → ℝ) (F : Fin (n + 1) → (Fin (n + 1) → ℝ) → E)
  (F' : Fin (n + 1) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E) (s : Set (Fin (n + 1) → ℝ))
  (hs : s.Countable)
  (Hc : ∀ (i : Fin (n + 1)), ContinuousOn (F i) ((fun u => p + L u) '' Set.Icc 0 1))
  (Hd :
    ∀ u ∈ (Set.univ.pi fun x => Set.Ioo 0 1) \ s,
      ∀ (i : Fin (n + 1)), HasFDerivAt (F i) (F' i (p + L u)) (p + L u))
  (Hi :
    MeasureTheory.IntegrableOn (fun u => ∑ i, (F' i (p + L u)) (Pi.single i 1)) (Set.Icc 0 1)
      MeasureTheory.volume) :
  LinearMap.det ↑↑L •
      ∫ (u : Fin (n + 1) → ℝ) in Set.Icc 0 1, ∑ i, (F' i (p + L u)) (Pi.single i 1) =
    ∑ j,
      ((∫ (x : Fin n → ℝ) in Set.Icc 0 1, L.affineFluxPullback p F j (j.insertNth 1 x)) -
        ∫ (x : Fin n → ℝ) in Set.Icc 0 1, L.affineFluxPullback p F j (j.insertNth 0 x))
Lean

Formalized in Tau Ceti as ContinuousLinearEquiv.integral_divergence_affineFluxPullback.

Sources
LeanContinuousLinearEquiv.integral_divergence_affineFluxPullback

TheoremThe dyadic John–Nirenberg inequality for any additive Haar measure#

the superlevel set at 2ⁿ⁺¹ N M has measure at most 2⁻ᴺ times the cube measure.

TauCeti.measure_lt_enorm_sub_setAverage_le_inv_two_pow.{u_1, u_2} {ι : Type u_1} [Fintype ι]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {q₀ : ℤ × (ι → ℤ)}
  {M : NNReal} [CompleteSpace E] {μ : MeasureTheory.Measure (ι → ℝ)} [μ.IsAddHaarMeasure]
  (hf : MeasureTheory.IntegrableOn f (TauCeti.dyadicCube q₀.1 q₀.2) μ)
  (hM :
    ∀ (q : ℤ × (ι → ℤ)),
      TauCeti.dyadicCube q.1 q.2 ⊆ TauCeti.dyadicCube q₀.1 q₀.2 →
        ⨍⁻ (x : ι → ℝ) in TauCeti.dyadicCube q.1 q.2,
            ‖f x - ⨍ (y : ι → ℝ) in TauCeti.dyadicCube q.1 q.2, f y ∂μ‖ₑ ∂μ ≤
          ↑M)
  (N : ℕ) :
  μ
      {x |
        x ∈ TauCeti.dyadicCube q₀.1 q₀.2 ∧
          2 ^ (Fintype.card ι + 1) * ↑N * ↑M <
            ‖f x - ⨍ (y : ι → ℝ) in TauCeti.dyadicCube q₀.1 q₀.2, f y ∂μ‖ₑ} ≤
    2⁻¹ ^ N * μ (TauCeti.dyadicCube q₀.1 q₀.2)
Lean

Formalized in Tau Ceti as TauCeti.measure_lt_enorm_sub_setAverage_le_inv_two_pow.

Sources
LeanTauCeti.measure_lt_enorm_sub_setAverage_le_inv_two_pow
Uses 1
Proof usesLebesgue's differentiation theorem along dyadic cubes

TheoremThe Fefferman–Stein inequality#

For 1 < p < ∞ and integrable f on ℝⁿ = ι → ℝ, n ≥ 1, the Lᵖ norm of f is controlled by that of its sharp maximal function f^#, with a constant depending only on n and p:

‖f‖_p ≤ (2^(p + 1) 2^((p + 2n + 2) p))^(1 / p) ‖f^#‖_p.

Balls are taken in the sup distance of ι → ℝ. The integrability of f cannot be dropped altogether, since f^# vanishes for constant f; and positive dimension is needed, since in dimension 0 every ball is the whole space and f^# vanishes identically.

TauCeti.eLpNorm_le_eLpNorm_sharpMaximalFunction.{u_1, u_2} {ι : Type u_1} [Fintype ι] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [Nonempty ι] {f : (ι → ℝ) → F}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) {p : ENNReal} (hp : 1 < p)
  (hp_top : p ≠ ⊤) :
  MeasureTheory.eLpNorm f p MeasureTheory.volume ≤
    ENNReal.ofReal (2 ^ (p.toReal + 1) * 2 ^ ((p.toReal + 2 * ↑(Fintype.card ι) + 2) * p.toReal)) ^
        (1 / p.toReal) *
      MeasureTheory.eLpNorm (TauCeti.sharpMaximalFunction MeasureTheory.volume f) p
        MeasureTheory.volume
Lean

Formalized in Tau Ceti as TauCeti.eLpNorm_le_eLpNorm_sharpMaximalFunction.

Other forms

The Fefferman–Stein inequality, as an inequality between the integrals ∫⁻ ‖·‖ₑ ^ p. Formalized in Tau Ceti as TauCeti.lintegral_enorm_rpow_le_lintegral_sharpMaximalFunction_rpow.

TauCeti.lintegral_enorm_rpow_le_lintegral_sharpMaximalFunction_rpow.{u_1, u_2} {ι : Type u_1}
  [Fintype ι] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [Nonempty ι]
  {f : (ι → ℝ) → F} (hf : MeasureTheory.Integrable f MeasureTheory.volume) {p : ℝ} (hp : 1 < p) :
  ∫⁻ (x : ι → ℝ), ‖f x‖ₑ ^ p ≤
    ENNReal.ofReal (2 ^ (p + 1) * 2 ^ ((p + 2 * ↑(Fintype.card ι) + 2) * p)) *
      ∫⁻ (x : ι → ℝ), TauCeti.sharpMaximalFunction MeasureTheory.volume f x ^ p
Sources
LeanTauCeti.eLpNorm_le_eLpNorm_sharpMaximalFunction · TauCeti.lintegral_enorm_rpow_le_lintegral_sharpMaximalFunction_rpow
Uses 1
Proof usesLebesgue's differentiation theorem along dyadic cubes

TheoremThe full strong-type Calderón–Zygmund theorem#

An L²-bounded operator for which both it and its adjoint satisfy the cancellation estimate with finite constants extends to a bounded operator on Lᵖ(ℝⁿ; H) → Lᵖ(ℝⁿ; K) for every 1 < p < ∞. On L² ∩ Lᵖ, the extended map agrees almost everywhere with the given operator.

ContinuousLinearMap.exists_strongTypeExtension_of_setLIntegral_compl_closedBall_le.{u_1, u_2, u_3}
  {ι : Type u_1} [Fintype ι] [Nonempty ι] {H : Type u_2} {K : Type u_3} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℝ K]
  [CompleteSpace K] {p : ENNReal} [Fact (1 ≤ p)]
  (T :
    ↥(MeasureTheory.Lp H 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp K 2 MeasureTheory.volume))
  {B B' : ENNReal} (hB : B ≠ ⊤) (hB' : B' ≠ ⊤)
  (hT :
    ∀ (b : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (y : ι → ℝ) (r : ℝ),
      (∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑b x = 0) →
        ∫ (x : ι → ℝ), ↑↑b x = 0 →
          ∫⁻ (x : ι → ℝ) in (Metric.closedBall y (2 * r))ᶜ, ‖↑↑(T b) x‖ₑ ≤
            B * ∫⁻ (x : ι → ℝ), ‖↑↑b x‖ₑ)
  (hT' :
    ∀ (b : ↥(MeasureTheory.Lp K 2 MeasureTheory.volume)) (y : ι → ℝ) (r : ℝ),
      (∀ᵐ (x : ι → ℝ), x ∉ Metric.closedBall y r → ↑↑b x = 0) →
        ∫ (x : ι → ℝ), ↑↑b x = 0 →
          ∫⁻ (x : ι → ℝ) in (Metric.closedBall y (2 * r))ᶜ,
              ‖↑↑((ContinuousLinearMap.adjoint T) b) x‖ₑ ≤
            B' * ∫⁻ (x : ι → ℝ), ‖↑↑b x‖ₑ)
  (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C S,
    ‖S‖ ≤ ↑C ∧
      ∀ (f : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume))
        (hf : MeasureTheory.MemLp (↑↑f) p MeasureTheory.volume),
        ↑↑(S (MeasureTheory.MemLp.toLp (↑↑f) hf)) =ᵐ[MeasureTheory.volume] ↑↑(T f)
Lean

Formalized in Tau Ceti as ContinuousLinearMap.exists_strongTypeExtension_of_setLIntegral_compl_closedBall_le.

Sources
LeanContinuousLinearMap.exists_strongTypeExtension_of_setLIntegral_compl_closedBall_le
Uses 1
Proof usesThe Calderón–Zygmund theorem

TheoremThe fundamental theorem of calculus along a coordinate of the standard simplex#

For a function g that is C¹ on Δᵖ⁺¹, the integral over Δᵖ⁺¹ of its partial derivative in the direction e_j is the integral over Δᵖ of the difference of its values at the points of the faces ∑ xᵢ = 1 and x_j = 0 whose other coordinates are given by y ∈ Δᵖ.

ContDiffOn.integral_fderivWithin_fullSimplex.{u_1} {F : Type u_1} [NormedAddCommGroup F]
  [NormedSpace ℝ F] [CompleteSpace F] {p : ℕ} {g : EuclideanSpace ℝ (Fin (p + 1)) → F}
  (hg : ContDiffOn ℝ 1 g (TauCeti.fullSimplex (p + 1))) (j : Fin (p + 1)) :
  ∫ (x : EuclideanSpace ℝ (Fin (p + 1))) in TauCeti.fullSimplex (p + 1),
      (fderivWithin ℝ g (TauCeti.fullSimplex (p + 1)) x) (EuclideanSpace.single j 1) =
    ∫ (y : EuclideanSpace ℝ (Fin p)) in TauCeti.fullSimplex p,
      g (WithLp.toLp 2 (j.insertNth (1 - ∑ k, y.ofLp k) y.ofLp)) -
        g (WithLp.toLp 2 (j.insertNth 0 y.ofLp))
Lean

Formalized in Tau Ceti as ContDiffOn.integral_fderivWithin_fullSimplex.

Sources
LeanContDiffOn.integral_fderivWithin_fullSimplex
Used by 1
Used byStokes' theorem on the standard simplex

TheoremThe fundamental theorem of calculus in the first coordinate#

The integral of a continuous partial derivative φ = ∂₁ Φ over the rectangle [a₁, b₁] × [a₂, b₂] is the integral over [a₂, b₂] of the difference of the values of Φ on the two vertical sides.

TauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_fst.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a₁ b₁ a₂ b₂ : ℝ} {Φ φ : ℝ × ℝ → E}
  (hφ : Continuous φ) (hΦ : ∀ (s t : ℝ), HasDerivAt (fun s => Φ (s, t)) (φ (s, t)) s)
  (hab : a₁ ≤ b₁) :
  ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, φ z =
    ∫ (t : ℝ) in Set.Icc a₂ b₂, Φ (b₁, t) - Φ (a₁, t)
Lean

Formalized in Tau Ceti as TauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_fst.

Sources
LeanTauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_fst

TheoremThe fundamental theorem of calculus in the second coordinate#

The integral of a continuous partial derivative φ = ∂₂ Φ over the rectangle [a₁, b₁] × [a₂, b₂] is the integral over [a₁, b₁] of the difference of the values of Φ on the two horizontal sides.

TauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_snd.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a₁ b₁ a₂ b₂ : ℝ} {Φ φ : ℝ × ℝ → E}
  (hφ : Continuous φ) (hΦ : ∀ (s t : ℝ), HasDerivAt (fun t => Φ (s, t)) (φ (s, t)) t)
  (hab : a₂ ≤ b₂) :
  ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, φ z =
    ∫ (s : ℝ) in Set.Icc a₁ b₁, Φ (s, b₂) - Φ (s, a₂)
Lean

Formalized in Tau Ceti as TauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_snd.

Sources
LeanTauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_snd

TheoremGreen's formula on a closed annulus#

For a C² map near the annulus of radii 0 ≤ a ≤ b, the integral of the alternating part of a bilinear pairing of its derivatives equals the outer circle integral of B u du minus the inner circle integral. Both circles are parametrized counterclockwise; their difference gives the boundary orientation.

ContinuousLinearMap.integral_bilinear_fderiv_sub_annulus.{u_2, u_3} {V : Type u_2} {W : Type u_3}
  [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W]
  (B : V →L[ℝ] V →L[ℝ] W) {u : ℂ → V} (z₀ : ℂ) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b)
  (hu : ∀ z ∈ {z | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, ContDiffAt ℝ 2 u z) :
  ∫ (z : ℂ) in {z | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b},
      (B ((fderiv ℝ u z) 1)) ((fderiv ℝ u z) Complex.I) -
        (B ((fderiv ℝ u z) Complex.I)) ((fderiv ℝ u z) 1) =
    (∫ (θ : ℝ) in -Real.pi..Real.pi,
        (B (u (circleMap z₀ b θ)))
          ((fderiv ℝ u (circleMap z₀ b θ)) (circleMap 0 b θ * Complex.I))) -
      ∫ (θ : ℝ) in -Real.pi..Real.pi,
        (B (u (circleMap z₀ a θ))) ((fderiv ℝ u (circleMap z₀ a θ)) (circleMap 0 a θ * Complex.I))
Lean

Formalized in Tau Ceti as ContinuousLinearMap.integral_bilinear_fderiv_sub_annulus.

Other forms

Green's formula for a bilinear pairing of partial derivatives. Formalized in Tau Ceti as ContinuousLinearMap.integral_bilinear_fderiv_sub_prod_Icc.

ContinuousLinearMap.integral_bilinear_fderiv_sub_prod_Icc.{u_2, u_3} {V : Type u_2} {W : Type u_3}
  [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W]
  (B : V →L[ℝ] V →L[ℝ] W) {u : ℝ × ℝ → V} {a b : ℝ × ℝ} (hle : a ≤ b)
  (hu : ∀ z ∈ Set.Icc a b, ContDiffAt ℝ 2 u z) :
  ∫ (z : ℝ × ℝ) in Set.Icc a b,
      (B ((fderiv ℝ u z) (1, 0))) ((fderiv ℝ u z) (0, 1)) -
        (B ((fderiv ℝ u z) (0, 1))) ((fderiv ℝ u z) (1, 0)) =
    ((∫ (t : ℝ) in a.2..b.2, (B (u (b.1, t))) ((fderiv ℝ u (b.1, t)) (0, 1))) -
        ∫ (t : ℝ) in a.2..b.2, (B (u (a.1, t))) ((fderiv ℝ u (a.1, t)) (0, 1))) -
      ((∫ (s : ℝ) in a.1..b.1, (B (u (s, b.2))) ((fderiv ℝ u (s, b.2)) (1, 0))) -
        ∫ (s : ℝ) in a.1..b.1, (B (u (s, a.2))) ((fderiv ℝ u (s, a.2)) (1, 0)))
Sources
LeanContinuousLinearMap.integral_bilinear_fderiv_sub_annulus · ContinuousLinearMap.integral_bilinear_fderiv_sub_prod_Icc
Used by 1
Used byStokes' formula for symplectic area on an annulus

TheoremThe Hardy–Littlewood maximal inequality#

The Hardy–Littlewood maximal inequality, the strong-type (p, p) bound for 1 < p < ∞, in terms of representative-level Lᵖ seminorms.

Together with TauCeti.maximalFunction_le_eLpNormEssSup (the case p = ∞) and TauCeti.mul_measure_lt_maximalFunction_le (the weak-type substitute at p = 1), this gives the representative-level strong estimate for the maximal function. The resulting finiteness statement is recorded by TauCeti.eLpNorm_maximalFunction_lt_top below.

TauCeti.eLpNorm_maximalFunction_le.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F]
  [TopologicalSpace F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E → F}
  (hf : AEMeasurable (fun x => ‖f x‖ₑ) μ) {p : ENNReal} (hp : 1 < p) (hp_top : p ≠ ⊤) :
  MeasureTheory.eLpNorm (TauCeti.maximalFunction μ f) p μ ≤
    (ENNReal.ofReal (2 * p.toReal * 2 ^ (p.toReal - 1) / (p.toReal - 1)) * 4 ^ Module.finrank ℝ E) ^
        (1 / p.toReal) *
      MeasureTheory.eLpNorm f p μ
Lean

Formalized in Tau Ceti as TauCeti.eLpNorm_maximalFunction_le.

Other forms

The Hardy–Littlewood maximal inequality. Formalized in Tau Ceti as TauCeti.lintegral_rpow_maximalFunction_le.

TauCeti.lintegral_rpow_maximalFunction_le.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] [ENorm F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E → F}
  (hf : AEMeasurable (fun x => ‖f x‖ₑ) μ) {p : ℝ} (hp : 1 < p) :
  ∫⁻ (x : E), TauCeti.maximalFunction μ f x ^ p ∂μ ≤
    ENNReal.ofReal (2 * p * 2 ^ (p - 1) / (p - 1)) * 4 ^ Module.finrank ℝ E *
      ∫⁻ (x : E), ‖f x‖ₑ ^ p ∂μ

The Hardy–Littlewood maximal inequality, in quotient form. Formalized in Tau Ceti as TauCeti.measure_lt_maximalFunction_le.

TauCeti.measure_lt_maximalFunction_le.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] [ENorm F] {t : ENNReal} (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
  (f : E → F) (ht : t ≠ 0) :
  μ {x | t < TauCeti.maximalFunction μ f x} ≤ (4 ^ Module.finrank ℝ E * ∫⁻ (x : E), ‖f x‖ₑ ∂μ) / t

The Hardy–Littlewood maximal inequality, the weak-type (1,1) bound. Formalized in Tau Ceti as TauCeti.mul_measure_lt_maximalFunction_le.

TauCeti.mul_measure_lt_maximalFunction_le.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] [ENorm F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E → F)
  (t : ENNReal) :
  t * μ {x | t < TauCeti.maximalFunction μ f x} ≤ 4 ^ Module.finrank ℝ E * ∫⁻ (x : E), ‖f x‖ₑ ∂μ
Sources
LeanTauCeti.eLpNorm_maximalFunction_le · TauCeti.lintegral_rpow_maximalFunction_le · TauCeti.measure_lt_maximalFunction_le · TauCeti.mul_measure_lt_maximalFunction_le
Uses 1
Proof usesThe Vitali covering estimate

TheoremHölder's bound on an average#

the average of f over a set s is at most μ s ^ (-1/p) times the Lᵖ seminorm of f on s. At p = 1 this is the bound by the average of ‖f‖, and the volume factor sharpens as p grows because a larger exponent controls the mass of s more efficiently. No measurability or integrability hypothesis is needed, since a function not integrable on s has average zero.

TauCeti.enorm_setAverage_le.{u_1, u_2} {α : Type u_1} {F : Type u_2} [MeasurableSpace α]
  {mu : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → F} {p : ENNReal}
  {s : Set α} (hp : 1 ≤ p) (hp' : p ≠ ⊤) :
  ‖⨍ (y : α) in s, f y ∂mu‖ₑ ≤ mu s ^ (-p.toReal⁻¹) * MeasureTheory.eLpNorm f p (mu.restrict s)
Lean

Formalized in Tau Ceti as TauCeti.enorm_setAverage_le.

Other forms

Hölder's bound on an average, in ∫⁻ form. Formalized in Tau Ceti as TauCeti.enorm_setAverage_rpow_le.

TauCeti.enorm_setAverage_rpow_le.{u_1, u_2} {α : Type u_1} {F : Type u_2} [MeasurableSpace α]
  {mu : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → F} {s : Set α}
  {q : ℝ} (hq : 1 ≤ q) : ‖⨍ (y : α) in s, f y ∂mu‖ₑ ^ q ≤ (mu s)⁻¹ * ∫⁻ (y : α) in s, ‖f y‖ₑ ^ q ∂mu
Sources
LeanTauCeti.enorm_setAverage_le · TauCeti.enorm_setAverage_rpow_le
Uses 1 · Used by 5
Proof usesHölder's inequality for the integral of a product
Used byThe interior Schauder estimate on small balls · Schauder estimate for a Hessian supported in a ball · The supercritical Sobolev multiplication estimate · The Poincaré–Wirtinger inequality on a closed Riemannian manifold · The Fréchet--Kolmogorov compactness criterion

TheoremHölder's inequality for Young's exponents#

Let 1 ≤ p ≤ q and let r be the exponent with 1/p + 1/r = 1 + 1/q. Then ∫⁻ k g ≤ (∫⁻ k ^ r g ^ p) ^ (1/q) (∫⁻ k ^ r) ^ (1 - 1/p) (∫⁻ g ^ p) ^ (1/p - 1/q).

This is Hölder's inequality with the three exponents 1/q, 1 - 1/p and 1/p - 1/q, which add up to 1, applied to the factorization k g = (k ^ r g ^ p) ^ (1/q) (k ^ r) ^ (1 - 1/p) (g ^ p) ^ (1/p - 1/q).

TauCeti.lintegral_mul_le_of_inv_add_inv_eq.{u_1} {β : Type u_1} [MeasurableSpace β]
  {ν : MeasureTheory.Measure β} {k g : β → ENNReal} (hk : AEMeasurable k ν) (hg : AEMeasurable g ν)
  {p q r : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) (hr : p⁻¹ + r⁻¹ = 1 + q⁻¹) :
  ∫⁻ (y : β), k y * g y ∂ν ≤
    (∫⁻ (y : β), k y ^ r * g y ^ p ∂ν) ^ q⁻¹ * (∫⁻ (y : β), k y ^ r ∂ν) ^ (1 - p⁻¹) *
      (∫⁻ (y : β), g y ^ p ∂ν) ^ (p⁻¹ - q⁻¹)
Lean

Formalized in Tau Ceti as TauCeti.lintegral_mul_le_of_inv_add_inv_eq.

Other forms

Hölder's inequality for a function vanishing off a set. Formalized in Tau Ceti as TauCeti.MeasureTheory.abs_integral_mul_le_eLpNorm_mul_eLpNorm_mul_measureReal_rpow.

TauCeti.MeasureTheory.abs_integral_mul_le_eLpNorm_mul_eLpNorm_mul_measureReal_rpow.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f w : Ω → ℝ} {r s : NNReal}
  (hr : 0 < r) (hs : 0 < s) (hrs : (↑r)⁻¹ + (↑s)⁻¹ ≤ 1) (hf : MeasureTheory.MemLp f (↑r) μ)
  (hw : MeasureTheory.MemLp w (↑s) μ) {A : Set Ω} (hA : MeasurableSet A) (hAfin : μ A ≠ ⊤)
  (hwA : ∀ᵐ (x : Ω) ∂μ, x ∉ A → w x = 0) :
  |∫ (x : Ω), f x * w x ∂μ| ≤
    (MeasureTheory.eLpNorm f (↑r) μ).toReal * (MeasureTheory.eLpNorm w (↑s) μ).toReal *
      μ.real A ^ (1 - (↑r)⁻¹ - (↑s)⁻¹)
Sources
LeanTauCeti.lintegral_mul_le_of_inv_add_inv_eq · TauCeti.MeasureTheory.abs_integral_mul_le_eLpNorm_mul_eLpNorm_mul_measureReal_rpow
Used by 4
Used byDe Giorgi's interior oscillation estimate · De Giorgi's theorem: Hölder continuity of weak solutions · Stampacchia's global bound · Young's inequality for integral kernels

TheoremJensen's inequality for the square of a mean#

On a set s of finite nonzero measure, the square of the mean of ‖g‖ is at most the mean of ‖g‖².

TauCeti.sq_setAverage_norm_le_setAverage_norm_sq.{u_1, u_2} {X : Type u_1} {F : Type u_2}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] {g : X → F} {s : Set X}
  (hs0 : μ s ≠ 0) (hs : μ s ≠ ⊤) (hg : MeasureTheory.IntegrableOn g s μ)
  (hg2 : MeasureTheory.IntegrableOn (fun x => ‖g x‖ ^ 2) s μ) :
  (⨍ (x : X) in s, ‖g x‖ ∂μ) ^ 2 ≤ ⨍ (x : X) in s, ‖g x‖ ^ 2 ∂μ
Lean

Formalized in Tau Ceti as TauCeti.sq_setAverage_norm_le_setAverage_norm_sq.

Sources
LeanTauCeti.sq_setAverage_norm_le_setAverage_norm_sq
Used by 1
Used byThe interior Schauder estimate on small balls

TheoremThe John–Nirenberg inequality on Euclidean balls#

There are constants A > 0 and C, depending only on the dimension n, such that the following holds for every additive Haar measure μ on ℝⁿ = EuclideanSpace ℝ ι. Let f : ℝⁿ → E be integrable on the ball B(x₀, R), with mean oscillation ⨍_B ‖f - f_B‖ ≤ M on every ball B ⊆ B(x₀, R). If σ M ≤ A, then on the concentric ball B' = B(x₀, R / (2√n)),

∫_{B'} exp (σ ‖f - f_{B'}‖) ≤ C |B'|.

TauCeti.exists_setLIntegral_exp_mul_norm_sub_setAverage_ball_le.{u_1, u_3} {ι : Type u_1}
  [Fintype ι] :
  ∃ A,
    0 < A ∧
      ∃ C,
        ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
          {μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [μ.IsAddHaarMeasure]
          {f : EuclideanSpace ℝ ι → E} {x₀ : EuclideanSpace ℝ ι} {R : ℝ} {M : NNReal} {σ : ℝ},
          MeasureTheory.IntegrableOn f (Metric.ball x₀ R) μ →
            (∀ (y : EuclideanSpace ℝ ι) (s : ℝ),
                Metric.ball y s ⊆ Metric.ball x₀ R →
                  ⨍⁻ (x : EuclideanSpace ℝ ι) in Metric.ball y s,
                      ‖f x - ⨍ (z : EuclideanSpace ℝ ι) in Metric.ball y s, f z ∂μ‖ₑ ∂μ ≤
                    ↑M) →
              σ * ↑M ≤ A →
                ∫⁻ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ (R / (2 * √↑(Fintype.card ι))),
                    ENNReal.ofReal
                      (Real.exp
                        (σ *
                          ‖f x -
                              ⨍ (y : EuclideanSpace ℝ ι) in
                                Metric.ball x₀ (R / (2 * √↑(Fintype.card ι))), f y ∂μ‖)) ∂μ ≤
                  ↑C * μ (Metric.ball x₀ (R / (2 * √↑(Fintype.card ι))))
Lean

Formalized in Tau Ceti as TauCeti.exists_setLIntegral_exp_mul_norm_sub_setAverage_ball_le.

Other forms

The John–Nirenberg inequality on a cube, for any additive Haar measure. Formalized in Tau Ceti as TauCeti.measure_lt_norm_sub_setAverage_closedBall_le.

TauCeti.measure_lt_norm_sub_setAverage_closedBall_le.{u_1, u_2} {ι : Type u_1} [Fintype ι]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {M : NNReal} {c : ι → ℝ}
  {r : ℝ} [CompleteSpace E] {μ : MeasureTheory.Measure (ι → ℝ)} [μ.IsAddHaarMeasure]
  (hf : MeasureTheory.IntegrableOn f (Metric.closedBall c r) μ)
  (hM :
    ∀ (y : ι → ℝ) (ρ : ℝ),
      Metric.closedBall y ρ ⊆ Metric.closedBall c r →
        ⨍⁻ (x : ι → ℝ) in Metric.closedBall y ρ,
            ‖f x - ⨍ (z : ι → ℝ) in Metric.closedBall y ρ, f z ∂μ‖ₑ ∂μ ≤
          ↑M)
  (s : ℝ) :
  μ {x | x ∈ Metric.closedBall c r ∧ s < ‖f x - ⨍ (y : ι → ℝ) in Metric.closedBall c r, f y ∂μ‖} ≤
    ENNReal.ofReal (2 * Real.exp (-(Real.log 2 * s / (2 ^ (Fintype.card ι + 1) * ↑M)))) *
      μ (Metric.closedBall c r)

The John–Nirenberg inequality on a dyadic cube, for any additive Haar measure. Formalized in Tau Ceti as TauCeti.measure_lt_norm_sub_setAverage_le.

TauCeti.measure_lt_norm_sub_setAverage_le.{u_1, u_2} {ι : Type u_1} [Fintype ι] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {q₀ : ℤ × (ι → ℤ)} {M : NNReal}
  [CompleteSpace E] {μ : MeasureTheory.Measure (ι → ℝ)} [μ.IsAddHaarMeasure]
  (hf : MeasureTheory.IntegrableOn f (TauCeti.dyadicCube q₀.1 q₀.2) μ)
  (hM :
    ∀ (q : ℤ × (ι → ℤ)),
      TauCeti.dyadicCube q.1 q.2 ⊆ TauCeti.dyadicCube q₀.1 q₀.2 →
        ⨍⁻ (x : ι → ℝ) in TauCeti.dyadicCube q.1 q.2,
            ‖f x - ⨍ (y : ι → ℝ) in TauCeti.dyadicCube q.1 q.2, f y ∂μ‖ₑ ∂μ ≤
          ↑M)
  (s : ℝ) :
  μ
      {x |
        x ∈ TauCeti.dyadicCube q₀.1 q₀.2 ∧
          s < ‖f x - ⨍ (y : ι → ℝ) in TauCeti.dyadicCube q₀.1 q₀.2, f y ∂μ‖} ≤
    ENNReal.ofReal (2 * Real.exp (-(Real.log 2 * s / (2 ^ (Fintype.card ι + 1) * ↑M)))) *
      μ (TauCeti.dyadicCube q₀.1 q₀.2)
Sources
LeanTauCeti.exists_setLIntegral_exp_mul_norm_sub_setAverage_ball_le · TauCeti.measure_lt_norm_sub_setAverage_closedBall_le · TauCeti.measure_lt_norm_sub_setAverage_le
Uses 1 · Used by 1
Proof usesLebesgue's differentiation theorem along dyadic cubes
Used byMoser's crossover estimate (TauCeti.exists_setLIntegral_exp_mul_mul_setLIntegral_exp_neg_mul_ball_le)

TheoremMinkowski's integral inequality#

For 1 ≤ p and a jointly a.e. measurable f : α → β → ℝ≥0∞, the Lᵖ(μ) seminorm of x ↦ ∫⁻ y, f x y ∂ν is at most the integral over ν of the Lᵖ(μ) seminorms of the functions x ↦ f x y: (∫⁻ x, (∫⁻ y, f x y ∂ν) ^ p ∂μ) ^ (1 / p) ≤ ∫⁻ y, (∫⁻ x, f x y ^ p ∂μ) ^ (1 / p) ∂ν.

TauCeti.lintegral_Lp_lintegral_le.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α]
  [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.SFinite ν] {f : α → β → ENNReal}
  (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) {p : ℝ} (hp : 1 ≤ p) :
  (∫⁻ (x : α), (∫⁻ (y : β), f x y ∂ν) ^ p ∂μ) ^ (1 / p) ≤
    ∫⁻ (y : β), (∫⁻ (x : α), f x y ^ p ∂μ) ^ (1 / p) ∂ν
Lean

Formalized in Tau Ceti as TauCeti.lintegral_Lp_lintegral_le.

Sources
LeanTauCeti.lintegral_Lp_lintegral_le
Used by 2
Used byThe sharp BV Sobolev bound · Lisini's superposition principle in a complete separable metric space

TheoremMoser's crossover estimate (TauCeti.exists_setLIntegral_exp_mul_mul_setLIntegral_exp_neg_mul_ball_le)#

There are constants A > 0 and C, depending only on the dimension n, such that the following holds for every additive Haar measure μ on ℝⁿ = EuclideanSpace ℝ ι. Let f : ℝⁿ → ℝ be integrable on the ball B(x₀, R), with mean oscillation ⨍_B |f - f_B| ≤ M on every ball B ⊆ B(x₀, R). If |σ| M ≤ A, then on the concentric ball B' = B(x₀, R / (2√n)),

(∫_{B'} exp (σ f)) (∫_{B'} exp (-σ f)) ≤ C |B'|².

For f = log u, with u positive, this compares the averages of u^σ and of u^(-σ) over B': it is the step of Moser's proof of the Harnack inequality that links the bounds for positive powers of a supersolution to those for its negative powers.

TauCeti.exists_setLIntegral_exp_mul_mul_setLIntegral_exp_neg_mul_ball_le.{u_1} {ι : Type u_1}
  [Fintype ι] :
  ∃ A,
    0 < A ∧
      ∃ C,
        ∀ {μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [μ.IsAddHaarMeasure]
          {f : EuclideanSpace ℝ ι → ℝ} {x₀ : EuclideanSpace ℝ ι} {R : ℝ} {M : NNReal} {σ : ℝ},
          MeasureTheory.IntegrableOn f (Metric.ball x₀ R) μ →
            (∀ (y : EuclideanSpace ℝ ι) (s : ℝ),
                Metric.ball y s ⊆ Metric.ball x₀ R →
                  ⨍⁻ (x : EuclideanSpace ℝ ι) in Metric.ball y s,
                      ‖f x - ⨍ (z : EuclideanSpace ℝ ι) in Metric.ball y s, f z ∂μ‖ₑ ∂μ ≤
                    ↑M) →
              |σ| * ↑M ≤ A →
                (∫⁻ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ (R / (2 * √↑(Fintype.card ι))),
                      ENNReal.ofReal (Real.exp (σ * f x)) ∂μ) *
                    ∫⁻ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ (R / (2 * √↑(Fintype.card ι))),
                      ENNReal.ofReal (Real.exp (-(σ * f x))) ∂μ ≤
                  ↑C * μ (Metric.ball x₀ (R / (2 * √↑(Fintype.card ι)))) ^ 2
Lean

Formalized in Tau Ceti as TauCeti.exists_setLIntegral_exp_mul_mul_setLIntegral_exp_neg_mul_ball_le.

Sources
LeanTauCeti.exists_setLIntegral_exp_mul_mul_setLIntegral_exp_neg_mul_ball_le
Uses 1 · Used by 1
Proof usesThe John–Nirenberg inequality on Euclidean balls
Used byMoser's crossover estimate (TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le)

TheoremRiesz–Markov–Kakutani on a compact Hausdorff space#

a linear functional on C(X, ℝ) that is nonnegative on nonnegative functions is integration against a regular measure.

LinearMap.exists_regular_integral_eq.{u_1} {X : Type u_1} [TopologicalSpace X] [CompactSpace X]
  [T2Space X] [MeasurableSpace X] [BorelSpace X] (L : C(X, ℝ) →ₗ[ℝ] ℝ)
  (hL : ∀ (h : C(X, ℝ)), 0 ≤ h → 0 ≤ L h) :
  ∃ μ, μ.Regular ∧ ∀ (h : C(X, ℝ)), ∫ (x : X), h x ∂μ = L h
Lean

Formalized in Tau Ceti as LinearMap.exists_regular_integral_eq.

Sources
LeanLinearMap.exists_regular_integral_eq
Used by 1
Used byPietsch domination theorem

TheoremThe Riesz–Thorin interpolation theorem#

Let T be a complex-linear map from simple functions on (α, μ) to almost-everywhere classes on a σ-finite (β, ν) with ‖T f‖_{q₀} ≤ M₀ ‖f‖_{p₀} and ‖T f‖_{q₁} ≤ M₁ ‖f‖_{p₁} for all simple f, where p₀, p₁ ∈ [0, ∞] and 1 ≤ q₀, q₁ ≤ ∞. For 0 < θ < 1 and the intermediate exponents 1 / p = (1 - θ) / p₀ + θ / p₁, 1 / q = (1 - θ) / q₀ + θ / q₁,

‖T f‖_q ≤ M₀ ^ (1 - θ) M₁ ^ θ ‖f‖_p

for every simple f. σ-finiteness of ν is only used when q = ∞; for q < ∞ see TauCeti.eLpNorm_le_rpow_mul_rpow_mul_eLpNorm_of_ne_top.

TauCeti.eLpNorm_le_rpow_mul_rpow_mul_eLpNorm.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite ν]
  {T : MeasureTheory.SimpleFunc α ℂ →ₗ[ℂ] β →ₘ[ν] ℂ} {p₀ p₁ p q₀ q₁ q : ENNReal} (hq₀ : 1 ≤ q₀)
  (hq₁ : 1 ≤ q₁) {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 1)
  (hp : p⁻¹ = ENNReal.ofReal (1 - θ) * p₀⁻¹ + ENNReal.ofReal θ * p₁⁻¹)
  (hq : q⁻¹ = ENNReal.ofReal (1 - θ) * q₀⁻¹ + ENNReal.ofReal θ * q₁⁻¹) {M₀ M₁ : NNReal}
  (h₀ :
    ∀ (f : MeasureTheory.SimpleFunc α ℂ),
      MeasureTheory.eLpNorm (↑(T f)) q₀ ν ≤ ↑M₀ * MeasureTheory.eLpNorm (⇑f) p₀ μ)
  (h₁ :
    ∀ (f : MeasureTheory.SimpleFunc α ℂ),
      MeasureTheory.eLpNorm (↑(T f)) q₁ ν ≤ ↑M₁ * MeasureTheory.eLpNorm (⇑f) p₁ μ)
  (f : MeasureTheory.SimpleFunc α ℂ) :
  MeasureTheory.eLpNorm (↑(T f)) q ν ≤ ↑(M₀ ^ (1 - θ) * M₁ ^ θ) * MeasureTheory.eLpNorm (⇑f) p μ
Lean

Formalized in Tau Ceti as TauCeti.eLpNorm_le_rpow_mul_rpow_mul_eLpNorm.

Other forms

The Riesz–Thorin interpolation theorem. Formalized in Tau Ceti as TauCeti.eLpNorm_le_rpow_mul_rpow_mul_eLpNorm_of_ne_top.

TauCeti.eLpNorm_le_rpow_mul_rpow_mul_eLpNorm_of_ne_top.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {T : MeasureTheory.SimpleFunc α ℂ →ₗ[ℂ] β →ₘ[ν] ℂ}
  {p₀ p₁ p q₀ q₁ q : ENNReal} (hq₀ : 1 ≤ q₀) (hq₁ : 1 ≤ q₁) {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 1)
  (hp : p⁻¹ = ENNReal.ofReal (1 - θ) * p₀⁻¹ + ENNReal.ofReal θ * p₁⁻¹)
  (hq : q⁻¹ = ENNReal.ofReal (1 - θ) * q₀⁻¹ + ENNReal.ofReal θ * q₁⁻¹) (hqtop : q ≠ ⊤)
  {M₀ M₁ : NNReal}
  (h₀ :
    ∀ (f : MeasureTheory.SimpleFunc α ℂ),
      MeasureTheory.eLpNorm (↑(T f)) q₀ ν ≤ ↑M₀ * MeasureTheory.eLpNorm (⇑f) p₀ μ)
  (h₁ :
    ∀ (f : MeasureTheory.SimpleFunc α ℂ),
      MeasureTheory.eLpNorm (↑(T f)) q₁ ν ≤ ↑M₁ * MeasureTheory.eLpNorm (⇑f) p₁ μ)
  (f : MeasureTheory.SimpleFunc α ℂ) :
  MeasureTheory.eLpNorm (↑(T f)) q ν ≤ ↑(M₀ ^ (1 - θ) * M₁ ^ θ) * MeasureTheory.eLpNorm (⇑f) p μ
Sources
LeanTauCeti.eLpNorm_le_rpow_mul_rpow_mul_eLpNorm · TauCeti.eLpNorm_le_rpow_mul_rpow_mul_eLpNorm_of_ne_top
Uses 1
Proof usesHölder's inequality for the integral of a product

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.