A genuine bounded angular primitive on the full cylinder L² space.

def EulerCylinderAnglePrimitive.angleShift (P s : ℝ) : EulerLiftedGradientSpace.LiftDomain P

Angle shift, given by (0,(s : AddCircle P)).

Equations

• EulerCylinderAnglePrimitive.angleShift P s = (0, ↑s)

theorem EulerCylinderAnglePrimitive.angleShift_continuous (P : ℝ) : Continuous (angleShift P)

noncomputable def EulerCylinderAnglePrimitive.kernelCurve (P : ℝ) [Fact (0 < P)] (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) (s : ℝ) : ↥(EulerLiftedGradientSpace.LiftL2 P)

Kernel curve, given by s • translation P (angleShift P s) u.

Equations

• EulerCylinderAnglePrimitive.kernelCurve P u s = s • (EulerLiftedGradientSpace.translation P (EulerCylinderAnglePrimitive.angleShift P s)) u

theorem EulerCylinderAnglePrimitive.kernelCurve_continuous (P : ℝ) [Fact (0 < P)] (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) : Continuous (kernelCurve P u)

noncomputable def EulerCylinderAnglePrimitive.kernelIntegral (P : ℝ) [Fact (0 < P)] (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) : ↥(EulerLiftedGradientSpace.LiftL2 P)

Kernel integral, given by P⁻¹ • (∫ s in (0 : ℝ)..P, kernelCurve P u s).

Equations

• EulerCylinderAnglePrimitive.kernelIntegral P u = P⁻¹ • ∫ (s : ℝ) in 0..P, EulerCylinderAnglePrimitive.kernelCurve P u s

theorem EulerCylinderAnglePrimitive.kernelIntegral_add (P : ℝ) [Fact (0 < P)] (u v : ↥(EulerLiftedGradientSpace.LiftL2 P)) : kernelIntegral P (u + v) = kernelIntegral P u + kernelIntegral P v

theorem EulerCylinderAnglePrimitive.kernelIntegral_smul (P : ℝ) [Fact (0 < P)] (r : ℝ) (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) : kernelIntegral P (r • u) = r • kernelIntegral P u

theorem EulerCylinderAnglePrimitive.kernelIntegral_norm (P : ℝ) [Fact (0 < P)] (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) : ‖kernelIntegral P u‖ ≤ P * ‖u‖

noncomputable def EulerCylinderAnglePrimitive.primitiveLinear (P : ℝ) [Fact (0 < P)] : ↥(EulerLiftedGradientSpace.LiftL2 P) →ₗ[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 P)

Primitive linear, bundling toFun, map_add, map_smul.

Equations

• EulerCylinderAnglePrimitive.primitiveLinear P = { toFun := EulerCylinderAnglePrimitive.kernelIntegral P, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerCylinderAnglePrimitive.primitive (P : ℝ) [Fact (0 < P)] : ↥(EulerLiftedGradientSpace.LiftL2 P) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 P)

Primitive, given by (primitiveLinear P).mkContinuous P (kernelIntegral_norm P).

Equations

• EulerCylinderAnglePrimitive.primitive P = (EulerCylinderAnglePrimitive.primitiveLinear P).mkContinuous P ⋯

@[simp]

theorem EulerCylinderAnglePrimitive.primitive_apply (P : ℝ) [Fact (0 < P)] (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) : (primitive P) u = kernelIntegral P u

theorem EulerCylinderAnglePrimitive.primitive_norm (P : ℝ) [Fact (0 < P)] : ‖primitive P‖ ≤ P

theorem EulerCylinderAnglePrimitive.primitive_translation (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftDomain P) (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) : (primitive P) ((EulerLiftedGradientSpace.translation P a) u) = (EulerLiftedGradientSpace.translation P a) ((primitive P) u)

The actual angular operator commutes with all spatial and angular translations.

noncomputable def EulerCylinderAnglePrimitive.sobolevPrimitive (P : ℝ) [Fact (0 < P)] (q : ℕ) : ↥(EulerCylinderSobolevSpace.SobolevSpace P q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace P q)

This same operator acts on every genuine Sobolev derivative coordinate.

Equations

• EulerCylinderAnglePrimitive.sobolevPrimitive P q = EulerCylinderSobolevSpace.liftOperator P q (EulerCylinderAnglePrimitive.primitive P) ⋯

theorem EulerCylinderAnglePrimitive.sobolevPrimitive_norm (P : ℝ) [Fact (0 < P)] (q : ℕ) : ‖sobolevPrimitive P q‖ ≤ P