Metric Energy Evolution

theorem EulerMetricEnergyEvolution.metric_energy_hasDerivAt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : ℝ → H →L[ℝ] H) (e : ℝ → H) (t : ℝ) (K' : H →L[ℝ] H) (e' : H) (hK : HasDerivAt K K' t) (he : HasDerivAt e e' t) (hsym : ∀ (v w : H), inner ℝ ((K t) v) w = inner ℝ v ((K t) w)) : HasDerivAt (fun (s : ℝ) => inner ℝ ((K s) (e s)) (e s)) (inner ℝ (K' (e t)) (e t) + 2 * inner ℝ ((K t) (e t)) e') t

The exact time derivative of a quadratic energy with a moving metric.

theorem EulerMetricEnergyEvolution.metric_energy_evolution {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : ℝ → H →L[ℝ] H) (e : ℝ → H) (t : ℝ) (K' : H →L[ℝ] H) (e' transport pressure forcing : H) (hK : HasDerivAt K K' t) (he : HasDerivAt e e' t) (hsym : ∀ (v w : H), inner ℝ ((K t) v) w = inner ℝ v ((K t) w)) (heq : e' + transport + pressure = forcing) (hp : inner ℝ ((K t) (e t)) pressure = 0) : HasDerivAt (fun (s : ℝ) => inner ℝ ((K s) (e s)) (e s)) (inner ℝ (K' (e t)) (e t) + 2 * inner ℝ ((K t) (e t)) forcing - 2 * inner ℝ ((K t) (e t)) transport) t

Cancellation of pressure and integration by parts for transport leave only metric variation and the forcing in the time derivative.

theorem EulerMetricEnergyEvolution.energy_derivative_bound {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K K' : H →L[ℝ] H) (e transport forcing : H) (B : ℝ) (_hB : 0 ≤ B) (ht : |inner ℝ (K e) transport| ≤ B * ‖e‖ ^ 2) : inner ℝ (K' e) e + 2 * inner ℝ (K e) forcing - 2 * inner ℝ (K e) transport ≤ (‖K'‖ + 2 * B) * ‖e‖ ^ 2 + 2 * ‖K‖ * ‖e‖ * ‖forcing‖

theorem EulerMetricEnergyEvolution.regularized_metric_norm_hasDerivAt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : ℝ → H →L[ℝ] H) (e : ℝ → H) (t δ : ℝ) (K' : H →L[ℝ] H) (e' : H) (hδ : 0 < δ) (hpos : 0 ≤ inner ℝ ((K t) (e t)) (e t)) (hK : HasDerivAt K K' t) (he : HasDerivAt e e' t) (hsym : ∀ (v w : H), inner ℝ ((K t) v) w = inner ℝ v ((K t) w)) : HasDerivAt (fun (s : ℝ) => √(inner ℝ ((K s) (e s)) (e s) + δ ^ 2)) ((inner ℝ (K' (e t)) (e t) + 2 * inner ℝ ((K t) (e t)) e') / (2 * √(inner ℝ ((K t) (e t)) (e t) + δ ^ 2))) t

A positive regularization gives a differentiable metric norm even at zero.

theorem EulerMetricEnergyEvolution.regularized_metric_norm_evolution {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : ℝ → H →L[ℝ] H) (e : ℝ → H) (t δ c B : ℝ) (K' : H →L[ℝ] H) (e' transport pressure forcing : H) (hδ : 0 < δ) (hc : 0 < c) (hB : 0 ≤ B) (hcoercive : c ^ 2 * ‖e t‖ ^ 2 ≤ inner ℝ ((K t) (e t)) (e t)) (hK : HasDerivAt K K' t) (he : HasDerivAt e e' t) (hsym : ∀ (v w : H), inner ℝ ((K t) v) w = inner ℝ v ((K t) w)) (heq : e' + transport + pressure = forcing) (hp : inner ℝ ((K t) (e t)) pressure = 0) (ht : |inner ℝ ((K t) (e t)) transport| ≤ B * ‖e t‖ ^ 2) : deriv (fun (s : ℝ) => √(inner ℝ ((K s) (e s)) (e s) + δ ^ 2)) t ≤ (‖K'‖ + 2 * B) / (2 * c ^ 2) * √(inner ℝ ((K t) (e t)) (e t) + δ ^ 2) + ‖K t‖ / c * ‖forcing‖

The norm estimate used before summing Gevrey weights. All terms come from the actual differential equation; no estimate for the energy derivative is assumed.