The actual translation action on homogeneous gradients and localized Newtonian operators.

noncomputable def EulerMeanBoundary.l2TranslationEquiv (a : EulerSmoothLimit.Space) : ↥EulerMeanSolenoidal.L2 ≃ₗᵢ[ℝ] ↥EulerMeanSolenoidal.L2

L2 translation equiv, constructed using LinearIsometryEquiv.ofSurjective.

Equations

• EulerMeanBoundary.l2TranslationEquiv a = LinearIsometryEquiv.ofSurjective (EulerMeanSolenoidal.translation a) ⋯

theorem EulerMeanBoundary.l2TranslationEquiv_apply (a : EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) : (l2TranslationEquiv a) u = (EulerMeanSolenoidal.translation a) u

noncomputable def EulerMeanBoundary.gradientTranslation (a : EulerSmoothLimit.Space) : EulerMeanGradientTest.GradientTensor ≃ₗᵢ[ℝ] EulerMeanGradientTest.GradientTensor

Gradient translation, given by LinearIsometryEquiv.piLpCongrRight 2 (fun _ : Fin 3 => l2TranslationEquiv a).

Equations

• EulerMeanBoundary.gradientTranslation a = LinearIsometryEquiv.piLpCongrRight 2 fun (x : Fin 3) => EulerMeanBoundary.l2TranslationEquiv a

theorem EulerMeanBoundary.gradientTranslation_apply (a : EulerSmoothLimit.Space) (G : EulerMeanGradientTest.GradientTensor) (i : Fin 3) : ((gradientTranslation a) G).ofLp i = (EulerMeanSolenoidal.translation a) (G.ofLp i)

theorem EulerMeanBoundary.gradientTranslation_add (a b : EulerSmoothLimit.Space) (G : EulerMeanGradientTest.GradientTensor) : (gradientTranslation a) ((gradientTranslation b) G) = (gradientTranslation (a + b)) G

theorem EulerMeanBoundary.gradientTranslation_zero (G : EulerMeanGradientTest.GradientTensor) : (gradientTranslation 0) G = G

def EulerMeanBoundary.translatedTest (a : EulerSmoothLimit.Space) (f : EulerMeanGradientTest.Test) : EulerMeanGradientTest.Test

Translated test as an element of Test.

Equations

• EulerMeanBoundary.translatedTest a f = ⟨fun (x : EulerSmoothLimit.Space) => ↑f (x + a), ⋯⟩

theorem EulerMeanBoundary.testGradient_translated (a : EulerSmoothLimit.Space) (f : EulerMeanGradientTest.Test) : EulerMeanGradientTest.testGradient (translatedTest a f) = (gradientTranslation a) (EulerMeanGradientTest.testGradient f)

theorem EulerMeanBoundary.gradientTranslation_homogeneous (a : EulerSmoothLimit.Space) (u : ↥EulerMeanGradientTest.homogeneousSpace) : (gradientTranslation a) ↑u ∈ EulerMeanGradientTest.homogeneousSpace

noncomputable def EulerMeanBoundary.homogeneousTranslation (a : EulerSmoothLimit.Space) : ↥EulerMeanGradientTest.homogeneousSpace →ₗᵢ[ℝ] ↥EulerMeanGradientTest.homogeneousSpace

Homogeneous translation, bundling toFun, map_add, map_smul, norm_map.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerMeanBoundary.homogeneousTranslation_coe (a : EulerSmoothLimit.Space) (u : ↥EulerMeanGradientTest.homogeneousSpace) : ↑((homogeneousTranslation a) u) = (gradientTranslation a) ↑u

theorem EulerMeanBoundary.homogeneousTranslation_add (a b : EulerSmoothLimit.Space) (u : ↥EulerMeanGradientTest.homogeneousSpace) : (homogeneousTranslation a) ((homogeneousTranslation b) u) = (homogeneousTranslation (a + b)) u

theorem EulerMeanBoundary.homogeneousTranslation_zero (u : ↥EulerMeanGradientTest.homogeneousSpace) : (homogeneousTranslation 0) u = u

theorem EulerMeanBoundary.homogeneousTranslation_test (a : EulerSmoothLimit.Space) (f : EulerMeanGradientTest.Test) : (homogeneousTranslation a) (EulerMeanGradientTest.homogeneousGradient f) = EulerMeanGradientTest.homogeneousGradient (translatedTest a f)

theorem EulerMeanBoundary.homogeneousTranslation_inner_shift (a : EulerSmoothLimit.Space) (u v : ↥EulerMeanGradientTest.homogeneousSpace) : inner ℝ ((homogeneousTranslation a) u) v = inner ℝ u ((homogeneousTranslation (-a)) v)

theorem EulerMeanBoundary.vectorCurl_translated (a : EulerSmoothLimit.Space) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => f (y + a)) x = EulerMeanCutoffCurl.vectorCurl f (x + a)

theorem EulerMeanBoundary.testCurl_translated (a : EulerSmoothLimit.Space) (χ : Cutoff) (f : EulerMeanGradientTest.Test) : (EulerMeanSolenoidal.translation a) (testCurl χ f) = testCurl (χ.translate a) (translatedTest a f)

theorem EulerMeanBoundary.cutoffCurl_translation (a : EulerSmoothLimit.Space) (χ : Cutoff) (u : ↥EulerMeanGradientTest.homogeneousSpace) : (EulerMeanSolenoidal.translation a) ((cutoffCurl χ) u) = (cutoffCurl (χ.translate a)) ((homogeneousTranslation a) u)

Translating the output translates both the cutoff and the homogeneous potential.

theorem EulerMeanBoundary.weakPotential_translation (a : EulerSmoothLimit.Space) (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : (homogeneousTranslation a) ((weakPotential χ) z) = (weakPotential (χ.translate a)) ((EulerMeanSolenoidal.translation a) z)

The actual weak inverse respects spatial translation of its cutoff and forcing.

theorem EulerMeanBoundary.mixedBoundaryOperator_translation (a : EulerSmoothLimit.Space) (χ ψ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : (EulerMeanSolenoidal.translation a) ((mixedBoundaryOperator χ ψ) z) = (mixedBoundaryOperator (χ.translate a) (ψ.translate a)) ((EulerMeanSolenoidal.translation a) z)

noncomputable def EulerMeanBoundary.translationCommutator (a : EulerSmoothLimit.Space) (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

The genuine spatial translation commutator on ordinary L².

Equations

• EulerMeanBoundary.translationCommutator a A = (EulerMeanSolenoidal.translation a).toContinuousLinearMap ∘SL A - A ∘SL (EulerMeanSolenoidal.translation a).toContinuousLinearMap

theorem EulerMeanBoundary.mixedBoundaryOperator_translationCommutator (a : EulerSmoothLimit.Space) (χ ψ : Cutoff) : translationCommutator a (mixedBoundaryOperator χ ψ) = (mixedBoundaryOperator ((χ.translate a).sub χ) (ψ.translate a) + mixedBoundaryOperator χ ((ψ.translate a).sub ψ)) ∘SL (EulerMeanSolenoidal.translation a).toContinuousLinearMap

Both cutoff positions, and only those positions, contribute to the spatial commutator.

theorem EulerMeanBoundary.mixedBoundaryOperator_translationCommutator_norm_le (a : EulerSmoothLimit.Space) (χ ψ : Cutoff) : ‖translationCommutator a (mixedBoundaryOperator χ ψ)‖ ≤ cutoffBound ((χ.translate a).sub χ) * cutoffBound (ψ.translate a) + cutoffBound χ * cutoffBound ((ψ.translate a).sub ψ)