The localized weak Newtonian potential produces the source's actual curl field w. Its complement is distributionally harmonic wherever the cutoff is one.

Classical integration by parts and its extension to the actual homogeneous gradient space.

The ordinary curl as a bounded antisymmetrization of actual L² gradient tensors.

noncomputable def EulerMeanCurlTensor.coordinateInsertion (i j : Fin 3) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Coordinate insertion, given by (EuclideanSpace.proj j).smulRight (EuclideanSpace.single i 1).

Equations

• EulerMeanCurlTensor.coordinateInsertion i j = ContinuousLinearMap.smulRight (EuclideanSpace.proj j) (EuclideanSpace.single i 1)

theorem EulerMeanCurlTensor.coordinateInsertion_norm_le (i j : Fin 3) : ‖coordinateInsertion i j‖ ≤ 1

noncomputable def EulerMeanCurlTensor.coordinateL2 (i j : Fin 3) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

Coordinate L², given by (coordinateInsertion i j).compLpL 2 volume.

Equations

• EulerMeanCurlTensor.coordinateL2 i j = ContinuousLinearMap.compLpL 2 MeasureTheory.volume (EulerMeanCurlTensor.coordinateInsertion i j)

theorem EulerMeanCurlTensor.coordinateL2_ae (i j : Fin 3) (u : ↥EulerMeanSolenoidal.L2) : ↑↑((coordinateL2 i j) u) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => (↑↑u x).ofLp j • EuclideanSpace.single i 1

theorem EulerMeanCurlTensor.coordinateL2_apply_norm_le (i j : Fin 3) (u : ↥EulerMeanSolenoidal.L2) : ‖(coordinateL2 i j) u‖ ≤ ‖u‖

noncomputable def EulerMeanCurlTensor.curlTensor : EulerMeanGradientTest.GradientTensor →L[ℝ] ↥EulerMeanSolenoidal.L2

Each output component is the difference of the two off-diagonal derivative entries.

Equations

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

theorem EulerMeanCurlTensor.curlTensor_apply (G : EulerMeanGradientTest.GradientTensor) : curlTensor G = ∑ i : Fin 3, ((coordinateL2 i (i + 2)) (G.ofLp (i + 1)) - (coordinateL2 i (i + 1)) (G.ofLp (i + 2)))

theorem EulerMeanCurlTensor.curlTensor_norm_le (G : EulerMeanGradientTest.GradientTensor) : ‖curlTensor G‖ ≤ 6 * ‖G‖

A fixed universal contraction bound; sharpness is not needed for localization.

theorem EulerMeanCurlTensor.curlTensor_ae (G : EulerMeanGradientTest.GradientTensor) : ↑↑(curlTensor G) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => WithLp.toLp 2 fun (i : Fin 3) => (↑↑(G.ofLp (i + 1)) x).ofLp (i + 2) - (↑↑(G.ofLp (i + 2)) x).ofLp (i + 1)

theorem EulerMeanCurlTensor.curlTensor_test_ae (f : EulerMeanGradientTest.Test) : ↑↑(curlTensor (EulerMeanGradientTest.testGradient f)) =ᵐ[MeasureTheory.volume] EulerMeanCutoffCurl.vectorCurl ↑f

On genuine test gradients the tensor operator is exactly the ordinary classical curl.

noncomputable def EulerMeanCurlTensor.harmonicPart (χ : EulerMeanBoundary.Cutoff) (z : ↥EulerMeanSolenoidal.L2) : ↥EulerMeanSolenoidal.L2

The source's field w, formed directly from the weak potential's gradient tensor.

Equations

• EulerMeanCurlTensor.harmonicPart χ z = EulerMeanCurlTensor.curlTensor ↑((EulerMeanBoundary.weakPotential χ) z)

theorem EulerMeanCurlTensor.harmonicPart_norm_le (χ : EulerMeanBoundary.Cutoff) (z : ↥EulerMeanSolenoidal.L2) : ‖harmonicPart χ z‖ ≤ 6 * ‖(EulerMeanBoundary.weakPotential χ) z‖

noncomputable def EulerMeanCurlIntegration.partialTest (f : EulerMeanGradientTest.Test) (i : Fin 3) : EulerMeanGradientTest.Test

Partial test, given by ⟨vectorPartial (f : Space → Space) i, vectorPartial_smooth f f.smooth i, vectorPartial_compact f f.compact i⟩.

Equations

• EulerMeanCurlIntegration.partialTest f i = ⟨EulerMeanVectorIdentities.vectorPartial (↑f) i, ⋯⟩

theorem EulerMeanCurlIntegration.test_memLp (f : EulerMeanGradientTest.Test) : MeasureTheory.MemLp (↑f) 2 MeasureTheory.volume

noncomputable def EulerMeanCurlIntegration.testValue (f : EulerMeanGradientTest.Test) : ↥EulerMeanSolenoidal.L2

Test value, given by (test_memLp f).toLp (f : Space → Space).

Equations

• EulerMeanCurlIntegration.testValue f = MeasureTheory.MemLp.toLp ↑f ⋯

theorem EulerMeanCurlIntegration.testValue_ae (f : EulerMeanGradientTest.Test) : ↑↑(testValue f) =ᵐ[MeasureTheory.volume] ↑f

theorem EulerMeanCurlIntegration.test_inner_integrable (f g : EulerMeanGradientTest.Test) : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => inner ℝ (↑f x) (↑g x)) MeasureTheory.volume

theorem EulerMeanCurlIntegration.test_inner_eq_integral (f g : EulerMeanGradientTest.Test) : inner ℝ (testValue f) (testValue g) = ∫ (x : EulerSmoothLimit.Space), inner ℝ (↑f x) (↑g x)

theorem EulerMeanCurlIntegration.directional_integration_by_parts (f g : EulerMeanGradientTest.Test) (i : Fin 3) : ∫ (x : EulerSmoothLimit.Space), inner ℝ (EulerMeanVectorIdentities.vectorPartial (↑f) i x) (↑g x) = -∫ (x : EulerSmoothLimit.Space), inner ℝ (↑f x) (EulerMeanVectorIdentities.vectorPartial (↑g) i x)

theorem EulerMeanCurlIntegration.testGradient_pairing (f g : EulerMeanGradientTest.Test) : inner ℝ (EulerMeanGradientTest.testGradient f) (EulerMeanGradientTest.testGradient g) = -∫ (x : EulerSmoothLimit.Space), inner ℝ (↑f x) (Laplacian.laplacian (↑g) x)

The actual tensor inner product has the usual distributional Laplacian formula.

theorem EulerMeanCurlIntegration.scalar_partial_ibp (f g : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfc : HasCompactSupport f) (hgc : HasCompactSupport g) (i : Fin 3) : ∫ (x : EulerSmoothLimit.Space), EulerVectorCalculus.partialDerivative f i x * g x = -∫ (x : EulerSmoothLimit.Space), f x * EulerVectorCalculus.partialDerivative g i x

theorem EulerMeanCurlIntegration.integral_three_sub (a b c d e f : EulerSmoothLimit.Space → ℝ) (ha : MeasureTheory.Integrable a MeasureTheory.volume) (hb : MeasureTheory.Integrable b MeasureTheory.volume) (hc : MeasureTheory.Integrable c MeasureTheory.volume) (hd : MeasureTheory.Integrable d MeasureTheory.volume) (he : MeasureTheory.Integrable e MeasureTheory.volume) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : EulerSmoothLimit.Space), a x - b x + (c x - d x) + (e x - f x) = ((∫ (x : EulerSmoothLimit.Space), a x) - ∫ (x : EulerSmoothLimit.Space), b x) + ((∫ (x : EulerSmoothLimit.Space), c x) - ∫ (x : EulerSmoothLimit.Space), d x) + ((∫ (x : EulerSmoothLimit.Space), e x) - ∫ (x : EulerSmoothLimit.Space), f x)

theorem EulerMeanCurlIntegration.integral_curl_selfadjoint (f g : EulerMeanGradientTest.Test) : ∫ (x : EulerSmoothLimit.Space), inner ℝ (EulerMeanCutoffCurl.vectorCurl (↑f) x) (↑g x) = ∫ (x : EulerSmoothLimit.Space), inner ℝ (↑f x) (EulerMeanCutoffCurl.vectorCurl (↑g) x)

The ordinary real curl is formally self-adjoint on compact smooth vector tests.

theorem EulerMeanCurlIntegration.curlTensor_test_eq (f : EulerMeanGradientTest.Test) : EulerMeanCurlTensor.curlTensor (EulerMeanGradientTest.testGradient f) = testValue (EulerMeanVectorIdentities.curlTest f)

theorem EulerMeanCurlIntegration.test_gradient_curl_pairing (f g : EulerMeanGradientTest.Test) : inner ℝ (EulerMeanGradientTest.testGradient f) (EulerMeanGradientTest.testGradient (EulerMeanVectorIdentities.curlTest g)) = -inner ℝ (EulerMeanCurlTensor.curlTensor (EulerMeanGradientTest.testGradient f)) (testValue (EulerMeanVectorIdentities.laplacianTest g))

theorem EulerMeanCurlIntegration.homogeneous_curl_pairing (u : ↥EulerMeanGradientTest.homogeneousSpace) (g : EulerMeanGradientTest.Test) : inner ℝ u (EulerMeanGradientTest.homogeneousGradient (EulerMeanVectorIdentities.curlTest g)) = -inner ℝ (EulerMeanCurlTensor.curlTensor ↑u) (testValue (EulerMeanVectorIdentities.laplacianTest g))

Distributional integration by parts survives passage to the closed homogeneous gradient space.

def EulerMeanHarmonic.WeakHarmonicOn (U : Set EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) : Prop

Distributional harmonicity of an actual ordinary L² vector field on a set.

Equations

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

theorem EulerMeanHarmonic.l2_test_pairing (u : ↥EulerMeanSolenoidal.L2) (f : EulerMeanGradientTest.Test) : inner ℝ u (EulerMeanCurlIntegration.testValue f) = ∫ (x : EulerSmoothLimit.Space), inner ℝ (↑↑u x) (↑f x)

noncomputable def EulerMeanHarmonic.divergenceGradient (f : EulerMeanGradientTest.Test) : ↥EulerMeanSolenoidal.L2

Divergence gradient, constructed using EulerMeanSolenoidal.testGradient.

Equations

• EulerMeanHarmonic.divergenceGradient f = EulerMeanSolenoidal.testGradient (EulerSmoothLimit.divergence ↑f) ⋯ ⋯

theorem EulerMeanHarmonic.divergenceGradient_ae (f : EulerMeanGradientTest.Test) : ↑↑(divergenceGradient f) =ᵐ[MeasureTheory.volume] gradient (EulerSmoothLimit.divergence ↑f)

theorem EulerMeanHarmonic.divergenceGradient_mem (f : EulerMeanGradientTest.Test) : divergenceGradient f ∈ EulerMeanSolenoidal.gradientSpace

theorem EulerMeanHarmonic.testValue_curlcurl (f : EulerMeanGradientTest.Test) : EulerMeanCurlIntegration.testValue (EulerMeanVectorIdentities.curlTest (EulerMeanVectorIdentities.curlTest f)) = divergenceGradient f - EulerMeanCurlIntegration.testValue (EulerMeanVectorIdentities.laplacianTest f)

theorem EulerMeanHarmonic.solenoidal_curlcurl_pairing (z : ↥EulerMeanSolenoidal.L2) (hz : z ∈ EulerMeanSolenoidal.solenoidalSpace) (f : EulerMeanGradientTest.Test) : inner ℝ z (EulerMeanCurlIntegration.testValue (EulerMeanVectorIdentities.curlTest (EulerMeanVectorIdentities.curlTest f))) = -inner ℝ z (EulerMeanCurlIntegration.testValue (EulerMeanVectorIdentities.laplacianTest f))

theorem EulerMeanHarmonic.cutoff_curlTest_eq (χ : EulerMeanBoundary.Cutoff) (U : Set EulerSmoothLimit.Space) (hχ : ∀ x ∈ U, χ.field x = 1) (f : EulerMeanGradientTest.Test) (hf : tsupport ↑f ⊆ U) : (fun (x : EulerSmoothLimit.Space) => χ.field x • ↑(EulerMeanVectorIdentities.curlTest f) x) = EulerMeanCutoffCurl.vectorCurl ↑f

theorem EulerMeanHarmonic.homogeneous_curl_solenoidal (u : ↥EulerMeanGradientTest.homogeneousSpace) : EulerMeanCurlTensor.curlTensor ↑u ∈ EulerMeanSolenoidal.solenoidalSpace

The actual curl tensor of any homogeneous potential remains solenoidal.

theorem EulerMeanHarmonic.harmonicPart_solenoidal (χ : EulerMeanBoundary.Cutoff) (z : ↥EulerMeanSolenoidal.L2) : EulerMeanCurlTensor.harmonicPart χ z ∈ EulerMeanSolenoidal.solenoidalSpace

theorem EulerMeanHarmonic.weakHarmonicOn_sub_harmonicPart (χ : EulerMeanBoundary.Cutoff) (U : Set EulerSmoothLimit.Space) (z : ↥EulerMeanSolenoidal.L2) (hz : z ∈ EulerMeanSolenoidal.solenoidalSpace) (hχ : ∀ x ∈ U, χ.field x = 1) : WeakHarmonicOn U (z - EulerMeanCurlTensor.harmonicPart χ z)

The source's z - w is genuinely weakly harmonic where the actual cutoff equals one.

theorem EulerMeanHarmonic.exists_weak_harmonic_decomposition (χ : EulerMeanBoundary.Cutoff) (U : Set EulerSmoothLimit.Space) (z : ↥EulerMeanSolenoidal.L2) (hz : z ∈ EulerMeanSolenoidal.solenoidalSpace) (hχ : ∀ x ∈ U, χ.field x = 1) : ∃ (w : ↥EulerMeanSolenoidal.L2), w = EulerMeanCurlTensor.harmonicPart χ z ∧ w ∈ EulerMeanSolenoidal.solenoidalSpace ∧ ‖w‖ ≤ 6 * ‖(EulerMeanBoundary.weakPotential χ) z‖ ∧ WeakHarmonicOn U (z - w)

A quantitative decomposition constructed from the cutoff and the given solenoidal field.