Radial Sobolev embedding

AbbreviationReal \(n\)-space with the Euclidean norm#✓fully proved

For a natural number \(n\), \(\mathbb{R}^n\) denotes the \(n\)-dimensional real Euclidean space: real \(n\)-tuples with the Euclidean inner product and norm.

abbrev Rn (n : ℕ) : Type := EuclideanSpace ℝ (Fin n)

Used by 3

Used byClosed unit ball of \(\mathbb{R}^n\) · Radial Sobolev embedding outside the unit ball · Radial functions on \(\mathbb{R}^n\)

DefinitionClosed unit ball of \(\mathbb{R}^n\)#✓fully proved

For a natural number \(n\), the closed unit ball of \(\mathbb{R}^n\) is the set \(\{x \in \mathbb{R}^n : \|x\| \le 1\}\), where \(\|\cdot\|\) is the Euclidean norm.

def ClosedUnitBall (n : ℕ) : Set (Rn n) := {x : Rn n | ‖x‖ ≤ 1}

Uses 1 · Used by 1

Statement usesReal \(n\)-space with the Euclidean norm

Used byRadial Sobolev embedding outside the unit ball

DefinitionRadial functions on \(\mathbb{R}^n\)#✓fully proved

A function \(f \colon \mathbb{R}^n \to \mathbb{R}\) is radial if \(f(x) = f(y)\) for all \(x, y \in \mathbb{R}^n\) with \(\|x\| = \|y\|\), where \(\|\cdot\|\) is the Euclidean norm.

def IsRadial {n : ℕ} (f : Rn n → ℝ) : Prop :=
  ∀ x y : Rn n, ‖x‖ = ‖y‖ → f x = f y

Uses 1 · Used by 1

Statement usesReal \(n\)-space with the Euclidean norm

Used byRadial Sobolev embedding outside the unit ball

TheoremRadial Sobolev embedding outside the unit ball#●ready to prove

Let \(n \ge 2\), let \(B\) be the closed unit ball of \(\mathbb{R}^n\), and let \(1 < p < 2\) and \(p \le q \le \infty\). Then there is a constant \(C > 0\) such that every radial function \(f \colon \mathbb{R}^n \to \mathbb{R}\) that has compact support, whose closed support is contained in \(\mathbb{R}^n \setminus B\), and which is \(C^\infty\) on \(\mathbb{R}^n \setminus B\), satisfies

\[\|f\|_{L^q} \le C \left( \|f\|_{L^p} + \big\| |Df| \big\|_{L^p} \right),\]

where the norms are taken with respect to Lebesgue measure and \(|Df(x)|\) is the operator norm of the derivative of \(f\) at \(x\).

Smoothness here means \(C^\infty\). The source's formal statement asked for real-analyticity instead, which makes the claim vacuous: an analytic, radial, compactly supported \(f\) vanishes outside the ball.

MathlibExt.Analysis.FunctionalAnalysis.RadialSobolevExteriorBallWanted.exists_eLpNorm_le_sobolev_of_radial_of_tsupport_subset_compl_closedBall · 17 lines

public theorem_wanted exists_eLpNorm_le_sobolev_of_radial_of_tsupport_subset_compl_closedBall
  (n : ℕ)
  (hn : 2 ≤ n)
  (p q : ENNReal)
  (hp1 : 1 < p)
  (hp2 : p < 2)
  (hpq : p ≤ q) :
  ∃ C : ℝ, 0 < C ∧
    ∀ f : Rn n → ℝ,
      ContDiffOn ℝ ∞ f ((ClosedUnitBall n)ᶜ) →
      HasCompactSupport f →
      tsupport f ⊆ (ClosedUnitBall n)ᶜ →
      IsRadial f →
      eLpNorm f q volume ≤
        ENNReal.ofReal C *
          (eLpNorm f p volume +
            eLpNorm (fun x : Rn n => ‖fderiv ℝ f x‖) p volume)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l2_80, with the change above.

Uses 3

Statement usesClosed unit ball of \(\mathbb{R}^n\) · Radial functions on \(\mathbb{R}^n\) · Real \(n\)-space with the Euclidean norm

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.