The actual joint spatial and angular reflection on cylinder L² fields.

theorem EulerCylinderReflection.measurePreserving_reflection (period : ℝ) [Fact (0 < period)] : MeasureTheory.MeasurePreserving (fun (x : EulerLiftedGradientSpace.LiftDomain period) => -x) (EulerLiftedGradientSpace.liftMeasure period) (EulerLiftedGradientSpace.liftMeasure period)

Joint negation of the spatial and periodic coordinates preserves cylinder measure.

noncomputable def EulerCylinderReflection.reflection (period : ℝ) [Fact (0 < period)] : ↥(EulerLiftedGradientSpace.LiftL2 period) →ₗᵢ[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Pullback by joint spatial and angular reflection, as an actual L² isometry.

Equations

• EulerCylinderReflection.reflection period = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (x : EulerLiftedGradientSpace.LiftDomain period) => -x) ⋯

theorem EulerCylinderReflection.reflection_ae (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↑↑((reflection period) f) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => ↑↑f (-x)

The L² reflection is represented by literal composition with negation.

@[simp]

theorem EulerCylinderReflection.reflection_involutive (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (reflection period) ((reflection period) f) = f

Reflecting twice is the identity on the actual L² field.

theorem EulerCylinderReflection.reflection_norm (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖(reflection period) f‖ = ‖f‖

Reflection preserves the actual L² norm.

theorem EulerCylinderReflection.reflection_translation (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (reflection period) ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period (-a)) ((reflection period) f)

Reflection reverses translations in every spatial or angular direction.

@[simp]

theorem EulerCylinderReflection.translationPath_neg (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : EulerPressureSpatialRegularity.translationPath period a (-t) = -EulerPressureSpatialRegularity.translationPath period a t

Negating a translation parameter negates its point on the cylinder.

theorem EulerCylinderReflection.reflection_hasDerivAt (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (h : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f) g 0) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) ((reflection period) f)) (-(reflection period) g) 0

Strong translation derivatives reverse sign under actual reflection.

def EulerCylinderReflection.reflectedTest (period : ℝ) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) : EulerLiftedGradientSpace.LiftDomain period → ℝ

A scalar test pulled back by joint negation.

Equations

• EulerCylinderReflection.reflectedTest period φ x = φ (-x)

theorem EulerCylinderReflection.localLift_reflected (period : ℝ) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.localLift period (reflectedTest period φ) x = fun (h : EulerLiftedGradientSpace.LiftTangent) => EulerLiftedGradientSpace.localLift period φ (-x) (-h)

In covering coordinates reflection is exactly negation of the increment.

theorem EulerCylinderReflection.smoothCompactTest_reflected (period : ℝ) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφ : HasCompactSupport φ ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift period φ x)) : HasCompactSupport (reflectedTest period φ) ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift period (reflectedTest period φ) x)

Reflection preserves the class of smooth compact scalar tests.

theorem EulerCylinderReflection.liftedGradient_reflected (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift period φ x)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.liftedGradient period κ m (reflectedTest period φ) x = -EulerLiftedGradientSpace.liftedGradient period κ m φ (-x)

The actual lifted gradient reverses parity under joint reflection.