Infinite dimensionality of H₀¹ of the unit ball

EllipticPdes.Sobolev.exists_eigen_family recurses on a vector of nonzero L² class orthogonal to the family built so far, which is the infinite dimensionality of H₀¹(Ω). This file discharges it on the unit ball.

n bumps sit at the points ((2k+1)/(2n) - 1/2)eᵢ of the first coordinate axis, each supported in the ball of radius 1/(2n) about its centre. The centres are 1/n apart, so the supports are disjoint, and each closed support sits inside the unit ball since 1/2 + 1/(2n) < 1. Disjoint supports make the L² classes orthogonal, and each is nonzero because a bump is one at its centre.

Given m vectors, take m + 1 of these bumps. A linear map from an (m+1)-dimensional space to an m-dimensional one has a nonzero kernel, so some combination of the bumps is L²-orthogonal to all m vectors, and orthogonality of the bumps makes that combination nonzero.

Main declarations

• EllipticPdes.Sobolev.ballBump: a bump at a centre, with its support a ball of given radius.
• EllipticPdes.Sobolev.orth_family_nonempty_ball: the hypothesis of exists_eigen_family.
• EllipticPdes.Sobolev.dirichlet_eigen_family_ball: the Dirichlet eigenvalue sequence of the unit ball, with 2 < d the only hypothesis.
• EllipticPdes.Sobolev.dirichlet_eigenvalue_pos_ball: every weak Dirichlet eigenvalue of the unit ball is positive.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §6.5.1, Theorem 1.

A bump at a centre

noncomputable def EllipticPdes.Sobolev.ballBump {d : ℕ} (c : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : ContDiffBump c

A bump at c, one on closedBall c (r/2) and supported in closedBall c r.

Equations

• EllipticPdes.Sobolev.ballBump c hr = { rIn := r / 2, rOut := r, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

theorem EllipticPdes.Sobolev.tsupport_ballBump {d : ℕ} (c : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : tsupport ↑(ballBump c hr) = Metric.closedBall c r

theorem EllipticPdes.Sobolev.support_ballBump {d : ℕ} (c : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : Function.support ↑(ballBump c hr) = Metric.ball c r

theorem EllipticPdes.Sobolev.ballBump_centre {d : ℕ} (c : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : ↑(ballBump c hr) c = 1

theorem EllipticPdes.Sobolev.isTestFn_ballBump {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (c : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) (hsub : Metric.closedBall c r ⊆ Ω) : IsTestFn Ω ↑(ballBump c hr)

theorem EllipticPdes.Sobolev.eLpNorm_ballBump_ne_zero {d : ℕ} (c : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) {p : ENNReal} (hp0 : p ≠ 0) : MeasureTheory.eLpNorm (↑(ballBump c hr)) p MeasureTheory.volume ≠ 0

A bump has positive Lᵖ seminorm, being continuous and one at its centre.

The centres

noncomputable def EllipticPdes.Sobolev.bumpCoord (n : ℕ) (k : Fin n) : ℝ

The coordinate of the k-th centre: n points spaced 1/n apart inside (-1/2, 1/2).

Equations

• EllipticPdes.Sobolev.bumpCoord n k = (2 * ↑↑k + 1) / (2 * ↑n) - 1 / 2

noncomputable def EllipticPdes.Sobolev.bumpRadius (n : ℕ) : ℝ

The common radius: half the spacing, so the balls are disjoint.

Equations

• EllipticPdes.Sobolev.bumpRadius n = 1 / (2 * ↑n)

noncomputable def EllipticPdes.Sobolev.bumpCentre {d : ℕ} (i : Fin d) (n : ℕ) (k : Fin n) : EuclideanSpace ℝ (Fin d)

The k-th centre, on the i-th coordinate axis.

Equations

• EllipticPdes.Sobolev.bumpCentre i n k = PiLp.single 2 i (EllipticPdes.Sobolev.bumpCoord n k)

theorem EllipticPdes.Sobolev.bumpRadius_pos {n : ℕ} (hn : 0 < n) : 0 < bumpRadius n

theorem EllipticPdes.Sobolev.bumpRadius_le {n : ℕ} (hn : 0 < n) : bumpRadius n ≤ 1 / 2

theorem EllipticPdes.Sobolev.bumpCoord_abs_lt {n : ℕ} (k : Fin n) : |bumpCoord n k| < 1 / 2

theorem EllipticPdes.Sobolev.bumpCoord_sub {n : ℕ} (j k : Fin n) : bumpCoord n j - bumpCoord n k = (↑↑j - ↑↑k) / ↑n

theorem EllipticPdes.Sobolev.one_le_abs_sub_of_ne {j k : ℕ} (h : j ≠ k) : 1 ≤ |↑j - ↑k|

theorem EllipticPdes.Sobolev.bumpCoord_dist {n : ℕ} {j k : Fin n} (h : j ≠ k) : 1 / ↑n ≤ |bumpCoord n j - bumpCoord n k|

theorem EllipticPdes.Sobolev.dist_bumpCentre {d : ℕ} (i : Fin d) {n : ℕ} {j k : Fin n} (h : j ≠ k) : 1 / ↑n ≤ dist (bumpCentre i n j) (bumpCentre i n k)

theorem EllipticPdes.Sobolev.closedBall_bumpCentre_subset {d : ℕ} (i : Fin d) {n : ℕ} (k : Fin n) : Metric.closedBall (bumpCentre i n k) (bumpRadius n) ⊆ Metric.ball 0 1

theorem EllipticPdes.Sobolev.disjoint_support_ballBump {d : ℕ} (i : Fin d) {n : ℕ} {j k : Fin n} (h : j ≠ k) (x : EuclideanSpace ℝ (Fin d)) (hj : ↑(ballBump (bumpCentre i n j) ⋯) x ≠ 0) (hk : ↑(ballBump (bumpCentre i n k) ⋯) x ≠ 0) : False

The family in H₀¹ of the unit ball

noncomputable def EllipticPdes.Sobolev.bumpFn {d : ℕ} (i : Fin d) (n : ℕ) (k : Fin n) : EuclideanSpace ℝ (Fin d) → ℝ

The k-th bump of a family of n, as a function.

Equations

• EllipticPdes.Sobolev.bumpFn i n k = ↑(EllipticPdes.Sobolev.ballBump (EllipticPdes.Sobolev.bumpCentre i n k) ⋯)

theorem EllipticPdes.Sobolev.isTestFn_bumpFn {d : ℕ} (i : Fin d) {n : ℕ} (k : Fin n) : IsTestFn (Metric.ball 0 1) (bumpFn i n k)

theorem EllipticPdes.Sobolev.bumpFn_eq_zero_or {d : ℕ} (i : Fin d) {n : ℕ} {j k : Fin n} (h : j ≠ k) (x : EuclideanSpace ℝ (Fin d)) : bumpFn i n j x = 0 ∨ bumpFn i n k x = 0

Two bumps of the family never both survive at a point.

noncomputable def EllipticPdes.Sobolev.bumpElt {d : ℕ} (i : Fin d) (n : ℕ) (k : Fin n) : ↥(H01 (Metric.ball 0 1))

The k-th bump, as an element of H₀¹ of the unit ball.

Equations

• EllipticPdes.Sobolev.bumpElt i n k = ⟨⋯.testGraph, ⋯⟩

theorem EllipticPdes.Sobolev.coeFn_embL2_bumpElt {d : ℕ} (i : Fin d) {n : ℕ} (k : Fin n) : ↑↑((embL2 (Metric.ball 0 1)) (bumpElt i n k)) =ᵐ[MeasureTheory.volume.restrict (Metric.ball 0 1)] bumpFn i n k

theorem EllipticPdes.Sobolev.inner_embL2_bumpElt {d : ℕ} (i : Fin d) {n : ℕ} {j k : Fin n} (h : j ≠ k) : inner ℝ ((embL2 (Metric.ball 0 1)) (bumpElt i n j)) ((embL2 (Metric.ball 0 1)) (bumpElt i n k)) = 0

Disjoint supports make the classes orthogonal.

theorem EllipticPdes.Sobolev.embL2_bumpElt_ne_zero {d : ℕ} (i : Fin d) {n : ℕ} (k : Fin n) : (embL2 (Metric.ball 0 1)) (bumpElt i n k) ≠ 0

Each class is nonzero, the bump being one at its centre.

The hypothesis of the eigenvalue recursion

theorem EllipticPdes.Sobolev.orth_family_nonempty_ball {d : ℕ} (hd : 2 < d) (m : ℕ) (v : Fin m → ↥(H01 (Metric.ball 0 1))) : ∃ U ∈ orthSubmodule v, (embL2 (Metric.ball 0 1)) U ≠ 0

H₀¹ of the unit ball is infinite dimensional, in the form the eigenvalue recursion asks for: given m vectors there is one of nonzero L² class orthogonal to them all. Take m + 1 bumps with disjoint supports; a linear map from an (m+1)-dimensional space to an m-dimensional one has a nonzero kernel, and the combination it names is nonzero because the bumps are orthogonal.

theorem EllipticPdes.Sobolev.dirichlet_eigen_family_ball {d : ℕ} (hd : 2 < d) (n : ℕ) : ∃ (w : Fin n → ↥(H01 (Metric.ball 0 1))) (lam : Fin n → ℝ), (∀ (i : Fin n), ‖(embL2 (Metric.ball 0 1)) (w i)‖ = 1) ∧ (∀ (i j : Fin n), i ≠ j → inner ℝ ((embL2 (Metric.ball 0 1)) (w i)) ((embL2 (Metric.ball 0 1)) (w j)) = 0) ∧ (∀ (i : Fin n), 0 < lam i) ∧ (∀ (i j : Fin n), i ≤ j → lam i ≤ lam j) ∧ ∀ (i : Fin n) (V : ↥(H01 (Metric.ball 0 1))), ((laplaceBilin (Metric.ball 0 1)) (w i)) V = lam i * inner ℝ ((embL2 (Metric.ball 0 1)) (w i)) ((embL2 (Metric.ball 0 1)) V)

Dirichlet eigenvalue sequence of the unit ball, with 2 < d the only hypothesis: for every n an L²-orthonormal family of n weak solutions of -Δw = λw with 0 < λ₁ ≤ ⋯ ≤ λₙ. Every side condition of the chapter is discharged here, boundedness by the ball itself and the infinite dimensionality by orth_family_nonempty_ball.

theorem EllipticPdes.Sobolev.dirichlet_eigenvalue_pos_ball {d : ℕ} (hd : 2 < d) {lam : ℝ} {U : ↥(H01 (Metric.ball 0 1))} (hU : U ≠ 0) (heig : ∀ (V : ↥(H01 (Metric.ball 0 1))), ((laplaceBilin (Metric.ball 0 1)) U) V = lam * inner ℝ ((embL2 (Metric.ball 0 1)) U) ((embL2 (Metric.ball 0 1)) V)) : 0 < lam

Every weak Dirichlet eigenvalue of the unit ball is positive, with 2 < d the only hypothesis beyond the eigenpair.