The genuine commuting coordinate derivatives and bounded Laplacian on the complete Sobolev scale.

theorem EulerSobolevLaplacian.derivative_value_ae (period : ℝ) [Fact (0 < period)] {q : ℕ} (i : Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : ↑↑(EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period q i) u)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) g

A genuine Sobolev coordinate derivative agrees with every smooth representative's classical derivative.

theorem EulerSobolevLaplacian.derivative_commute_smooth (period : ℝ) [Fact (0 < period)] {q : ℕ} (i j : Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 2))) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : (EulerCylinderSobolevSpace.derivativeOperator period q i) ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) j) u) = (EulerCylinderSobolevSpace.derivativeOperator period q j) ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i) u)

Coordinate derivatives commute on every genuinely smooth represented Sobolev field.

theorem EulerSobolevLaplacian.derivative_commute (period : ℝ) [Fact (0 < period)] {q : ℕ} (i j : Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 2))) : (EulerCylinderSobolevSpace.derivativeOperator period q i) ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) j) u) = (EulerCylinderSobolevSpace.derivativeOperator period q j) ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i) u)

Strong coordinate derivatives commute for every actual finite Sobolev field, by genuine smooth density.

noncomputable def EulerSobolevLaplacian.laplacianOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 2)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The actual Laplacian as a bounded map H^(q+2)→Hq.

Equations

• EulerSobolevLaplacian.laplacianOperator period q = ∑ i : Fin 4, EulerCylinderSobolevSpace.derivativeOperator period q i ∘SL EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i

theorem EulerSobolevLaplacian.laplacianOperator_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 2))) : (laplacianOperator period q) u = ∑ i : Fin 4, (EulerCylinderSobolevSpace.derivativeOperator period q i) ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i) u)

The bounded Laplacian is the sum of the genuine pure second derivatives.

theorem EulerSobolevLaplacian.laplacianOperator_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 2))) : EulerCylinderSobolevSpace.value period ((laplacianOperator period q) u) = (EulerSobolevHeatGenerator.laplacianEvaluation period (q + 2) ⋯) u

Its L² field is exactly the previously proved actual Laplacian evaluation.

theorem EulerSobolevLaplacian.laplacianOperator_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 2))) : ‖(laplacianOperator period q) u‖ ≤ 4 * ‖u‖

The actual complete-Sobolev Laplacian has norm at most four.

theorem EulerSobolevLaplacian.laplacian_derivative (period : ℝ) [Fact (0 < period)] {q : ℕ} (i : Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 3))) : (laplacianOperator period q) ((EulerCylinderSobolevSpace.derivativeOperator period (q + 2) i) u) = (EulerCylinderSobolevSpace.derivativeOperator period q i) ((laplacianOperator period (q + 1)) u)

The actual Laplacian commutes with every coordinate derivative.