The actual history solve commutes with all mixed spatial/angular translations.

theorem EulerLpCylinderRectangular.fullOperator_translation_back (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (a : EulerLiftedGradientSpace.LiftTangent) (Q : BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] E)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((fullOperatorMap P) Q) ((ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) u) = (ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) (((fullOperatorMap P) (EulerMeanCoefficients.translated Q a.1)) u)

noncomputable def EulerCylinderDirichlet.Coefficients.shifted {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (a : EulerSmoothLimit.Space) : Coefficients T U E

The actual translated coefficient fields, with their inherited pointwise time derivatives and unchanged coercivity constants.

Equations

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

theorem EulerCylinderDirichlet.Coefficients.shifted_frame {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((frame P (D.shifted a.1)) t) ((EulerLpCylinderTranslation.translate P a) u) = (EulerLpCylinderTranslation.translate P a) (((frame P D) t) u)

theorem EulerCylinderDirichlet.Coefficients.shifted_frameDerivative {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((frameDerivative P (D.shifted a.1)) t) ((EulerLpCylinderTranslation.translate P a) u) = (EulerLpCylinderTranslation.translate P a) (((frameDerivative P D) t) u)

theorem EulerCylinderDirichlet.Coefficients.shifted_hessian {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)) : ((hessian P (D.shifted a.1)) t) ((EulerLpCylinderTranslation.translate P a) u) = (EulerLpCylinderTranslation.translate P a) (((hessian P D) t) u)

theorem EulerCylinderDirichlet.Coefficients.shifted_frame_back {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((frame P D) t) ((ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) u) = (ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) (((frame P (D.shifted a.1)) t) u)

theorem EulerCylinderDirichlet.Coefficients.shifted_frameDerivative_back {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((frameDerivative P D) t) ((ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) u) = (ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) (((frameDerivative P (D.shifted a.1)) t) u)

theorem EulerCylinderDirichlet.Coefficients.velocityLp_translation {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : (velocityLp P (D.shifted a.1)) ((EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) f) = (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) ((velocityLp P D) f)

theorem EulerCylinderDirichlet.Coefficients.velocityPath_translation {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : ((velocityPath P (D.shifted a.1)) ((EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) f)) t = (EulerLpCylinderTranslation.translate P a) (((velocityPath P D) f) t)

theorem EulerCylinderDirichlet.Coefficients.continuousVelocity_translation {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : ((velocityPath P (D.shifted a.1)) (EulerTimeLp.pathLp T ⋯ ((EulerLpCylinderTranslation.pathTranslate P a) f))) t = (EulerLpCylinderTranslation.translate P a) (((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t)

theorem EulerCylinderDirichlet.Coefficients.accelerationPath_translation {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : (accelerationPath P (D.shifted a.1) ((EulerLpCylinderTranslation.pathTranslate P a) f)) t = (EulerLpCylinderTranslation.translate P a) ((accelerationPath P D f) t)

theorem EulerCylinderDirichlet.Coefficients.physicalVelocity_translation {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : (physicalVelocity P (D.shifted a.1) ((EulerLpCylinderTranslation.pathTranslate P a) f)) t = (EulerLpCylinderTranslation.translate P a) ((physicalVelocity P D f) t)

theorem EulerCylinderDirichlet.Coefficients.physicalDerivative_translation {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : (physicalDerivative P (D.shifted a.1) ((EulerLpCylinderTranslation.pathTranslate P a) f)) t = (EulerLpCylinderTranslation.translate P a) ((physicalDerivative P D f) t)