The literal angular vector potential on the periodic cylinder.

theorem EulerPacketPeriodicPotential.liftIco_eq_periodicLift (P : ℝ) [Fact (0 < P)] {E : Type u_1} (f : ℝ → E) (hf : Function.Periodic f P) : AddCircle.liftIco P 0 f = hf.lift

noncomputable def EulerPacketPeriodicPotential.field (P : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerSmoothLimit.Space

Field, given by AddCircle.liftIco P 0 (potential P (m x.1) (fun θ => A (x.1,(θ : AddCircle P)))) x.2.

Equations

• EulerPacketPeriodicPotential.field P m A x = AddCircle.liftIco P 0 (EulerPacketAngularPotential.potential P (m x.1) fun (θ : ℝ) => A (x.1, ↑θ)) x.2

theorem EulerPacketPeriodicPotential.angle_periodic (P : ℝ) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (y : EulerSmoothLimit.Space) : Function.Periodic (fun (θ : ℝ) => A (y, ↑θ)) P

theorem EulerPacketPeriodicPotential.field_cover (P : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hA : Continuous A) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (θ : ℝ) in 0..P, A (y, ↑θ) = 0) (z : EulerLiftedGradientSpace.LiftTangent) : field P m A (EulerLiftedGradientSpace.coveringMap P z) = EulerPacketPiola.coveringPotential P m (EulerMetricTransport.localFieldLift P A 0) z

theorem EulerPacketPeriodicPotential.field_smooth (P : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hm : ContDiff ℝ (↑⊤) m) (hnz : ∀ (y : EulerSmoothLimit.Space), m y ≠ 0) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P A x)) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (θ : ℝ) in 0..P, A (y, ↑θ) = 0) (x : EulerLiftedGradientSpace.LiftDomain P) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (field P m A) x)

theorem EulerPacketPeriodicPotential.field_continuous (P : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hm : ContDiff ℝ (↑⊤) m) (hnz : ∀ (y : EulerSmoothLimit.Space), m y ≠ 0) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P A x)) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (θ : ℝ) in 0..P, A (y, ↑θ) = 0) : Continuous (field P m A)

theorem EulerPacketPeriodicPotential.field_vanishes (P : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (y : EulerSmoothLimit.Space) (hy : ∀ (θ : AddCircle P), A (y, θ) = 0) (θ : AddCircle P) : field P m A (y, θ) = 0

theorem EulerPacketPeriodicPotential.field_compact (P : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hA : HasCompactSupport A) : HasCompactSupport (field P m A)

Angular integration preserves the compact spatial support of the input.

theorem EulerPacketPeriodicPotential.field_angle_derivative (P : ℝ) [Fact (0 < P)] (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hm : ContDiff ℝ (↑⊤) m) (hnz : ∀ (y : EulerSmoothLimit.Space), m y ≠ 0) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P A x)) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (θ : ℝ) in 0..P, A (y, ↑θ) = 0) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerTransportDerivatives.fieldDerivative P (0, 1) (field P m A) x = (EulerPacketCrossProduct.potentialMultiplier (m x.1)) (A x)

The actual angular derivative of the genuine periodic potential.