Reflection covariance of the actual cutoff-curl/Riesz boundary operator. On homogeneous gradient tensors reflection is componentwise pullback. It is represented by the reflected vector test -φ(-x), so both curl signs cancel. No covariance or parity of an inverse operator is assumed.

def EulerMeanBoundary.Cutoff.reflect (χ : Cutoff) : Cutoff

Reflect, given by ⟨fun x => χ.field (-x), χ.smooth.comp contDiff_id.neg, χ.compact.comp_homeomorph (Homeomorph.neg Space)⟩.

Equations

• χ.reflect = { field := fun (x : EulerSmoothLimit.Space) => χ.field (-x), smooth := ⋯, compact := ⋯ }

theorem EulerMeanBoundary.Cutoff.reflect_reflect (χ : Cutoff) : χ.reflect.reflect = χ

theorem EulerMeanBoundary.Cutoff.reflect_eq_of_even (χ : Cutoff) (hχ : ∀ (x : EulerSmoothLimit.Space), χ.field (-x) = χ.field x) : χ.reflect = χ

noncomputable def EulerMeanBoundary.l2ReflectionEquiv : ↥EulerMeanSolenoidal.L2 ≃ₗᵢ[ℝ] ↥EulerMeanSolenoidal.L2

L2 reflection equiv, given by LinearIsometryEquiv.ofSurjective reflection (fun u => ⟨reflection u, reflection_involutive u⟩).

Equations

• EulerMeanBoundary.l2ReflectionEquiv = LinearIsometryEquiv.ofSurjective EulerMeanSolenoidal.reflection EulerMeanBoundary.l2ReflectionEquiv._proof_5

noncomputable def EulerMeanBoundary.gradientReflection : EulerMeanGradientTest.GradientTensor ≃ₗᵢ[ℝ] EulerMeanGradientTest.GradientTensor

Gradient reflection, given by LinearIsometryEquiv.piLpCongrRight 2 (fun _ : Fin 3 => l2ReflectionEquiv).

Equations

• EulerMeanBoundary.gradientReflection = LinearIsometryEquiv.piLpCongrRight 2 fun (x : Fin 3) => EulerMeanBoundary.l2ReflectionEquiv

theorem EulerMeanBoundary.gradientReflection_apply (G : EulerMeanGradientTest.GradientTensor) (i : Fin 3) : (gradientReflection G).ofLp i = EulerMeanSolenoidal.reflection (G.ofLp i)

theorem EulerMeanBoundary.gradientReflection_involutive (G : EulerMeanGradientTest.GradientTensor) : gradientReflection (gradientReflection G) = G

def EulerMeanBoundary.reflectedTest (f : EulerMeanGradientTest.Test) : EulerMeanGradientTest.Test

Reflected test, given by ⟨fun x => -(f : Space → Space) (-x), (f.smooth.comp contDiff_id.neg).neg, (f.compact.comp_homeomorph (Homeomorph.neg Space)).neg⟩.

Equations

• EulerMeanBoundary.reflectedTest f = ⟨fun (x : EulerSmoothLimit.Space) => -↑f (-x), ⋯⟩

theorem EulerMeanBoundary.testGradient_reflected (f : EulerMeanGradientTest.Test) : EulerMeanGradientTest.testGradient (reflectedTest f) = gradientReflection (EulerMeanGradientTest.testGradient f)

theorem EulerMeanBoundary.gradientReflection_homogeneous (u : ↥EulerMeanGradientTest.homogeneousSpace) : gradientReflection ↑u ∈ EulerMeanGradientTest.homogeneousSpace

noncomputable def EulerMeanBoundary.homogeneousReflection : ↥EulerMeanGradientTest.homogeneousSpace →ₗᵢ[ℝ] ↥EulerMeanGradientTest.homogeneousSpace

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

Equations

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

theorem EulerMeanBoundary.homogeneousReflection_coe (u : ↥EulerMeanGradientTest.homogeneousSpace) : ↑(homogeneousReflection u) = gradientReflection ↑u

theorem EulerMeanBoundary.homogeneousReflection_involutive (u : ↥EulerMeanGradientTest.homogeneousSpace) : homogeneousReflection (homogeneousReflection u) = u

theorem EulerMeanBoundary.homogeneousReflection_test (f : EulerMeanGradientTest.Test) : homogeneousReflection (EulerMeanGradientTest.homogeneousGradient f) = EulerMeanGradientTest.homogeneousGradient (reflectedTest f)

theorem EulerMeanBoundary.homogeneousReflection_inner_shift (u v : ↥EulerMeanGradientTest.homogeneousSpace) : inner ℝ (homogeneousReflection u) v = inner ℝ u (homogeneousReflection v)

theorem EulerMeanBoundary.vectorCurl_neg_reflect (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : Differentiable ℝ f) (x : EulerSmoothLimit.Space) : EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => -f (-y)) x = EulerMeanCutoffCurl.vectorCurl f (-x)

theorem EulerMeanBoundary.testCurl_reflected (χ : Cutoff) (f : EulerMeanGradientTest.Test) : EulerMeanSolenoidal.reflection (testCurl χ f) = testCurl χ.reflect (reflectedTest f)

theorem EulerMeanBoundary.cutoffCurl_reflection (χ : Cutoff) (u : ↥EulerMeanGradientTest.homogeneousSpace) : EulerMeanSolenoidal.reflection ((cutoffCurl χ) u) = (cutoffCurl χ.reflect) (homogeneousReflection u)

Covariance is proved first on real compact tests, then by density.

theorem EulerMeanBoundary.weakPotential_reflection (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : homogeneousReflection ((weakPotential χ) z) = (weakPotential χ.reflect) (EulerMeanSolenoidal.reflection z)

The actual Riesz solution, rather than an assumed inverse, respects reflection.

theorem EulerMeanBoundary.mixedBoundaryOperator_reflection (χ ψ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : EulerMeanSolenoidal.reflection ((mixedBoundaryOperator χ ψ) z) = (mixedBoundaryOperator χ.reflect ψ.reflect) (EulerMeanSolenoidal.reflection z)

theorem EulerMeanBoundary.boundaryOperator_reflection (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : EulerMeanSolenoidal.reflection ((boundaryOperator χ) z) = (boundaryOperator χ.reflect) (EulerMeanSolenoidal.reflection z)

theorem EulerMeanBoundary.boundaryOperator_reflection_of_even (χ : Cutoff) (hχ : ∀ (x : EulerSmoothLimit.Space), χ.field (-x) = χ.field x) (z : ↥EulerMeanSolenoidal.L2) : EulerMeanSolenoidal.reflection ((boundaryOperator χ) z) = (boundaryOperator χ) (EulerMeanSolenoidal.reflection z)

theorem EulerMeanBoundary.scaledBoundaryOperator_reflection (ℓ : ℝ) (hℓ : 0 < ℓ) (z : ↥EulerMeanSolenoidal.L2) : EulerMeanSolenoidal.reflection ((boundaryOperator (scaledCutoff ℓ hℓ)) z) = (boundaryOperator (scaledCutoff ℓ hℓ)) (EulerMeanSolenoidal.reflection z)

The concrete source boundary operator commutes with ordinary spatial reflection.