Spatial support is preserved by the actual angular primitive, mixed derivative, and slow curl paths.

@[instance_reducible]

noncomputable def EulerCylinderLocalSupport.instCylinderLocalSupport1 (P : ℝ) [Fact (0 < P)] : NormedAddCommGroup ↥(EulerLiftedGradientSpace.LiftL2 P)

Cache the standard NormedAddCommGroup (LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderLocalSupport.instCylinderLocalSupport1 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderLocalSupport.instCylinderLocalSupport2 (P : ℝ) [Fact (0 < P)] : NormedSpace ℝ ↥(EulerLiftedGradientSpace.LiftL2 P)

Cache the standard NormedSpace ℝ (LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderLocalSupport.instCylinderLocalSupport2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderLocalSupport.instCylinderLocalSupport3 (P : ℝ) [Fact (0 < P)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS)

Cache the standard NormedAddCommGroup (Supported P Space S hS) instance to shorten typeclass synthesis.

Equations

• EulerCylinderLocalSupport.instCylinderLocalSupport3 P S hS = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderLocalSupport.instCylinderLocalSupport4 (P : ℝ) [Fact (0 < P)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS)

Cache the standard NormedSpace ℝ (Supported P Space S hS) instance to shorten typeclass synthesis.

Equations

• EulerCylinderLocalSupport.instCylinderLocalSupport4 P S hS = inferInstance

theorem EulerCylinderLocalSupport.primitive_supported (P : ℝ) [Fact (0 < P)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu : u ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) : (EulerCylinderAnglePrimitive.primitive P) u ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS

Pure angular integration does not move the spatial support.

theorem EulerCylinderLocalSupport.fieldFDeriv_zero_outside (P : ℝ) (S : Set EulerSmoothLimit.Space) (hSc : IsClosed S) (f : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), x.1 ∉ S → f x = 0) (x : EulerLiftedGradientSpace.LiftDomain P) (hx : x.1 ∉ S) : EulerLiftedWeakDerivative.fieldFDeriv P f x = 0

Outside a closed spatial support, all local first derivatives vanish.

theorem EulerCylinderLocalSupport.pointField_zero_outside (P : ℝ) [Fact (0 < P)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hSc : IsClosed S) (hs : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (t : K) (x : EulerLiftedGradientSpace.LiftDomain P) (hx : x.1 ∉ S) : EulerCylinderSmoothOrbit.pointField P p hp t x = 0

theorem EulerCylinderLocalSupport.derivativePath_supported (P : ℝ) [Fact (0 < P)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hSc : IsClosed S) (hs : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (i : Fin 4) (t : K) : (EulerCylinderSmoothOrbit.derivativePath P p i) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS

theorem EulerCylinderLocalSupport.potentialPath_supported (P : ℝ) [Fact (0 < P)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hs : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (t : K) : (EulerCylinderPotential.potentialPath P B p) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS

theorem EulerCylinderLocalSupport.slowCurlPath_supported (P : ℝ) [Fact (0 < P)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hSc : IsClosed S) (hs : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (t : K) : (EulerCylinderSlowCurl.path P G p) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS