Weighted Hardy–Sobolev inequalities on an annulus

AbbreviationEuclidean plane#✓fully proved

The Euclidean plane.

abbrev R2 : Type := EuclideanSpace ℝ (Fin 2)
Used by 5
Used byOpen discs about the origin for the annulus Hardy inequality · Weighted Hardy inequality on the annulus · Full annulus of the weighted Hardy inequality · Outer annulus of the weighted Hardy inequality · Weight of the annulus Hardy inequality

AbbreviationOpen discs about the origin for the annulus Hardy inequality#✓fully proved

For a real number \(r\), \(B_r = \{x \in \mathbb{R}^2 : |x| < r\}\) is the open disc of radius \(r\) about the origin of the Euclidean plane \(\mathbb{R}^2\), where \(|x|\) is the Euclidean norm.

abbrev B (r : ℝ) : Set R2 := Metric.ball (0 : R2) r
Uses 1 · Used by 2
Statement usesEuclidean plane
Used byFull annulus of the weighted Hardy inequality · Outer annulus of the weighted Hardy inequality

AbbreviationFull annulus of the weighted Hardy inequality#✓fully proved

\(\Omega_1 = B_3 \setminus \overline{B}_1\), where \(B_r\) is the open disc of radius \(r\) about the origin of the Euclidean plane \(\mathbb{R}^2\) and \(\overline{B}_1\) is the closure of \(B_1\); that is, writing \(|x|\) for the Euclidean norm, \(\Omega_1\) is the annulus \(\{x \in \mathbb{R}^2 : 1 < |x| < 3\}\).

abbrev Omega1 : Set R2 := B 3 \ closure (B 1)
Uses 2 · Used by 1
Statement usesOpen discs about the origin for the annulus Hardy inequality · Euclidean plane
Used byWeighted Hardy inequality on the annulus

AbbreviationOuter annulus of the weighted Hardy inequality#✓fully proved

\(\Omega_2 = B_3 \setminus \overline{B}_2\), where \(B_r\) is the open disc of radius \(r\) about the origin of the Euclidean plane \(\mathbb{R}^2\) and \(\overline{B}_2\) is the closure of \(B_2\); that is, writing \(|x|\) for the Euclidean norm, \(\Omega_2\) is the annulus \(\{x \in \mathbb{R}^2 : 2 < |x| < 3\}\).

abbrev Omega2 : Set R2 := B 3 \ closure (B 2)
Uses 2 · Used by 1
Statement usesOpen discs about the origin for the annulus Hardy inequality · Euclidean plane
Used byWeighted Hardy inequality on the annulus

DefinitionWeight of the annulus Hardy inequality#✓fully proved

For \(x\) in the Euclidean plane \(\mathbb{R}^2\), \(\phi(x) = \max\{|x| - 1, 0\}\), where \(|x|\) is the Euclidean norm; this is the distance from \(x\) to the closed unit disc.

noncomputable def phi (x : R2) : ℝ := max (‖x‖ - 1) 0
Uses 1 · Used by 1
Statement usesEuclidean plane
Used byWeighted Hardy inequality on the annulus

TheoremWeighted Hardy inequality on the annulus#●ready to prove

For \(r > 0\) let \(B_r\) be the open disc of radius \(r\) about the origin of \(\mathbb{R}^2\), let \(|x|\) be the Euclidean norm, and let \(\phi(x) = \max\{|x| - 1, 0\}\) be the distance from \(x\) to the closed unit disc. Let \(\Omega_1 = B_3 \setminus \overline{B}_1\) and \(\Omega_2 = B_3 \setminus \overline{B}_2\), with Lebesgue measure. For every real number \(p \ge 1\) there is a constant \(C > 0\) such that every function \(u \colon \mathbb{R}^2 \to \mathbb{R}\) that is continuously differentiable on \(\Omega_1\), and for which \(\|\phi \, |\nabla u|\|_{L^p(\Omega_1)}\) and \(\|u\|_{L^p(\Omega_2)}\) are finite, satisfies

\[\|u\|_{L^p(\Omega_1)} \le C \|\phi \, |\nabla u|\|_{L^p(\Omega_1)} + C \|u\|_{L^p(\Omega_2)}.\]
public theorem_wanted exists_eLpNorm_le_weighted_grad_add_outer_annulus
  (p : ℝ)
  (hp : 1 ≤ p) :
  ∃ C : ℝ, 0 < C ∧
    ∀ u : R2 → ℝ,
      ContDiffOn ℝ 1 u Omega1 →
      eLpNorm (fun x : R2 => phi x * ‖fderivWithin ℝ u Omega1 x‖)
          (ENNReal.ofReal p) (volume.restrict Omega1) ≠ ⊤ →
      eLpNorm u (ENNReal.ofReal p) (volume.restrict Omega2) ≠ ⊤ →
      eLpNorm u (ENNReal.ofReal p) (volume.restrict Omega1) ≤
        ENNReal.ofReal C *
            eLpNorm (fun x : R2 => phi x * ‖fderivWithin ℝ u Omega1 x‖)
              (ENNReal.ofReal p) (volume.restrict Omega1) +
          ENNReal.ofReal C * eLpNorm u (ENNReal.ofReal p) (volume.restrict Omega2)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l2_77.
Uses 4
Statement usesFull annulus of the weighted Hardy inequality · Outer annulus of the weighted Hardy inequality · Euclidean plane · Weight of the annulus Hardy inequality

AbbreviationThe plane of the critical weighted Sobolev inequality#✓fully proved

\(\mathbb{R}^2\) denotes the Euclidean plane, the space of pairs of real numbers with the Euclidean norm.

abbrev R2 : Type := EuclideanSpace ℝ (Fin 2)
Used by 5
Used byDiscs about the origin for the critical weighted Sobolev inequality · Critical weighted Sobolev inequality on an annulus · The annulus of the critical weighted Sobolev inequality · The outer annulus of the critical weighted Sobolev inequality · The weight of the critical weighted Sobolev inequality

AbbreviationDiscs about the origin for the critical weighted Sobolev inequality#✓fully proved

For a real number \(r\), \(B_r\) is the open disc \(\{x \in \mathbb{R}^2 : |x| < r\}\) of radius \(r\) about the origin of the Euclidean plane \(\mathbb{R}^2\).

abbrev B (r : ℝ) : Set R2 := Metric.ball (0 : R2) r
Uses 1 · Used by 2
Statement usesThe plane of the critical weighted Sobolev inequality
Used byThe annulus of the critical weighted Sobolev inequality · The outer annulus of the critical weighted Sobolev inequality

AbbreviationThe annulus of the critical weighted Sobolev inequality#✓fully proved

Let \(B_r\) denote the open disc of radius \(r\) about the origin of the Euclidean plane \(\mathbb{R}^2\). The annulus \(\Omega_1\) is \(B_3 \setminus \overline{B}_1\), the set of points of \(B_3\) outside the closure of \(B_1\), that is, \(\Omega_1 = \{x \in \mathbb{R}^2 : 1 < |x| < 3\}\).

abbrev Omega1 : Set R2 := B 3 \ closure (B 1)
Uses 2 · Used by 1
Statement usesDiscs about the origin for the critical weighted Sobolev inequality · The plane of the critical weighted Sobolev inequality
Used byCritical weighted Sobolev inequality on an annulus

AbbreviationThe outer annulus of the critical weighted Sobolev inequality#✓fully proved

Let \(B_r\) denote the open disc of radius \(r\) about the origin of the Euclidean plane \(\mathbb{R}^2\). The outer annulus \(\Omega_2\) is \(B_3 \setminus \overline{B}_2\), the set of points of \(B_3\) outside the closure of \(B_2\), that is, \(\Omega_2 = \{x \in \mathbb{R}^2 : 2 < |x| < 3\}\).

abbrev Omega2 : Set R2 := B 3 \ closure (B 2)
Uses 2 · Used by 1
Statement usesDiscs about the origin for the critical weighted Sobolev inequality · The plane of the critical weighted Sobolev inequality
Used byCritical weighted Sobolev inequality on an annulus

DefinitionThe weight of the critical weighted Sobolev inequality#✓fully proved

For \(x\) in the Euclidean plane \(\mathbb{R}^2\), the weight is \(\phi(x) = \max\{|x| - 1, 0\}\), the distance from \(x\) to the closed unit disc.

noncomputable def phi (x : R2) : ℝ := max (‖x‖ - 1) 0
Uses 1 · Used by 1
Statement usesThe plane of the critical weighted Sobolev inequality
Used byCritical weighted Sobolev inequality on an annulus

DefinitionSobolev conjugate exponent in dimension two#✓fully proved

For a real number \(p\), the Sobolev conjugate exponent is \(p^* = 2p/(2 - p)\) (at \(p = 2\), where the denominator vanishes, this is \(0\) by the convention that division by zero gives zero).

noncomputable def pStar (p : ℝ) : ℝ := 2 * p / (2 - p)
Used by 1
Used byCritical weighted Sobolev inequality on an annulus

TheoremCritical weighted Sobolev inequality on an annulus#●ready to prove

For \(r > 0\) let \(B_r\) be the open disc of radius \(r\) about the origin in the Euclidean plane \(\mathbb{R}^2\), let \(\Omega_1 = B_3 \setminus \overline{B}_1\) and \(\Omega_2 = B_3 \setminus \overline{B}_2\), and let \(\phi(x) = \max\{|x| - 1, 0\}\), the distance from \(x\) to the closed unit disc. Let \(1 \le p < 2\) and \(p^* = 2p/(2-p)\). Then there is a real number \(C > 0\) such that every function \(u \colon \mathbb{R}^2 \to \mathbb{R}\) that is continuously differentiable on \(\Omega_1\) and for which \(\|\phi \nabla u\|_{L^p(\Omega_1)}\) and \(\|u\|_{L^p(\Omega_2)}\) are finite satisfies

\[\|\phi u\|_{L^{p^*}(\Omega_1)} \le C\|\phi \nabla u\|_{L^p(\Omega_1)} + C\|u\|_{L^p(\Omega_2)}.\]

Here the norms are taken with respect to Lebesgue measure, \(\|\phi \nabla u\|_{L^p(\Omega_1)}\) is the \(L^p(\Omega_1)\) norm of \(x \mapsto \phi(x)\,|\nabla u(x)|\), and \(\nabla u(x)\) is the derivative of \(u\) at \(x\) within \(\Omega_1\).

MathlibExt.Analysis.FunctionalAnalysis.AnnulusWeightedSobolevCriticalWanted.exists_eLpNorm_phi_mul_le_weighted_grad_add_outer_annulus · 16 lines 
public theorem_wanted exists_eLpNorm_phi_mul_le_weighted_grad_add_outer_annulus
  (p : ℝ)
  (hp₁ : 1 ≤ p)
  (hp₂ : p < 2) :
  ∃ C : ℝ, 0 < C ∧
    ∀ u : R2 → ℝ,
      ContDiffOn ℝ 1 u Omega1 →
      eLpNorm (fun x : R2 => phi x * ‖fderivWithin ℝ u Omega1 x‖)
          (ENNReal.ofReal p) (volume.restrict Omega1) ≠ ⊤ →
      eLpNorm u (ENNReal.ofReal p) (volume.restrict Omega2) ≠ ⊤ →
      eLpNorm (fun x : R2 => phi x * u x) (ENNReal.ofReal (pStar p))
          (volume.restrict Omega1) ≤
        ENNReal.ofReal C *
            eLpNorm (fun x : R2 => phi x * ‖fderivWithin ℝ u Omega1 x‖)
              (ENNReal.ofReal p) (volume.restrict Omega1) +
          ENNReal.ofReal C * eLpNorm u (ENNReal.ofReal p) (volume.restrict Omega2)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l2_65.
Uses 5
Statement usesThe annulus of the critical weighted Sobolev inequality · The outer annulus of the critical weighted Sobolev inequality · The plane of the critical weighted Sobolev inequality · Sobolev conjugate exponent in dimension two · The weight of the critical weighted Sobolev inequality
11 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.