Dense subspaces of Lp spaces

DefinitionVanishing cutoff factor#✓fully proved

For real numbers \(a\), \(b\), \(\delta\) and \(x\), the value at \(x\) of the vanishing cutoff factor with endpoints \(a\), \(b\) and width \(\delta\) is \(\max\bigl(0, \min\bigl(1, \min((x - a)/\delta, (b - x)/\delta)\bigr)\bigr)\), where division by \(0\) is read as \(0\).

It vanishes at \(a\) and at \(b\). For \(\delta > 0\) it equals \(1\) on \([a + \delta, b - \delta]\), an interval that is nonempty when \(2\delta \le b - a\). At \(\delta = 0\) it is identically zero.

noncomputable def vanishingCutoff (a b δ : ℝ) (x : ℝ) : ℝ :=
  Real.intervalCutoff a b δ x

Uses 1 · Used by 13

Statement usesInterval cutoff

Used byCutoff approximants · Continuity of the cutoff approximants · Cutoff approximants vanish at the left endpoint · Cutoff approximants vanish at the right endpoint · Cutoff approximants stay in \(L^p\) · Continuous functions vanishing at the endpoints are dense in \(L^p\) of a compact interval · Pointwise bound on the cutoff error · Continuity of the vanishing cutoff factor · The vanishing cutoff factor equals one on its plateau · The vanishing cutoff factor vanishes at the left endpoint · The vanishing cutoff factor vanishes at the right endpoint · The vanishing cutoff factor is at most one · The vanishing cutoff factor is nonnegative

TheoremThe vanishing cutoff factor is nonnegative#✓fully proved

For all real numbers \(a\), \(b\), \(\delta\) and \(x\), the value at \(x\) of the vanishing cutoff factor with endpoints \(a\), \(b\) and width \(\delta\) is at least \(0\).

theorem vanishingCutoff_nonneg (a b δ : ℝ) (x : ℝ) :
    0 ≤ vanishingCutoff a b δ x

Uses 2 · Used by 2

Statement usesVanishing cutoff factor

Proof usesThe interval cutoff is nonnegative

Used byCutoff approximants stay in \(L^p\) · Pointwise bound on the cutoff error

TheoremThe vanishing cutoff factor is at most one#✓fully proved

For all real numbers \(a\), \(b\), \(\delta\) and \(x\), the value at \(x\) of the vanishing cutoff factor with endpoints \(a\), \(b\) and width \(\delta\) is at most \(1\).

theorem vanishingCutoff_le_one (a b δ : ℝ) (x : ℝ) :
    vanishingCutoff a b δ x ≤ 1

Uses 2 · Used by 2

Statement usesVanishing cutoff factor

Proof usesThe interval cutoff is at most one

Used byCutoff approximants stay in \(L^p\) · Pointwise bound on the cutoff error

TheoremContinuity of the vanishing cutoff factor#✓fully proved

For all \(a, b, \delta \in \mathbb{R}\), the vanishing cutoff factor with endpoints \(a\), \(b\) and width \(\delta\) is a continuous function \(\mathbb{R} \to \mathbb{R}\).

theorem vanishingCutoff_continuous (a b δ : ℝ) :
    Continuous (vanishingCutoff a b δ)

Uses 2 · Used by 1

Statement usesVanishing cutoff factor

Proof usesContinuity of the interval cutoff

Used byContinuity of the cutoff approximants

TheoremThe vanishing cutoff factor vanishes at the left endpoint#✓fully proved

For all \(a, b, \delta \in \mathbb{R}\), the vanishing cutoff factor with endpoints \(a\), \(b\) and width \(\delta\) takes the value \(0\) at \(a\).

theorem vanishingCutoff_eq_zero_left (a b δ : ℝ) :
    vanishingCutoff a b δ a = 0

Uses 2 · Used by 1

Statement usesVanishing cutoff factor

Proof usesThe interval cutoff vanishes at the left endpoint

Used byCutoff approximants vanish at the left endpoint

TheoremThe vanishing cutoff factor vanishes at the right endpoint#✓fully proved

For all real numbers \(a\), \(b\) and \(\delta\), the vanishing cutoff factor with endpoints \(a\), \(b\) and width \(\delta\) takes the value \(0\) at \(b\).

theorem vanishingCutoff_eq_zero_right (a b δ : ℝ) :
    vanishingCutoff a b δ b = 0

Uses 2 · Used by 1

Statement usesVanishing cutoff factor

Proof usesThe interval cutoff vanishes at the right endpoint

Used byCutoff approximants vanish at the right endpoint

TheoremThe vanishing cutoff factor equals one on its plateau#✓fully proved

Let \(a, b \in \mathbb{R}\) and \(\delta > 0\). For every real \(x\) with \(a + \delta \le x \le b - \delta\), the vanishing cutoff factor with endpoints \(a\), \(b\) and width \(\delta\) takes the value \(1\) at \(x\).

theorem vanishingCutoff_eq_one (a b : ℝ) {δ : ℝ} (hδ : 0 < δ) {x : ℝ}
    (hx1 : a + δ ≤ x) (hx2 : x ≤ b - δ) :
    vanishingCutoff a b δ x = 1

Uses 2 · Used by 1

Statement usesVanishing cutoff factor

Proof usesThe interval cutoff equals one on its plateau

Used byContinuous functions vanishing at the endpoints are dense in \(L^p\) of a compact interval

DefinitionCutoff approximants#✓fully proved

Let \(a, b \in \mathbb{R}\), let \(E\) be a real normed space, let \(g_0 : \mathbb{R} \to E\) and \(n \in \mathbb{N}\), and put \(\delta_n = (b - a)/(n + 1)\). The \(n\)-th cutoff approximant of \(g_0\) with endpoints \(a\) and \(b\) is the function \(x \mapsto \varphi(x)\, g_0(x)\), where \(\varphi\) is the vanishing cutoff factor with endpoints \(a\), \(b\) and width \(\delta_n\).

noncomputable def cutoffApprox (a b : ℝ) (g₀ : ℝ → E) (n : ℕ) (x : ℝ) : E :=
  vanishingCutoff a b ((b - a) / ((n + 1 : ℕ) : ℝ)) x • g₀ x

Uses 1 · Used by 6

Statement usesVanishing cutoff factor

Used byContinuity of the cutoff approximants · Cutoff approximants vanish at the left endpoint · Cutoff approximants vanish at the right endpoint · Cutoff approximants stay in \(L^p\) · Continuous functions vanishing at the endpoints are dense in \(L^p\) of a compact interval · Pointwise bound on the cutoff error

TheoremContinuity of the cutoff approximants#✓fully proved

Let \(a, b \in \mathbb{R}\), let \(E\) be a real normed space and let \(g_0 : \mathbb{R} \to E\) be continuous. Then for every \(n \in \mathbb{N}\) the \(n\)-th cutoff approximant of \(g_0\) with endpoints \(a\) and \(b\) is continuous.

theorem cutoffApprox_continuous (a b : ℝ) (g₀ : ℝ → E) (hg₀ : Continuous g₀)
    (n : ℕ) : Continuous (cutoffApprox a b g₀ n)

Uses 3 · Used by 2

Statement usesCutoff approximants

Proof usesVanishing cutoff factor · Continuity of the vanishing cutoff factor

Used byCutoff approximants stay in \(L^p\) · Continuous functions vanishing at the endpoints are dense in \(L^p\) of a compact interval

TheoremCutoff approximants vanish at the left endpoint#✓fully proved

Let \(a, b \in \mathbb{R}\), let \(E\) be a real normed space and let \(g_0 : \mathbb{R} \to E\) be any function. For every \(n \in \mathbb{N}\), the \(n\)-th cutoff approximant of \(g_0\) with endpoints \(a\) and \(b\) takes the value \(0\) at \(a\).

theorem cutoffApprox_eq_zero_left (a b : ℝ) (g₀ : ℝ → E) (n : ℕ) :
    cutoffApprox a b g₀ n a = 0

Uses 3 · Used by 1

Statement usesCutoff approximants

Proof usesVanishing cutoff factor · The vanishing cutoff factor vanishes at the left endpoint

Used byContinuous functions vanishing at the endpoints are dense in \(L^p\) of a compact interval

TheoremCutoff approximants vanish at the right endpoint#✓fully proved

Let \(a, b \in \mathbb{R}\), let \(E\) be a real normed space and let \(g_0 : \mathbb{R} \to E\) be any function. For every \(n \in \mathbb{N}\), the \(n\)-th cutoff approximant of \(g_0\) with endpoints \(a\) and \(b\) takes the value \(0\) at \(b\).

theorem cutoffApprox_eq_zero_right (a b : ℝ) (g₀ : ℝ → E) (n : ℕ) :
    cutoffApprox a b g₀ n b = 0

Uses 3 · Used by 1

Statement usesCutoff approximants

Proof usesVanishing cutoff factor · The vanishing cutoff factor vanishes at the right endpoint

Used byContinuous functions vanishing at the endpoints are dense in \(L^p\) of a compact interval

TheoremCutoff approximants stay in \(L^p\)#✓fully proved

Let \(E\) be a real normed space, let \(\mu\) be a measure on \(\mathbb{R}\), let \(p \in [0, \infty]\), and let \(g_0 : \mathbb{R} \to E\) be continuous with \(g_0 \in L^p(\mu)\). Then for all \(a, b \in \mathbb{R}\) and \(n \in \mathbb{N}\), the \(n\)-th cutoff approximant of \(g_0\) with endpoints \(a\) and \(b\) lies in \(L^p(\mu)\).

The approximant is pointwise dominated by \(\|g_0\|\), since the cutoff factor takes values in \([0, 1]\).

theorem cutoffApprox_memLp {p : ℝ≥0∞} {μ : Measure ℝ} {g₀ : ℝ → E}
    (hg₀ : MemLp g₀ p μ) (hg₀cont : Continuous g₀) (a b : ℝ)
    (n : ℕ) : MemLp (cutoffApprox a b g₀ n) p μ

Uses 5 · Used by 1

Statement usesCutoff approximants

Proof usesContinuity of the cutoff approximants · Vanishing cutoff factor · The vanishing cutoff factor is at most one · The vanishing cutoff factor is nonnegative

Used byContinuous functions vanishing at the endpoints are dense in \(L^p\) of a compact interval

TheoremPointwise bound on the cutoff error#✓fully proved

Let \(a, b \in \mathbb{R}\), let \(E\) be a real normed space and let \(g_0 : \mathbb{R} \to E\). If \(g_n\) denotes the \(n\)-th cutoff approximant of \(g_0\) with endpoints \(a\) and \(b\), then \(\|g_0(x) - g_n(x)\| \le \|g_0(x)\|\) for every \(n \in \mathbb{N}\) and every \(x \in \mathbb{R}\).

theorem norm_sub_cutoffApprox_le (a b : ℝ) (g₀ : ℝ → E) (n : ℕ) (x : ℝ) :
    ‖g₀ x - cutoffApprox a b g₀ n x‖ ≤ ‖g₀ x‖

Uses 4 · Used by 1

Statement usesCutoff approximants

Proof usesVanishing cutoff factor · The vanishing cutoff factor is at most one · The vanishing cutoff factor is nonnegative

Used byContinuous functions vanishing at the endpoints are dense in \(L^p\) of a compact interval

TheoremContinuous functions vanishing at the endpoints are dense in \(L^p\) of a compact interval#✓fully proved

Let \(a < b\) be real numbers, let \(1 \le p < \infty\) and let \(E\) be a real normed space. Write \(L^p([a, b])\) for \(L^p\) with respect to Lebesgue measure restricted to \([a, b]\). For every \(f : \mathbb{R} \to E\) in \(L^p([a, b])\) and every \(\varepsilon \in (0, \infty]\), there is a continuous \(g : \mathbb{R} \to E\) with \(g(a) = g(b) = 0\), \(g \in L^p([a, b])\) and \(\|f - g\|_{L^p([a, b])} < \varepsilon\).

theorem exists_continuous_vanishing_endpoints_eLpNorm_sub_lt
    (a b : ℝ) (hab : a < b) {p : ℝ≥0∞} (hp1 : 1 ≤ p) (hp_top : p ≠ ⊤)
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : ℝ → E} (hf : MemLp f p (volume.restrict (Set.Icc a b)))
    {ε : ℝ≥0∞} (hε : 0 < ε) :
    ∃ g : ℝ → E, Continuous g ∧ g a = 0 ∧ g b = 0 ∧
      MemLp g p (volume.restrict (Set.Icc a b)) ∧
      eLpNorm (f - g) p (volume.restrict (Set.Icc a b)) < ε

Uses 8

Proof usesCutoff approximants · Continuity of the cutoff approximants · Cutoff approximants vanish at the left endpoint · Cutoff approximants vanish at the right endpoint · Cutoff approximants stay in \(L^p\) · Pointwise bound on the cutoff error · Vanishing cutoff factor · The vanishing cutoff factor equals one on its plateau

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.