Weak path compactness for Galerkin approximations

The pointwise Hilbert-space extraction in Compactness does not by itself produce one subsequence converging at every time. This file packages the path-space step: a uniformly bounded, weakly equicontinuous sequence of continuous Hilbert-valued paths has a subsequence converging pointwise weakly on the whole compact time interval. A common initial trace and the uniform norm bound pass to that limit.

For a Galerkin sequence, the equation is responsible for the weak equicontinuity premise. The constructor for that modulus is kept separate from this compactness theorem.

@[reducible, inline]

abbrev AVenhance.Infra.Parabolic.FourierGalerkin.PathCompactness.TimeInterval : Set ℝ

Closed unit time interval for the Galerkin path compactness argument.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.PathCompactness.TimeInterval = Set.Icc 0 1

theorem AVenhance.Infra.Parabolic.FourierGalerkin.weakDualTopologicalAddGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsTopologicalAddGroup (WeakDual ℝ E)

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.weakDualUniformSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : UniformSpace (WeakDual ℝ E)

Translation-invariant uniform structure on the weak dual.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.weakDualUniformSpace = IsTopologicalAddGroup.rightUniformSpace (WeakDual ℝ E)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.weakDualUniformAddGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsUniformAddGroup (WeakDual ℝ E)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.hilbertToWeakDual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : WeakDual ℝ E

The Hilbert Riesz map, viewed with the weak-dual topology.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.hilbertToWeakDual x = StrongDual.toWeakDual ((InnerProductSpace.toDualMap ℝ E) x)

@[simp]

theorem AVenhance.Infra.Parabolic.FourierGalerkin.hilbertToWeakDual_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x v : E) : (hilbertToWeakDual x) v = inner ℝ x v

theorem AVenhance.Infra.Parabolic.FourierGalerkin.PathCompactness.exists_finite_test_modulus {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {uSeq : ℕ → ↑TimeInterval → E} (hmod : ∀ (v : E), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ) (t s : ↑TimeInterval), |inner ℝ (uSeq n t) v - inner ℝ (uSeq n s) v| ≤ C * √(dist t s)) (s : Finset E) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (t₀ t : ↑TimeInterval) (n : ℕ), dist t t₀ < δ → (s.sup (WeakDual.seminormFamily ℝ E)) (hilbertToWeakDual (uSeq n t) - hilbertToWeakDual (uSeq n t₀)) < ε

theorem AVenhance.Infra.Parabolic.FourierGalerkin.PathCompactness.exists_weakDual_neighborhood_modulus {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {uSeq : ℕ → ↑TimeInterval → E} (hmod : ∀ (v : E), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ) (t s : ↑TimeInterval), |inner ℝ (uSeq n t) v - inner ℝ (uSeq n s) v| ≤ C * √(dist t s)) {V : Set (WeakDual ℝ E)} (hV : V ∈ nhds 0) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (t₀ t : ↑TimeInterval) (n : ℕ), dist t t₀ < δ → hilbertToWeakDual (uSeq n t) - hilbertToWeakDual (uSeq n t₀) ∈ V

theorem AVenhance.Infra.Parabolic.FourierGalerkin.PathCompactness.exists_finite_dense_test_modulus {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {uSeq : ℕ → ↑TimeInterval → E} {S : Set E} {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ (n : ℕ) (t : ↑TimeInterval), ‖uSeq n t‖ ≤ M) (happrox : ∀ (v : E) (ε : ℝ), 0 < ε → ∃ w ∈ S, dist v w < ε) (hmod : ∀ w ∈ S, ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ) (t s : ↑TimeInterval), |inner ℝ (uSeq n t) w - inner ℝ (uSeq n s) w| ≤ C * √(dist t s)) (s : Finset E) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (t₀ t : ↑TimeInterval) (n : ℕ), dist t t₀ < δ → (s.sup (WeakDual.seminormFamily ℝ E)) (hilbertToWeakDual (uSeq n t) - hilbertToWeakDual (uSeq n t₀)) < ε

theorem AVenhance.Infra.Parabolic.FourierGalerkin.PathCompactness.exists_weakDual_neighborhood_modulus_of_dense_tests {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {uSeq : ℕ → ↑TimeInterval → E} {S : Set E} {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ (n : ℕ) (t : ↑TimeInterval), ‖uSeq n t‖ ≤ M) (happrox : ∀ (v : E) (ε : ℝ), 0 < ε → ∃ w ∈ S, dist v w < ε) (hmod : ∀ w ∈ S, ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ) (t s : ↑TimeInterval), |inner ℝ (uSeq n t) w - inner ℝ (uSeq n s) w| ≤ C * √(dist t s)) {V : Set (WeakDual ℝ E)} (hV : V ∈ nhds 0) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (t₀ t : ↑TimeInterval) (n : ℕ), dist t t₀ < δ → hilbertToWeakDual (uSeq n t) - hilbertToWeakDual (uSeq n t₀) ∈ V

theorem AVenhance.Infra.Parabolic.FourierGalerkin.weakDual_equicontinuous_of_dense_pairing_moduli {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {uSeq : ℕ → ↑PathCompactness.TimeInterval → E} {S : Set E} {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ (n : ℕ) (t : ↑PathCompactness.TimeInterval), ‖uSeq n t‖ ≤ M) (happrox : ∀ (v : E) (ε : ℝ), 0 < ε → ∃ w ∈ S, dist v w < ε) (hmod : ∀ w ∈ S, ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ) (t s : ↑PathCompactness.TimeInterval), |inner ℝ (uSeq n t) w - inner ℝ (uSeq n s) w| ≤ C * √(dist t s)) : Equicontinuous fun (n : ℕ) (t : ↑PathCompactness.TimeInterval) => StrongDual.toWeakDual ((InnerProductSpace.toDualMap ℝ E) (uSeq n t))

Dense-test scalar moduli plus a uniform Hilbert bound imply weak-dual equicontinuity.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.exists_subseq_weakContinuousPath {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] {uSeq : ℕ → C(↑PathCompactness.TimeInterval, E)} {M : ℝ} {u₀ : E} (hbound : ∀ (n : ℕ) (t : ↑PathCompactness.TimeInterval), ‖(uSeq n) t‖ ≤ M) (hinit : ∀ (v : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((uSeq n) ⟨0, ⋯⟩) v) Filter.atTop (nhds (inner ℝ u₀ v))) (hequicont : Equicontinuous fun (n : ℕ) (t : ↑PathCompactness.TimeInterval) => StrongDual.toWeakDual ((InnerProductSpace.toDualMap ℝ E) ((uSeq n) t))) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (u : ↑PathCompactness.TimeInterval → E), (∀ (v : E), Continuous fun (t : ↑PathCompactness.TimeInterval) => inner ℝ (u t) v) ∧ (∀ (t : ↑PathCompactness.TimeInterval) (v : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((uSeq (φ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) ∧ (∀ (t : ↑PathCompactness.TimeInterval), ‖u t‖ ≤ M) ∧ u ⟨0, ⋯⟩ = u₀

Simultaneous pointwise weak extraction for a uniformly bounded, weakly equicontinuous family of continuous paths in a separable real Hilbert space.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.exists_subseq_weakContinuousPath_of_dense_pairing_moduli {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] {uSeq : ℕ → C(↑PathCompactness.TimeInterval, E)} {M : ℝ} {u₀ : E} {S : Set E} (hbound : ∀ (n : ℕ) (t : ↑PathCompactness.TimeInterval), ‖(uSeq n) t‖ ≤ M) (hinit : ∀ (v : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((uSeq n) ⟨0, ⋯⟩) v) Filter.atTop (nhds (inner ℝ u₀ v))) (hM : 0 ≤ M) (happrox : ∀ (v : E) (ε : ℝ), 0 < ε → ∃ w ∈ S, dist v w < ε) (hmod : ∀ w ∈ S, ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ) (t s : ↑PathCompactness.TimeInterval), |inner ℝ ((uSeq n) t) w - inner ℝ ((uSeq n) s) w| ≤ C * √(dist t s)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (u : ↑PathCompactness.TimeInterval → E), (∀ (v : E), Continuous fun (t : ↑PathCompactness.TimeInterval) => inner ℝ (u t) v) ∧ (∀ (t : ↑PathCompactness.TimeInterval) (v : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((uSeq (φ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) ∧ (∀ (t : ↑PathCompactness.TimeInterval), ‖u t‖ ≤ M) ∧ u ⟨0, ⋯⟩ = u₀

The weak path and initial-trace extraction with scalar moduli only on a dense test family. This is the compactness interface suited to Fourier Galerkin equations: the equation controls each fixed trigonometric test, while the uniform L² bound extends the modulus to all tests.