The literal periodic vector potential as an actual continuous cylinder L² path.

Time differentiation of the actual normalized angular integral on the cylinder.

Same-radius mixed-word and continuous-time estimates for the actual angular operator.

theorem EulerCylinderAnglePrimitive.primitive_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (s : Set ℝ) (t : ℝ) (u : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 P)) (ut : ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu : HasDerivWithinAt u ut s t) : HasDerivWithinAt (fun (r : ℝ) => (primitive P) (u r)) ((primitive P) ut) s t

theorem EulerCylinderAnglePrimitive.primitive_mixed_translation (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftTangent) (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) : (primitive P) ((EulerLpCylinderTranslation.translate P a) u) = (EulerLpCylinderTranslation.translate P a) ((primitive P) u)

theorem EulerCylinderAnglePrimitive.primitive_block_bound (P : ℝ) [Fact (0 < P)] {X : Type u_1} {ι : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [Fintype ι] (directions : ι → X) (q : ℕ) (f : X → ↥(EulerLiftedGradientSpace.LiftL2 P)) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (primitive P) (f y)) n x ≤ P * EulerParameterWordGevrey.block directions q f n x

theorem EulerCylinderAnglePrimitive.primitive_block_majorant (P : ℝ) [Fact (0 < P)] {X : Type u_1} {ι : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [Fintype ι] (directions : ι → X) (q : ℕ) (f : X → ↥(EulerLiftedGradientSpace.LiftL2 P)) (hf : ContDiff ℝ (↑⊤) f) (R C : ℝ) (d : ℕ) (hb : ∀ (n : ℕ) (x : X), EulerParameterWordGevrey.block directions q f n x ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (primitive P) (f y)) n x ≤ P * C * EulerGevrey.majorant R d n

@[instance_reducible]

noncomputable def EulerCylinderAnglePrimitive.instCylinderAngleWordBounds1 (P : ℝ) [Fact (0 < P)] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

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

Equations

• EulerCylinderAnglePrimitive.instCylinderAngleWordBounds1 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderAnglePrimitive.instCylinderAngleWordBounds2 (P : ℝ) [Fact (0 < P)] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

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

Equations

• EulerCylinderAnglePrimitive.instCylinderAngleWordBounds2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderAnglePrimitive.instCylinderAngleWordBounds3 (P : ℝ) [Fact (0 < P)] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup (C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)) →L[ℝ] C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))

Cache the standard NormedAddCommGroup (C(K,LiftL2 P) →L[ℝ] C(K,LiftL2 P)) instance to shorten typeclass synthesis.

Equations

• EulerCylinderAnglePrimitive.instCylinderAngleWordBounds3 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderAnglePrimitive.instCylinderAngleWordBounds4 (P : ℝ) [Fact (0 < P)] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ (C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)) →L[ℝ] C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))

Cache the standard NormedSpace ℝ (C(K,LiftL2 P) →L[ℝ] C(K,LiftL2 P)) instance to shorten typeclass synthesis.

Equations

• EulerCylinderAnglePrimitive.instCylinderAngleWordBounds4 P = inferInstance

noncomputable def EulerCylinderAnglePrimitive.pathPrimitive (P : ℝ) [Fact (0 < P)] {K : Type u_3} [TopologicalSpace K] : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)) →L[ℝ] C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Path primitive, given by (primitive P).compLeftContinuous ℝ K.

Equations

• EulerCylinderAnglePrimitive.pathPrimitive P = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderAnglePrimitive.primitive P)

@[simp]

theorem EulerCylinderAnglePrimitive.pathPrimitive_apply (P : ℝ) [Fact (0 < P)] {K : Type u_3} [TopologicalSpace K] (u : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (t : K) : ((pathPrimitive P) u) t = (primitive P) (u t)

theorem EulerCylinderAnglePrimitive.pathPrimitive_norm (P : ℝ) [Fact (0 < P)] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] : ‖pathPrimitive P‖ ≤ P

theorem EulerCylinderAnglePrimitive.pathPrimitive_block_bound (P : ℝ) [Fact (0 < P)] {X : Type u_1} {ι : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [Fintype ι] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] (directions : ι → X) (q : ℕ) (f : X → C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (pathPrimitive P) (f y)) n x ≤ P * EulerParameterWordGevrey.block directions q f n x

The angular operation preserves the same fixed base order and radius in the true time supremum.

theorem EulerCylinderAnglePrimitive.pathPrimitive_block_majorant (P : ℝ) [Fact (0 < P)] {X : Type u_1} {ι : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [Fintype ι] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] (directions : ι → X) (q : ℕ) (f : X → C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hf : ContDiff ℝ (↑⊤) f) (R C : ℝ) (d : ℕ) (hb : ∀ (n : ℕ) (x : X), EulerParameterWordGevrey.block directions q f n x ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (pathPrimitive P) (f y)) n x ≤ P * C * EulerGevrey.majorant R d n

theorem EulerCylinderAnglePrimitive.pathPrimitive_translation (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (a : EulerLiftedGradientSpace.LiftTangent) : (pathPrimitive P) ((EulerLpCylinderTranslation.pathTranslate P a) p) = (EulerLpCylinderTranslation.pathTranslate P a) ((pathPrimitive P) p)

theorem EulerCylinderAnglePrimitive.pathPrimitive_orbit_contDiff (P : ℝ) [Fact (0 < P)] {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) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((pathPrimitive P) p)

theorem EulerCylinderAnglePrimitive.primitive_sobolevPath (P : ℝ) [Fact (0 < P)] {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) (q : ℕ) (t : K) : (EulerCylinderSmoothOrbit.sobolevPath P q ((pathPrimitive P) p) ⋯) t = (sobolevPrimitive P q) ((EulerCylinderSmoothOrbit.sobolevPath P q p hp) t)

theorem EulerCylinderAnglePrimitive.pointField_primitive_formula (P : ℝ) [Fact (0 < P)] {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) (hmean : ∀ (t : K) (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s) = 0) (t : K) (y : EulerLiftedGradientSpace.Vector3) (θ : ℝ) : EulerCylinderSmoothOrbit.pointField P ((pathPrimitive P) p) ⋯ t (y, ↑θ) = EulerAngleMeanZeroPrimitive.primitive P (fun (s : ℝ) => EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s)) θ

The representative of the time-dependent L² primitive is the same explicit angular integral.

theorem EulerCylinderAnglePrimitive.pathPrimitive_time_derivative (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (f t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT ((pathPrimitive P) p)) (((pathPrimitive P) f) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderAnglePrimitive.classicalPrimitive_time_derivative (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (f t) (Set.Icc 0 T) ↑t) (hpm : ∀ (t : ↑(Set.Icc 0 T)) (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s) = 0) (hfm : ∀ (t : ↑(Set.Icc 0 T)) (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P f hf t (y, ↑s) = 0) (t : ↑(Set.Icc 0 T)) (y : EulerLiftedGradientSpace.Vector3) (θ : ℝ) : HasDerivWithinAt (fun (r : ℝ) => EulerAngleMeanZeroPrimitive.primitive P (fun (s : ℝ) => EulerCylinderSmoothOrbit.pointField P p hp (Set.projIcc 0 T hT r) (y, ↑s)) θ) (EulerAngleMeanZeroPrimitive.primitive P (fun (s : ℝ) => EulerCylinderSmoothOrbit.pointField P f hf t (y, ↑s)) θ) (Set.Icc 0 T) ↑t

The literal primitive differentiates within the closed time interval at every angle.

noncomputable def EulerCylinderPotential.potentialPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Potential path, given by fullMultiplierMap P B (pathPrimitive P p).

Equations

• EulerCylinderPotential.potentialPath P B p = ((EulerLpCylinderRectangular.fullMultiplierMap P) B) ((EulerCylinderAnglePrimitive.pathPrimitive P) p)

theorem EulerCylinderPotential.potentialPath_orbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (potentialPath P B p)

noncomputable def EulerCylinderPotential.potentialField (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space

Potential field, given by pointField P (potentialPath P B p) (potentialPath_orbit P B hB p hp) t.

Equations

• EulerCylinderPotential.potentialField P B hB p hp t = EulerCylinderSmoothOrbit.pointField P (EulerCylinderPotential.potentialPath P B p) ⋯ t

theorem EulerCylinderPotential.potentialPath_ae (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : ↑↑((potentialPath P B p) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => ((B t) x.1) (EulerCylinderSmoothOrbit.pointField P ((EulerCylinderAnglePrimitive.pathPrimitive P) p) ⋯ t x)

theorem EulerCylinderPotential.potentialField_formula (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hmean : ∀ (t : K) (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s) = 0) (t : K) (y : EulerSmoothLimit.Space) (θ : ℝ) : potentialField P B hB p hp t (y, ↑θ) = ((B t) y) (EulerAngleMeanZeroPrimitive.primitive P (fun (s : ℝ) => EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s)) θ)

The canonical representative is the coefficient times the literal angular primitive.

theorem EulerCylinderPotential.potentialField_source_formula (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hmean : ∀ (t : K) (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s) = 0) (m : K → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hBm : ∀ (t : K) (y : EulerSmoothLimit.Space), (B t) y = EulerPacketCrossProduct.potentialMultiplier (m t y)) (t : K) (y : EulerSmoothLimit.Space) (θ : ℝ) : potentialField P B hB p hp t (y, ↑θ) = EulerPacketAngularPotential.potential P (m t y) (fun (s : ℝ) => EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s)) θ

theorem EulerCylinderPotential.potentialField_eq_periodic (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hmean : ∀ (t : K) (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s) = 0) (m : K → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hBm : ∀ (t : K) (y : EulerSmoothLimit.Space), (B t) y = EulerPacketCrossProduct.potentialMultiplier (m t y)) (t : K) : potentialField P B hB p hp t = EulerPacketPeriodicPotential.field P (m t) (EulerCylinderSmoothOrbit.pointField P p hp t)

The L² construction is the same actual field used in the compact Piola construction.

theorem EulerCylinderPotential.potentialPath_block_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) {ι : Type u_2} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (Rc C R D : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hD : 0 ≤ D) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hbB : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath B) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbp : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) n 0 ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (potentialPath P B p)) n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C * (P * D) * EulerGevrey.majorant R d n

Angular integration and multiplication retain the input radius and external shift.