Construction of the actual mean boundary operator by homogeneous-gradient completion and the Hilbert adjoint. No bounded inverse Laplacian on L² is assumed.

structure EulerMeanBoundary.Cutoff : Type

The only cutoff data: an actual compactly supported smooth scalar function.

• field : EulerSmoothLimit.Space → ℝ

  Underlying field of Cutoff, of type Space → ℝ.

• smooth : ContDiff ℝ (↑⊤) self.field
• compact : HasCompactSupport self.field

noncomputable def EulerMeanBoundary.curlMatrix (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Coordinate antisymmetrization of a genuine derivative.

Equations

• EulerMeanBoundary.curlMatrix A = WithLp.toLp 2 fun (i : Fin 3) => (A (EuclideanSpace.single (i + 1) 1)).ofLp (i + 2) - (A (EuclideanSpace.single (i + 2) 1)).ofLp (i + 1)

theorem EulerMeanBoundary.vectorCurl_eq_matrix (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hf : DifferentiableAt ℝ f x) : EulerMeanCutoffCurl.vectorCurl f x = curlMatrix (fderiv ℝ f x)

theorem EulerMeanBoundary.curlMatrix_add (A B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : curlMatrix (A + B) = curlMatrix A + curlMatrix B

theorem EulerMeanBoundary.curlMatrix_smul (c : ℝ) (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : curlMatrix (c • A) = c • curlMatrix A

theorem EulerMeanBoundary.vectorCurl_add (f g : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) : EulerMeanCutoffCurl.vectorCurl (f + g) = EulerMeanCutoffCurl.vectorCurl f + EulerMeanCutoffCurl.vectorCurl g

theorem EulerMeanBoundary.vectorCurl_smul (c : ℝ) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : Differentiable ℝ f) : EulerMeanCutoffCurl.vectorCurl (c • f) = c • EulerMeanCutoffCurl.vectorCurl f

theorem EulerMeanBoundary.testCurl_memLp (χ : Cutoff) (f : EulerMeanGradientTest.Test) : MeasureTheory.MemLp (EulerMeanCutoffCurl.vectorCurl fun (x : EulerSmoothLimit.Space) => χ.field x • ↑f x) 2 MeasureTheory.volume

noncomputable def EulerMeanBoundary.testCurl (χ : Cutoff) (f : EulerMeanGradientTest.Test) : ↥EulerMeanSolenoidal.L2

The literal curl of the cutoff times a compact vector test, in ordinary L².

Equations

• EulerMeanBoundary.testCurl χ f = MeasureTheory.MemLp.toLp (EulerMeanCutoffCurl.vectorCurl fun (x : EulerSmoothLimit.Space) => χ.field x • ↑f x) ⋯

theorem EulerMeanBoundary.testCurl_ae (χ : Cutoff) (f : EulerMeanGradientTest.Test) : ↑↑(testCurl χ f) =ᵐ[MeasureTheory.volume] EulerMeanCutoffCurl.vectorCurl fun (x : EulerSmoothLimit.Space) => χ.field x • ↑f x

theorem EulerMeanBoundary.testCurl_add (χ : Cutoff) (f g : EulerMeanGradientTest.Test) : testCurl χ (f + g) = testCurl χ f + testCurl χ g

theorem EulerMeanBoundary.testCurl_smul (χ : Cutoff) (c : ℝ) (f : EulerMeanGradientTest.Test) : testCurl χ (c • f) = c • testCurl χ f

noncomputable def EulerMeanBoundary.testCurlLinear (χ : Cutoff) : EulerMeanGradientTest.Test →ₗ[ℝ] ↥EulerMeanSolenoidal.L2

The actual linear cutoff-curl operation on vector tests.

Equations

• EulerMeanBoundary.testCurlLinear χ = { toFun := EulerMeanBoundary.testCurl χ, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerMeanBoundary.cutoffBound (χ : Cutoff) : ℝ

The proved cutoff-dependent bound on the homogeneous space.

Equations

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

theorem EulerMeanBoundary.cutoffBound_nonneg (χ : Cutoff) : 0 ≤ cutoffBound χ

theorem EulerMeanBoundary.testCurl_bound (χ : Cutoff) (f : EulerMeanGradientTest.Test) : ‖(testCurlLinear χ) f‖ ≤ cutoffBound χ * ‖EulerMeanGradientTest.homogeneousGradient f‖

noncomputable def EulerMeanBoundary.cutoffCurl (χ : Cutoff) : ↥EulerMeanGradientTest.homogeneousSpace →L[ℝ] ↥EulerMeanSolenoidal.L2

The bounded extension of actual cutoff-curl to the homogeneous Hilbert space.

Equations

• EulerMeanBoundary.cutoffCurl χ = (EulerMeanBoundary.testCurlLinear χ).extendOfNorm EulerMeanGradientTest.homogeneousGradient

theorem EulerMeanBoundary.cutoffCurl_on_test (χ : Cutoff) (f : EulerMeanGradientTest.Test) : (cutoffCurl χ) (EulerMeanGradientTest.homogeneousGradient f) = testCurl χ f

theorem EulerMeanBoundary.cutoffCurl_norm_le (χ : Cutoff) : ‖cutoffCurl χ‖ ≤ cutoffBound χ

noncomputable def EulerMeanBoundary.weakPotential (χ : Cutoff) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanGradientTest.homogeneousSpace

The Riesz/weak-Newtonian representation of the cutoff curl functional.

Equations

• EulerMeanBoundary.weakPotential χ = ContinuousLinearMap.adjoint (EulerMeanBoundary.cutoffCurl χ)

theorem EulerMeanBoundary.weakPotential_pairing (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) (f : EulerMeanGradientTest.Test) : inner ℝ ((weakPotential χ) z) (EulerMeanGradientTest.homogeneousGradient f) = ∫ (x : EulerSmoothLimit.Space), inner ℝ (↑↑z x) (EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => χ.field y • ↑f y) x)

The represented functional agrees exactly with the source's distributional pairing.

theorem EulerMeanBoundary.weakPotential_norm_le (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : ‖(weakPotential χ) z‖ ≤ cutoffBound χ * ‖z‖

theorem EulerMeanBoundary.weakPotential_unique (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) (u : ↥EulerMeanGradientTest.homogeneousSpace) (hu : ∀ (f : EulerMeanGradientTest.Test), inner ℝ u (EulerMeanGradientTest.homogeneousGradient f) = ∫ (x : EulerSmoothLimit.Space), inner ℝ (↑↑z x) (EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => χ.field y • ↑f y) x)) : u = (weakPotential χ) z

Compact vector tests determine the weak potential uniquely in the actual homogeneous space.

theorem EulerMeanBoundary.existsUnique_weakPotential (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : ∃! u : ↥EulerMeanGradientTest.homogeneousSpace, ∀ (f : EulerMeanGradientTest.Test), inner ℝ u (EulerMeanGradientTest.homogeneousGradient f) = ∫ (x : EulerSmoothLimit.Space), inner ℝ (↑↑z x) (EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => χ.field y • ↑f y) x)

A genuine uniquely solvable weak Poisson/Riesz problem for the cutoff-curl functional.

noncomputable def EulerMeanBoundary.boundaryOperator (χ : Cutoff) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

The actual bounded positive mean boundary operator Tχ Tχ*.

Equations

• EulerMeanBoundary.boundaryOperator χ = EulerMeanBoundary.cutoffCurl χ ∘SL EulerMeanBoundary.weakPotential χ

theorem EulerMeanBoundary.boundaryOperator_pairing (χ : Cutoff) (z w : ↥EulerMeanSolenoidal.L2) : inner ℝ ((boundaryOperator χ) z) w = inner ℝ ((weakPotential χ) z) ((weakPotential χ) w)

theorem EulerMeanBoundary.boundaryOperator_positive (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : 0 ≤ inner ℝ ((boundaryOperator χ) z) z

theorem EulerMeanBoundary.boundaryOperator_energy (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : inner ℝ ((boundaryOperator χ) z) z = ‖(weakPotential χ) z‖ ^ 2

theorem EulerMeanBoundary.boundaryOperator_norm_le (χ : Cutoff) : ‖boundaryOperator χ‖ ≤ cutoffBound χ ^ 2

theorem EulerMeanBoundary.testCurl_solenoidal (χ : Cutoff) (f : EulerMeanGradientTest.Test) : testCurl χ f ∈ EulerMeanSolenoidal.solenoidalSpace

The actual test-level cutoff curl is solenoidal.

theorem EulerMeanBoundary.cutoffCurl_solenoidal (χ : Cutoff) (u : ↥EulerMeanGradientTest.homogeneousSpace) : (cutoffCurl χ) u ∈ EulerMeanSolenoidal.solenoidalSpace

Closedness of the ordinary solenoidal space preserves the curl constraint under completion.

theorem EulerMeanBoundary.boundaryOperator_solenoidal (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : (boundaryOperator χ) z ∈ EulerMeanSolenoidal.solenoidalSpace

noncomputable def EulerMeanBoundary.supportedSpace (χ : Cutoff) : Submodule ℝ ↥EulerMeanSolenoidal.L2

Fields supported in the cutoff's closed support, defined by actual L² restriction.

Equations

• EulerMeanBoundary.supportedSpace χ = (↑(MeasureTheory.LpToLpRestrictCLM EulerSmoothLimit.Space EulerSmoothLimit.Space ℝ MeasureTheory.volume 2 (tsupport χ.field)ᶜ)).ker

theorem EulerMeanBoundary.supportedSpace_closed (χ : Cutoff) : IsClosed ↑(supportedSpace χ)

theorem EulerMeanBoundary.mem_supportedSpace_iff (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : z ∈ supportedSpace χ ↔ ↑↑z =ᵐ[MeasureTheory.volume.restrict (tsupport χ.field)ᶜ] 0

theorem EulerMeanBoundary.testCurl_supported (χ : Cutoff) (f : EulerMeanGradientTest.Test) : testCurl χ f ∈ supportedSpace χ

Multiplication by the cutoff and then curl has no support outside the cutoff support.

theorem EulerMeanBoundary.cutoffCurl_supported (χ : Cutoff) (u : ↥EulerMeanGradientTest.homogeneousSpace) : (cutoffCurl χ) u ∈ supportedSpace χ

Actual support is retained under homogeneous completion because L² restriction is continuous.

theorem EulerMeanBoundary.boundaryOperator_supported (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : (boundaryOperator χ) z ∈ supportedSpace χ

theorem EulerMeanBoundary.boundaryOperator_zero_off_support (χ : Cutoff) (z : ↥EulerMeanSolenoidal.L2) : ↑↑((boundaryOperator χ) z) =ᵐ[MeasureTheory.volume.restrict (tsupport χ.field)ᶜ] 0

The constructed mean boundary output vanishes almost everywhere outside the cutoff support.

theorem EulerMeanBoundary.boundaryOperator_symmetric (χ : Cutoff) (z w : ↥EulerMeanSolenoidal.L2) : inner ℝ ((boundaryOperator χ) z) w = inner ℝ z ((boundaryOperator χ) w)

Symmetry follows from the actual Hilbert-adjoint construction.