Translation invariance of the ordinary solenoidal projection

The nonoscillating inverse uses spatial difference quotients. These act on the actual R³ L² space, preserve its weak divergence constraint, and commute with the orthogonal solenoidal projection.

noncomputable def EulerMeanSolenoidal.translation (a : EulerSmoothLimit.Space) : ↥L2 →ₗᵢ[ℝ] ↥L2

Translation, given by Lp.compMeasurePreservingₗᵢ ℝ (fun x : Space => x + a) (measurePreserving_add_right (volume : Measure Space) a).

Equations

• EulerMeanSolenoidal.translation a = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (x : EulerSmoothLimit.Space) => x + a) ⋯

theorem EulerMeanSolenoidal.translation_ae (a : EulerSmoothLimit.Space) (u : ↥L2) : ↑↑((translation a) u) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => ↑↑u (x + a)

theorem EulerMeanSolenoidal.translation_add (a b : EulerSmoothLimit.Space) (u : ↥L2) : (translation a) ((translation b) u) = (translation (a + b)) u

@[simp]

theorem EulerMeanSolenoidal.translation_zero (u : ↥L2) : (translation 0) u = u

theorem EulerMeanSolenoidal.gradient_translated (a : EulerSmoothLimit.Space) (φ : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) : gradient (fun (y : EulerSmoothLimit.Space) => φ (y + a)) x = gradient φ (x + a)

theorem EulerMeanSolenoidal.translated_generator (a : EulerSmoothLimit.Space) {g : ↥L2} (hg : g ∈ gradientGenerators) : (translation a) g ∈ gradientGenerators

theorem EulerMeanSolenoidal.translation_gradient_mem (a : EulerSmoothLimit.Space) {g : ↥L2} (hg : g ∈ gradientSpace) : (translation a) g ∈ gradientSpace

theorem EulerMeanSolenoidal.translation_solenoidal_mem (a : EulerSmoothLimit.Space) {u : ↥L2} (hu : u ∈ solenoidalSpace) : (translation a) u ∈ solenoidalSpace

theorem EulerMeanSolenoidal.solenoidalSpace_map_translation (a : EulerSmoothLimit.Space) : Submodule.map (translation a).toLinearMap solenoidalSpace = solenoidalSpace

theorem EulerMeanSolenoidal.solenoidalProjection_translation (a : EulerSmoothLimit.Space) (u : ↥L2) : (translation a) (solenoidalProjection u) = solenoidalProjection ((translation a) u)

Ordinary Helmholtz projection commutes with every spatial translation.