The vector potential Q of a tangent, mean-zero, periodic high coefficient.

Uniform bounds for the actual mean-zero angular primitive.

theorem EulerAngleMeanZeroPrimitive.rawPrimitive_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (P M : ℝ) (hM : 0 ≤ M) (f : ℝ → E) (hf : ∀ θ ∈ Set.Icc 0 P, ‖f θ‖ ≤ M) (θ : ℝ) (hθ : θ ∈ Set.Icc 0 P) : ‖rawPrimitive f θ‖ ≤ M * P

theorem EulerAngleMeanZeroPrimitive.primitive_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (P M : ℝ) (hP : 0 < P) (hM : 0 ≤ M) (f : ℝ → E) (hf : ∀ θ ∈ Set.Icc 0 P, ‖f θ‖ ≤ M) (θ : ℝ) (hθ : θ ∈ Set.Icc 0 P) : ‖primitive P f θ‖ ≤ 2 * P * M

noncomputable def EulerPacketAngularPotential.potential (P : ℝ) (m : EulerSmoothLimit.Space) (A : ℝ → EulerSmoothLimit.Space) : ℝ → EulerSmoothLimit.Space

Potential, given by primitive P (fun θ => potentialMultiplier m (A θ)).

Equations

• EulerPacketAngularPotential.potential P m A = EulerAngleMeanZeroPrimitive.primitive P fun (θ : ℝ) => (EulerPacketCrossProduct.potentialMultiplier m) (A θ)

theorem EulerPacketAngularPotential.potential_hasDerivAt (P : ℝ) (m : EulerSmoothLimit.Space) (A : ℝ → EulerSmoothLimit.Space) (hA : Continuous A) (θ : ℝ) : HasDerivAt (potential P m A) ((EulerPacketCrossProduct.potentialMultiplier m) (A θ)) θ

theorem EulerPacketAngularPotential.cross_deriv_potential (P : ℝ) (m : EulerSmoothLimit.Space) (hm : m ≠ 0) (A : ℝ → EulerSmoothLimit.Space) (hA : Continuous A) (htan : ∀ (θ : ℝ), inner ℝ m (A θ) = 0) (θ : ℝ) : EulerPacketCrossProduct.cross m (deriv (potential P m A) θ) = A θ

The actual angular derivative recovers A after crossing with m.

theorem EulerPacketAngularPotential.potential_periodic (P : ℝ) (m : EulerSmoothLimit.Space) (A : ℝ → EulerSmoothLimit.Space) (hA : Continuous A) (hper : Function.Periodic A P) (hmean : ∫ (θ : ℝ) in 0..P, A θ = 0) : Function.Periodic (potential P m A) P

theorem EulerPacketAngularPotential.potential_mean_zero (P : ℝ) (hP : P ≠ 0) (m : EulerSmoothLimit.Space) (A : ℝ → EulerSmoothLimit.Space) (hA : Continuous A) : ∫ (θ : ℝ) in 0..P, potential P m A θ = 0

theorem EulerPacketAngularPotential.potential_zero (P : ℝ) (m : EulerSmoothLimit.Space) : (potential P m fun (x : ℝ) => 0) = fun (x : ℝ) => 0

theorem EulerPacketAngularPotential.potential_vanishes (P : ℝ) (m : EulerSmoothLimit.Space) (A : ℝ → EulerSmoothLimit.Space) (hA : ∀ (θ : ℝ), A θ = 0) (θ : ℝ) : potential P m A θ = 0

The angular construction creates no values at labels where the whole input vanishes.

theorem EulerPacketAngularPotential.potential_bound (P M : ℝ) (hP : 0 < P) (hM : 0 ≤ M) (m : EulerSmoothLimit.Space) (A : ℝ → EulerSmoothLimit.Space) (hA : ∀ θ ∈ Set.Icc 0 P, ‖A θ‖ ≤ M) (θ : ℝ) (hθ : θ ∈ Set.Icc 0 P) : ‖potential P m A θ‖ ≤ 2 * P * (‖EulerPacketCrossProduct.potentialMultiplier m‖ * M)