Spatial support is preserved by the actual zero-endpoint history inverse.

noncomputable def EulerLpCylinderTranslation.spatialCutoff (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : ↥(CylinderL2 P V) →L[ℝ] ↥(CylinderL2 P V)

Spatial cutoff, given by cutoffOperator (liftMeasure P) (spatialSet P S) (spatialSet_measurable P S hS).

Equations

• EulerLpCylinderTranslation.spatialCutoff P S hS = EulerLpSupportedSubspace.cutoffOperator (EulerLiftedGradientSpace.liftMeasure P) (EulerLpCylinderTranslation.spatialSet P S) ⋯

theorem EulerLpCylinderTranslation.spatialCutoff_norm (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : ‖spatialCutoff P S hS‖ ≤ 1

theorem EulerLpCylinderTranslation.spatialCutoff_fix (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : ↥(CylinderL2 P V)) : u ∈ EulerLpCylinderPaths.Supported P V S hS ↔ (spatialCutoff P S hS) u = u

theorem EulerLpCylinderTranslation.spatialCutoff_adjoint (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) [CompleteSpace V] : ContinuousLinearMap.adjoint (spatialCutoff P S hS) = spatialCutoff P S hS

theorem EulerLpCylinderTranslation.spatialCutoff_path_fix (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) {K : Type u_2} [TopologicalSpace K] (f : C(K, ↥(CylinderL2 P V))) (hf : ∀ (t : K), f t ∈ EulerLpCylinderPaths.Supported P V S hS) : (ContinuousLinearMap.compLeftContinuous ℝ K (spatialCutoff P S hS)) f = f

theorem EulerCylinderDirichlet.Coefficients.frame_cutoff (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((frame P D) t) ((EulerLpCylinderTranslation.spatialCutoff P S hS) u) = (EulerLpCylinderTranslation.spatialCutoff P S hS) (((frame P D) t) u)

theorem EulerCylinderDirichlet.Coefficients.frameDerivative_cutoff (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((frameDerivative P D) t) ((EulerLpCylinderTranslation.spatialCutoff P S hS) u) = (EulerLpCylinderTranslation.spatialCutoff P S hS) (((frameDerivative P D) t) u)

theorem EulerCylinderDirichlet.Coefficients.hessian_cutoff (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)) : ((hessian P D) t) ((EulerLpCylinderTranslation.spatialCutoff P S hS) u) = (EulerLpCylinderTranslation.spatialCutoff P S hS) (((hessian P D) t) u)

theorem EulerCylinderDirichlet.Coefficients.frame_cutoff_back (P : ℝ) [Fact (0 < P)] {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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((frame P D) t) ((ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.spatialCutoff P S hS)) u) = (ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.spatialCutoff P S hS)) (((frame P D) t) u)

theorem EulerCylinderDirichlet.Coefficients.frameDerivative_cutoff_back (P : ℝ) [Fact (0 < P)] {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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((frameDerivative P D) t) ((ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.spatialCutoff P S hS)) u) = (ContinuousLinearMap.adjoint (EulerLpCylinderTranslation.spatialCutoff P S hS)) (((frameDerivative P D) t) u)

theorem EulerCylinderDirichlet.Coefficients.velocityLp_cutoff (P : ℝ) [Fact (0 < P)] {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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : (velocityLp P D) ((EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.spatialCutoff P S hS)) f) = (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.spatialCutoff P S hS)) ((velocityLp P D) f)

theorem EulerCylinderDirichlet.Coefficients.velocityPath_cutoff (P : ℝ) [Fact (0 < P)] {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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : ((velocityPath P D) ((EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.spatialCutoff P S hS)) f)) t = (EulerLpCylinderTranslation.spatialCutoff P S hS) (((velocityPath P D) f) t)

theorem EulerCylinderDirichlet.Coefficients.velocityPath_supported (P : ℝ) [Fact (0 < P)] {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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ∀ (t : ↑(Set.Icc 0 T)), f t ∈ EulerLpCylinderPaths.Supported P E S hS) (t : ↑(Set.Icc 0 T)) : ((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t ∈ EulerLpCylinderPaths.Supported P U S hS

theorem EulerCylinderDirichlet.Coefficients.accelerationPath_supported (P : ℝ) [Fact (0 < P)] {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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ∀ (t : ↑(Set.Icc 0 T)), f t ∈ EulerLpCylinderPaths.Supported P E S hS) (t : ↑(Set.Icc 0 T)) : (accelerationPath P D f) t ∈ EulerLpCylinderPaths.Supported P U S hS

theorem EulerCylinderDirichlet.Coefficients.physicalVelocity_supported (P : ℝ) [Fact (0 < P)] {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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ∀ (t : ↑(Set.Icc 0 T)), f t ∈ EulerLpCylinderPaths.Supported P E S hS) (t : ↑(Set.Icc 0 T)) : (physicalVelocity P D f) t ∈ EulerLpCylinderPaths.Supported P E S hS

theorem EulerCylinderDirichlet.Coefficients.physicalDerivative_supported (P : ℝ) [Fact (0 < P)] {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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ∀ (t : ↑(Set.Icc 0 T)), f t ∈ EulerLpCylinderPaths.Supported P E S hS) (t : ↑(Set.Icc 0 T)) : (physicalDerivative P D f) t ∈ EulerLpCylinderPaths.Supported P E S hS