Closed graphs of the genuine strong cylinder translation derivatives.

theorem EulerClosedTranslationGraph.translationPath_add (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (s t : ℝ) : EulerPressureSpatialRegularity.translationPath period a (s + t) = EulerPressureSpatialRegularity.translationPath period a s + EulerPressureSpatialRegularity.translationPath period a t

A covering-space direction gives an additive one-parameter cylinder translation.

theorem EulerClosedTranslationGraph.translation_hasDerivAt_all (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) (h : HasDerivAt (fun (s : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a s)) f) g 0) (t : ℝ) : HasDerivAt (fun (s : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a s)) f) ((EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) g) t

Strong differentiation of a translation orbit at zero determines its derivative everywhere.

theorem EulerClosedTranslationGraph.translation_orbits_tendstoUniformly (period : ℝ) [Fact (0 < period)] {ι : Type u_1} {l : Filter ι} (a : EulerLiftedGradientSpace.LiftTangent) (f : ι → ↥(EulerLiftedGradientSpace.LiftL2 period)) (g : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : Filter.Tendsto f l (nhds g)) : TendstoUniformly (fun (n : ι) (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) (f n)) (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) g) l

Convergence of L² fields gives uniform convergence of their entire isometric translation orbits.

def EulerClosedTranslationGraph.translationDerivativeGraph (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) : Submodule ℝ (↥(EulerLiftedGradientSpace.LiftL2 period) × ↥(EulerLiftedGradientSpace.LiftL2 period))

The graph of one genuine strong L² translation derivative, as a linear subspace.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerClosedTranslationGraph.translationDerivativeGraph_closed (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) : IsClosed ↑(translationDerivativeGraph period a)

The strong translation derivative is a closed operator on the actual cylinder L² space.