Finite sums of genuine Hilbert metric energies, with viscosity and explicit norm comparison.

def EulerFiniteMetricEnergy.familySquaredNorm {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] (v : ι → H) : ℝ

The square of the Hilbert norm of a finite family.

Equations

• EulerFiniteMetricEnergy.familySquaredNorm v = ∑ i : ι, ‖v i‖ ^ 2

noncomputable def EulerFiniteMetricEnergy.familyNorm {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] (v : ι → H) : ℝ

The Hilbert norm of a finite family, expressed without choosing a product-space model.

Equations

• EulerFiniteMetricEnergy.familyNorm v = √(EulerFiniteMetricEnergy.familySquaredNorm v)

def EulerFiniteMetricEnergy.familyEnergy {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : H →L[ℝ] H) (v : ι → H) : ℝ

The actual sum of metric quadratic energies of a finite family.

Equations

• EulerFiniteMetricEnergy.familyEnergy K v = ∑ i : ι, inner ℝ (K (v i)) (v i)

noncomputable def EulerFiniteMetricEnergy.familyMetricNorm {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : H →L[ℝ] H) (v : ι → H) : ℝ

The source's square root of the sum of all base-word metric energies.

Equations

• EulerFiniteMetricEnergy.familyMetricNorm K v = √(EulerFiniteMetricEnergy.familyEnergy K v)

theorem EulerFiniteMetricEnergy.familySquaredNorm_nonneg {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] (v : ι → H) : 0 ≤ familySquaredNorm v

theorem EulerFiniteMetricEnergy.familyNorm_nonneg {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] (v : ι → H) : 0 ≤ familyNorm v

theorem EulerFiniteMetricEnergy.familyNorm_sq {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] (v : ι → H) : familyNorm v ^ 2 = familySquaredNorm v

theorem EulerFiniteMetricEnergy.family_cauchy_schwarz {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] (v w : ι → H) : ∑ i : ι, ‖v i‖ * ‖w i‖ ≤ familyNorm v * familyNorm w

Cauchy-Schwarz for the actual component norms of two finite Hilbert families.

theorem EulerFiniteMetricEnergy.familyNorm_le_sum_norm {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] (v : ι → H) : familyNorm v ≤ ∑ i : ι, ‖v i‖

The root-of-squares norm is bounded by the sum of component norms.

theorem EulerFiniteMetricEnergy.sum_norm_le_card_sqrt_familyNorm {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] (v : ι → H) : ∑ i : ι, ‖v i‖ ≤ √↑(Fintype.card ι) * familyNorm v

The reverse finite-dimensional comparison has only the fixed square-root cardinality loss.

theorem EulerFiniteMetricEnergy.familyEnergy_coercive {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : H →L[ℝ] H) (v : ι → H) (c : ℝ) (hK : ∀ (u : H), c ^ 2 * ‖u‖ ^ 2 ≤ inner ℝ (K u) u) : c ^ 2 * familySquaredNorm v ≤ familyEnergy K v

Pointwise operator coercivity sums exactly over a finite family.

theorem EulerFiniteMetricEnergy.familyEnergy_upper {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : H →L[ℝ] H) (v : ι → H) : familyEnergy K v ≤ ‖K‖ * familySquaredNorm v

The metric energy has the exact operator-norm upper bound.

theorem EulerFiniteMetricEnergy.familyMetricNorm_lower {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : H →L[ℝ] H) (v : ι → H) (c : ℝ) (hc : 0 ≤ c) (hK : ∀ (u : H), c ^ 2 * ‖u‖ ^ 2 ≤ inner ℝ (K u) u) : c * familyNorm v ≤ familyMetricNorm K v

Coercivity makes the root-of-sum metric norm uniformly equivalent to the finite Hilbert norm.

theorem EulerFiniteMetricEnergy.familyMetricNorm_upper {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : H →L[ℝ] H) (v : ι → H) : familyMetricNorm K v ≤ √‖K‖ * familyNorm v

The upper metric comparison is independent of the number of external derivatives.

theorem EulerFiniteMetricEnergy.family_energy_hasDerivAt {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : ℝ → H →L[ℝ] H) (e : ι → ℝ → H) (t ν : ℝ) (K' : H →L[ℝ] H) (e' transport pressure forcing lap : ι → H) (hK : HasDerivAt K K' t) (he : ∀ (i : ι), HasDerivAt (e i) (e' i) t) (hsym : ∀ (v w : H), inner ℝ ((K t) v) w = inner ℝ v ((K t) w)) (heq : ∀ (i : ι), e' i + transport i + pressure i = forcing i + ν • lap i) (hp : ∀ (i : ι), inner ℝ ((K t) (e i t)) (pressure i) = 0) : HasDerivAt (fun (s : ℝ) => familyEnergy (K s) fun (i : ι) => e i s) (∑ i : ι, (inner ℝ (K' (e i t)) (e i t) + 2 * inner ℝ ((K t) (e i t)) (forcing i + ν • lap i) - 2 * inner ℝ ((K t) (e i t)) (transport i))) t

The exact derivative of the finite quadratic energy for a transport-pressure-heat system.

theorem EulerFiniteMetricEnergy.family_energy_derivative_bound {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K K' : H →L[ℝ] H) (e transport forcing lap : ι → H) (B C ν : ℝ) (hB : 0 ≤ B) (hν : 0 ≤ ν) (ht : ∀ (i : ι), |inner ℝ (K (e i)) (transport i)| ≤ B * ‖e i‖ ^ 2) (hheat : ∀ (i : ι), inner ℝ (K (e i)) (lap i) ≤ C * ‖e i‖ ^ 2) : ∑ i : ι, (inner ℝ (K' (e i)) (e i) + 2 * inner ℝ (K (e i)) (forcing i + ν • lap i) - 2 * inner ℝ (K (e i)) (transport i)) ≤ (‖K'‖ + 2 * B + 2 * ν * C) * familySquaredNorm e + 2 * ‖K‖ * familyNorm e * familyNorm forcing

The finite energy estimate keeps forcing in the Hilbert sum norm and treats heat through its proved quadratic bound.

theorem EulerFiniteMetricEnergy.family_regularized_energy_evolution {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : ℝ → H →L[ℝ] H) (e : ι → ℝ → H) (t δ c B C ν : ℝ) (K' : H →L[ℝ] H) (e' transport pressure forcing lap : ι → H) (hδ : 0 < δ) (hc : 0 < c) (hB : 0 ≤ B) (hC : 0 ≤ C) (hν : 0 ≤ ν) (hcoercive : ∀ (u : H), c ^ 2 * ‖u‖ ^ 2 ≤ inner ℝ ((K t) u) u) (hK : HasDerivAt K K' t) (he : ∀ (i : ι), HasDerivAt (e i) (e' i) t) (hsym : ∀ (v w : H), inner ℝ ((K t) v) w = inner ℝ v ((K t) w)) (heq : ∀ (i : ι), e' i + transport i + pressure i = forcing i + ν • lap i) (hp : ∀ (i : ι), inner ℝ ((K t) (e i t)) (pressure i) = 0) (ht : ∀ (i : ι), |inner ℝ ((K t) (e i t)) (transport i)| ≤ B * ‖e i t‖ ^ 2) (hheat : ∀ (i : ι), inner ℝ ((K t) (e i t)) (lap i) ≤ C * ‖e i t‖ ^ 2) : deriv (fun (s : ℝ) => √((familyEnergy (K s) fun (i : ι) => e i s) + δ ^ 2)) t ≤ (‖K'‖ + 2 * B + 2 * ν * C) / (2 * c ^ 2) * √((familyEnergy (K t) fun (i : ι) => e i t) + δ ^ 2) + ‖K t‖ / c * familyNorm forcing

Regularized root energy for a finite family, with constants independent of its cardinality.