Actual spatial reflection on ordinary R³ L². Reflection preserves the closed gradient and solenoidal spaces and commutes with the genuine Helmholtz projection. The scalar test is reflected with a minus sign so its gradient has the same pullback as an ordinary vector field.

theorem EulerMeanSolenoidal.measurePreserving_reflection : MeasureTheory.MeasurePreserving (fun (x : EulerSmoothLimit.Space) => -x) MeasureTheory.volume MeasureTheory.volume

noncomputable def EulerMeanSolenoidal.reflection : ↥L2 →ₗᵢ[ℝ] ↥L2

Reflection, given by Lp.compMeasurePreservingₗᵢ ℝ (fun x : Space => -x) measurePreserving_reflection.

Equations

• EulerMeanSolenoidal.reflection = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (x : EulerSmoothLimit.Space) => -x) EulerMeanSolenoidal.measurePreserving_reflection

theorem EulerMeanSolenoidal.reflection_ae (u : ↥L2) : ↑↑(reflection u) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => ↑↑u (-x)

@[simp]

theorem EulerMeanSolenoidal.reflection_involutive (u : ↥L2) : reflection (reflection u) = u

theorem EulerMeanSolenoidal.reflection_norm (u : ↥L2) : ‖reflection u‖ = ‖u‖

theorem EulerMeanSolenoidal.reflection_inner_shift (u v : ↥L2) : inner ℝ (reflection u) v = inner ℝ u (reflection v)

theorem EulerMeanSolenoidal.fderiv_neg_reflect {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerSmoothLimit.Space → F) (hf : Differentiable ℝ f) (x : EulerSmoothLimit.Space) : fderiv ℝ (fun (y : EulerSmoothLimit.Space) => -f (-y)) x = fderiv ℝ f (-x)

The two signs in the derivative of -f(-x) cancel.

theorem EulerMeanSolenoidal.gradient_neg_reflect (φ : EulerSmoothLimit.Space → ℝ) (hφ : Differentiable ℝ φ) (x : EulerSmoothLimit.Space) : gradient (fun (y : EulerSmoothLimit.Space) => -φ (-y)) x = gradient φ (-x)

theorem EulerMeanSolenoidal.reflected_generator {g : ↥L2} (hg : g ∈ gradientGenerators) : reflection g ∈ gradientGenerators

theorem EulerMeanSolenoidal.reflection_gradient_mem {g : ↥L2} (hg : g ∈ gradientSpace) : reflection g ∈ gradientSpace

theorem EulerMeanSolenoidal.reflection_solenoidal_mem {u : ↥L2} (hu : u ∈ solenoidalSpace) : reflection u ∈ solenoidalSpace

theorem EulerMeanSolenoidal.solenoidalSpace_map_reflection : Submodule.map reflection.toLinearMap solenoidalSpace = solenoidalSpace

theorem EulerMeanSolenoidal.solenoidalProjection_reflection (u : ↥L2) : reflection (solenoidalProjection u) = solenoidalProjection (reflection u)

The actual ordinary Helmholtz projection commutes with reflection.

theorem EulerMeanSolenoidal.reflection_translation (a : EulerSmoothLimit.Space) (u : ↥L2) : reflection ((translation a) u) = (translation (-a)) (reflection u)