Uniform convergence of actual finite metric energies along continuous Hilbert-space paths.
theorem
EulerMetricPathConvergence.familyMetricNorm_continuous
{I : Type u_1}
{H : Type u_2}
[Fintype I]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
:
Continuous fun (p : (H →L[ℝ] H) × (I → H)) => EulerFiniteMetricEnergy.familyMetricNorm p.1 p.2
A finite family metric norm is continuous jointly in its actual bounded metric and field.
noncomputable def
EulerMetricPathConvergence.metricPath
{I : Type u_1}
{H : Type u_2}
[Fintype I]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
(T : ℝ)
(K : C(↑(Set.Icc 0 T), H →L[ℝ] H))
(u : C(↑(Set.Icc 0 T), I → H))
:
The actual finite-family metric norm along a continuous time path.
Equations
- EulerMetricPathConvergence.metricPath T K u = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerFiniteMetricEnergy.familyMetricNorm (K t) (u t), continuous_toFun := ⋯ }
Instances For
theorem
EulerMetricPathConvergence.metricPath_continuous
{I : Type u_1}
{H : Type u_2}
[Fintype I]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
(T : ℝ)
(K : C(↑(Set.Icc 0 T), H →L[ℝ] H))
:
Continuous fun (u : C(↑(Set.Icc 0 T), I → H)) => metricPath T K u
The actual metric-root path depends continuously on the field path in the uniform topology.
theorem
EulerMetricPathConvergence.metricPath_tendsto
{I : Type u_1}
{H : Type u_2}
[Fintype I]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
(T : ℝ)
(K : C(↑(Set.Icc 0 T), H →L[ℝ] H))
(u : ℕ → C(↑(Set.Icc 0 T), I → H))
(v : C(↑(Set.Icc 0 T), I → H))
(hu : Filter.Tendsto u Filter.atTop (nhds v))
:
Filter.Tendsto (fun (n : ℕ) => metricPath T K (u n)) Filter.atTop (nhds (metricPath T K v))
Strong uniform field convergence gives uniform convergence of the actual square-root metric energy, including zeros.
noncomputable def
EulerMetricPathConvergence.weightedMetricPath
{I : Type u_1}
{H : Type u_2}
[Fintype I]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
{A : Type u_3}
[Fintype A]
(T : ℝ)
(w : A → C(↑(Set.Icc 0 T), ℝ))
(K : C(↑(Set.Icc 0 T), H →L[ℝ] H))
(u : A → C(↑(Set.Icc 0 T), I → H))
:
A finite weighted sum of actual metric-root paths.
Equations
- EulerMetricPathConvergence.weightedMetricPath T w K u = ∑ i : A, w i * EulerMetricPathConvergence.metricPath T K (u i)
Instances For
theorem
EulerMetricPathConvergence.weightedMetricPath_apply
{I : Type u_1}
{H : Type u_2}
[Fintype I]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
{A : Type u_3}
[Fintype A]
(T : ℝ)
(w : A → C(↑(Set.Icc 0 T), ℝ))
(K : C(↑(Set.Icc 0 T), H →L[ℝ] H))
(u : A → C(↑(Set.Icc 0 T), I → H))
(t : ↑(Set.Icc 0 T))
:
(weightedMetricPath T w K u) t = ∑ i : A, (w i) t * EulerFiniteMetricEnergy.familyMetricNorm (K t) ((u i) t)
A bundled finite metric path evaluates to its literal weighted metric-root sum.
theorem
EulerMetricPathConvergence.weightedMetricPath_tendsto
{I : Type u_1}
{H : Type u_2}
[Fintype I]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
{A : Type u_3}
[Fintype A]
(T : ℝ)
(w : A → C(↑(Set.Icc 0 T), ℝ))
(K : C(↑(Set.Icc 0 T), H →L[ℝ] H))
(u : ℕ → A → C(↑(Set.Icc 0 T), I → H))
(v : A → C(↑(Set.Icc 0 T), I → H))
(hu : ∀ (i : A), Filter.Tendsto (fun (n : ℕ) => u n i) Filter.atTop (nhds (v i)))
:
Filter.Tendsto (fun (n : ℕ) => weightedMetricPath T w K (u n)) Filter.atTop (nhds (weightedMetricPath T w K v))
Every finite Gevrey metric sum passes uniformly through actual strong field approximations.