Weak limits of difference quotients

The H^k bootstrap of Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2 runs the interior H² estimate on a directional derivative ∂_ℓ u. In the graph encoding of EllipticPdes.Sobolev.Basic that derivative has to be produced as a limit of the discrete family Dₖ^h u, and the limit is taken weakly, so this file supplies the two weak-limit facts the bootstrap needs.

The first is weak sequential compactness of a bounded sequence in a separable real Hilbert space, which is the abstract form of EllipticPdes.Regularity.exists_weak_limit_of_bounded: the difference-quotient engine needs it on the ambient graph space H1amb Ω, not only on the whole-space EucL2 d where that theorem states it.

The second is weak L² convergence of the difference quotients themselves. The bound norm_diffQuot_le_of_hasWeakDeriv makes the family uniformly bounded, and against a smooth compactly supported test the discrete integration-by-parts identity together with the strong convergence Dₖ^{-h} φ → ∂ₖφ identifies the limit as the weak derivative; density of the smooth compactly supported classes then upgrades the test class to an arbitrary one.

Main declarations

• exists_weak_limit_of_bounded_hilbert: weak sequential compactness in a separable real Hilbert space.
• tendsto_inner_of_dense_of_bounded: a uniformly bounded sequence converging weakly against a dense set converges weakly against every vector.
• tendsto_inner_diffQuot_of_hasWeakDeriv: Dₖ^{hₘ} g ⇀ g' whenever g' is the weak k-derivative of g and hₘ → 0 through nonzero steps.

Weak sequential compactness in a separable real Hilbert space

theorem EllipticPdes.Regularity.exists_weak_limit_of_bounded_hilbert {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] {x : ℕ → E} {M : ℝ} (hx : ∀ (m : ℕ), ‖x m‖ ≤ M) : ∃ (g' : E) (σ : ℕ → ℕ), StrictMono σ ∧ ‖g'‖ ≤ M ∧ ∀ (y : E), Filter.Tendsto (fun (m : ℕ) => inner ℝ (x (σ m)) y) Filter.atTop (nhds (inner ℝ g' y))

Weak sequential compactness of bounded sequences. A sequence bounded by M in a separable real Hilbert space has a subsequence converging weakly to a limit g' with ‖g'‖ ≤ M. This is EllipticPdes.Regularity.exists_weak_limit_of_bounded with the whole-space L² substrate replaced by an abstract space, so that it also applies to the ambient graph space H1amb Ω. Assembled from the sequential Banach-Alaoglu theorem on the weak dual (WeakDual.isSeqCompact_closedBall), the Riesz self-duality of the Hilbert space (InnerProductSpace.toDual), and the closed-ball membership of the weak-* limit.

Upgrading weak convergence from a dense set

theorem EllipticPdes.Regularity.tendsto_inner_of_dense_of_bounded {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : ℕ → E} {L : E} {M : ℝ} (hX : ∀ (m : ℕ), ‖X m‖ ≤ M) (hL : ‖L‖ ≤ M) {S : Set E} (hS : Dense S) (hconv : ∀ z ∈ S, Filter.Tendsto (fun (m : ℕ) => inner ℝ (X m) z) Filter.atTop (nhds (inner ℝ L z))) (y : E) : Filter.Tendsto (fun (m : ℕ) => inner ℝ (X m) y) Filter.atTop (nhds (inner ℝ L y))

Density upgrade for weak convergence. A sequence bounded by M, whose weak limit candidate is also bounded by M, and which converges weakly against every vector of a dense set, converges weakly against every vector: split the pairing across a nearby dense vector and spend a third of the tolerance on each of the three pieces.

Weak convergence of the difference quotients

theorem EllipticPdes.Regularity.tendsto_inner_diffQuot_of_hasWeakDeriv {d : ℕ} (k : Fin d) {g g' : ↥(MeasureTheory.EucL2 d)} (hg : HasWeakDeriv k g g') {η : ℕ → ℝ} (hη0 : ∀ (m : ℕ), η m ≠ 0) (hηlim : Filter.Tendsto η Filter.atTop (nhds 0)) (y : ↥(MeasureTheory.EucL2 d)) : Filter.Tendsto (fun (m : ℕ) => inner ℝ ((diffQuot k (η m)) g) y) Filter.atTop (nhds (inner ℝ g' y))

Weak L² convergence of difference quotients (Evans §5.8.2). If g' is the weak k-derivative of g in L²(ℝᵈ) and the steps ηₘ → 0 are nonzero, then Dₖ^{ηₘ} g ⇀ g' weakly in L². Against a smooth compactly supported test the discrete integration-by-parts identity ⟪Dₖ^h g, φ⟫ = -⟪g, Dₖ^{-h} φ⟫ together with the strong convergence Dₖ^{-ηₘ} φ → ∂ₖφ gives the limit -⟪g, ∂ₖφ⟫ = ⟪g', φ⟫, and the uniform bound ‖Dₖ^h g‖ ≤ ‖g'‖ extends it to every test class by density.