The ordinary three-dimensional solenoidal space for the mean inverse

This is the actual Lebesgue L² space on R³. Its solenoidal subspace is defined by orthogonality to genuine compactly supported smooth gradients, and the weak divergence test characterization is proved. The projected coefficient inverse below acts on this space, rather than on the lifted cylinder used by the oscillatory correction construction.

@[reducible, inline]

noncomputable abbrev EulerMeanSolenoidal.L2 : AddSubgroup (EulerSmoothLimit.Space →ₘ[MeasureTheory.volume] EulerSmoothLimit.Space)

L²: an abbreviation for MeasureTheory.Lp Space 2 (volume : Measure Space).

Equations

• EulerMeanSolenoidal.L2 = MeasureTheory.Lp EulerSmoothLimit.Space 2 MeasureTheory.volume

theorem EulerMeanSolenoidal.contDiff_gradient {φ : EulerSmoothLimit.Space → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ (↑⊤) (gradient φ)

theorem EulerMeanSolenoidal.compactSupport_gradient {φ : EulerSmoothLimit.Space → ℝ} (hφ : HasCompactSupport φ) : HasCompactSupport (gradient φ)

theorem EulerMeanSolenoidal.gradient_memLp {φ : EulerSmoothLimit.Space → ℝ} (hc : HasCompactSupport φ) (hs : ContDiff ℝ (↑⊤) φ) : MeasureTheory.MemLp (gradient φ) 2 MeasureTheory.volume

noncomputable def EulerMeanSolenoidal.testGradient (φ : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport φ) (hs : ContDiff ℝ (↑⊤) φ) : ↥L2

Test gradient, given by (gradient_memLp hc hs).toLp (gradient φ).

Equations

• EulerMeanSolenoidal.testGradient φ hc hs = MeasureTheory.MemLp.toLp (gradient φ) ⋯

theorem EulerMeanSolenoidal.testGradient_ae (φ : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport φ) (hs : ContDiff ℝ (↑⊤) φ) : ↑↑(testGradient φ hc hs) =ᵐ[MeasureTheory.volume] gradient φ

def EulerMeanSolenoidal.gradientGenerators : Set ↥L2

Gradient generators, given by {g | ∃ φ : Space → ℝ, HasCompactSupport φ ∧ ContDiff ℝ ∞ φ ∧ g =ᵐ[volume] gradient φ}.

Equations

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

noncomputable def EulerMeanSolenoidal.gradientSpace : Submodule ℝ ↥L2

Gradient space, given by (Submodule.span ℝ gradientGenerators).topologicalClosure.

Equations

• EulerMeanSolenoidal.gradientSpace = (Submodule.span ℝ EulerMeanSolenoidal.gradientGenerators).topologicalClosure

theorem EulerMeanSolenoidal.gradientSpace_closed : IsClosed ↑gradientSpace

instance EulerMeanSolenoidal.instCompleteSpaceSubtypeAEEqFunSpaceVolumeMemAddSubgroupL2SubmoduleRealGradientSpace : CompleteSpace ↥gradientSpace

noncomputable def EulerMeanSolenoidal.solenoidalSpace : Submodule ℝ ↥L2

Solenoidal space, given by gradientSpace.orthogonal instance : CompleteSpace solenoidalSpace := gradientSpace.isClosed_orthogonal.completeSpace_coe.

Equations

• EulerMeanSolenoidal.solenoidalSpace = EulerMeanSolenoidal.gradientSpaceᗮ

instance EulerMeanSolenoidal.instCompleteSpaceSubtypeAEEqFunSpaceVolumeMemAddSubgroupL2SubmoduleRealSolenoidalSpace : CompleteSpace ↥solenoidalSpace

theorem EulerMeanSolenoidal.testGradient_mem (φ : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport φ) (hs : ContDiff ℝ (↑⊤) φ) : testGradient φ hc hs ∈ gradientSpace

theorem EulerMeanSolenoidal.weak_divergence_test {u : ↥L2} (hu : u ∈ solenoidalSpace) (φ : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport φ) (hs : ContDiff ℝ (↑⊤) φ) : ∫ (x : EulerSmoothLimit.Space), inner ℝ (gradient φ x) (↑↑u x) = 0

theorem EulerMeanSolenoidal.mem_solenoidal_iff (u : ↥L2) : u ∈ solenoidalSpace ↔ ∀ (φ : EulerSmoothLimit.Space → ℝ), HasCompactSupport φ → ContDiff ℝ (↑⊤) φ → ∫ (x : EulerSmoothLimit.Space), inner ℝ (gradient φ x) (↑↑u x) = 0

Orthogonality is equivalent to the ordinary distributional divergence test.

noncomputable def EulerMeanSolenoidal.solenoidalProjection : ↥L2 →L[ℝ] ↥L2

Solenoidal projection, given by solenoidalSpace.starProjection.

Equations

• EulerMeanSolenoidal.solenoidalProjection = EulerMeanSolenoidal.solenoidalSpace.starProjection

theorem EulerMeanSolenoidal.solenoidalProjection_mem (u : ↥L2) : solenoidalProjection u ∈ solenoidalSpace

theorem EulerMeanSolenoidal.solenoidalProjection_norm_le : ‖solenoidalProjection‖ ≤ 1

theorem EulerMeanSolenoidal.solenoidalProjection_apply_norm_le (u : ↥L2) : ‖solenoidalProjection u‖ ≤ ‖u‖

theorem EulerMeanSolenoidal.solenoidal_orthogonal : solenoidalSpaceᗮ = gradientSpace

theorem EulerMeanSolenoidal.sub_solenoidalProjection_mem_gradient (u : ↥L2) : u - solenoidalProjection u ∈ gradientSpace

The pressure component of the ordinary Helmholtz decomposition.

theorem EulerMeanSolenoidal.solenoidalProjection_eq_zero_iff (u : ↥L2) : solenoidalProjection u = 0 ↔ u ∈ gradientSpace

theorem EulerMeanSolenoidal.pressure_pairing_zero {p u : ↥L2} (hp : p ∈ gradientSpace) (hu : u ∈ solenoidalSpace) : inner ℝ p u = 0

theorem EulerMeanSolenoidal.gradient_test_integration_by_parts (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (φ : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport φ) (hs : ContDiff ℝ (↑⊤) φ) : ∫ (x : EulerSmoothLimit.Space), inner ℝ (gradient φ x) (u x) = -∫ (x : EulerSmoothLimit.Space), φ x * EulerSmoothLimit.divergence u x

Classical integration by parts against a compact smooth test, on R³.

theorem EulerMeanSolenoidal.smooth_mem_solenoidal (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hLp : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) : MeasureTheory.MemLp.toLp u hLp ∈ solenoidalSpace

A classical divergence-free L² field lies in the actual closed mean space.

theorem EulerMeanSolenoidal.curl_mem_solenoidal (ψ : Fin 3 → EulerSmoothLimit.Space → ℝ) (hψ : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (ψ i)) (hLp : MeasureTheory.MemLp (EulerVectorCalculus.curl ψ) 2 MeasureTheory.volume) : MeasureTheory.MemLp.toLp (EulerVectorCalculus.curl ψ) hLp ∈ solenoidalSpace

In particular, every smooth L² curl is solenoidal in the ordinary space.

noncomputable def EulerMeanSolenoidal.metricInverse (A : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hA : MeasureTheory.AEStronglyMeasurable A MeasureTheory.volume) (C : NNReal) (hbound : ∀ (x : EulerSmoothLimit.Space), ‖A x‖ ≤ ↑C) (c : ℝ) (hc : 0 < c) (hpositive : ∀ (x v : EulerSmoothLimit.Space), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) : ↥solenoidalSpace →L[ℝ] ↥solenoidalSpace

The concrete inverse of the projected ordinary-space coefficient multiplier.

Equations

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

theorem EulerMeanSolenoidal.metricInverse_equation (A : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hA : MeasureTheory.AEStronglyMeasurable A MeasureTheory.volume) (C : NNReal) (hbound : ∀ (x : EulerSmoothLimit.Space), ‖A x‖ ≤ ↑C) (c : ℝ) (hc : 0 < c) (hpositive : ∀ (x v : EulerSmoothLimit.Space), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : ↥solenoidalSpace) : solenoidalSpace.orthogonalProjectionOnto ((EulerLiftedPressure.coefficientOperator A hA C hbound) ↑((metricInverse A hA C hbound c hc hpositive) f)) = f

theorem EulerMeanSolenoidal.metricInverse_norm_le (A : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hA : MeasureTheory.AEStronglyMeasurable A MeasureTheory.volume) (C : NNReal) (hbound : ∀ (x : EulerSmoothLimit.Space), ‖A x‖ ≤ ↑C) (c : ℝ) (hc : 0 < c) (hpositive : ∀ (x v : EulerSmoothLimit.Space), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) : ‖metricInverse A hA C hbound c hc hpositive‖ ≤ c⁻¹

theorem EulerMeanSolenoidal.existsUnique_metric_solution (A : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hA : MeasureTheory.AEStronglyMeasurable A MeasureTheory.volume) (C : NNReal) (hbound : ∀ (x : EulerSmoothLimit.Space), ‖A x‖ ≤ ↑C) (c : ℝ) (hc : 0 < c) (hpositive : ∀ (x v : EulerSmoothLimit.Space), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : ↥L2) : ∃! u : ↥solenoidalSpace, solenoidalSpace.orthogonalProjectionOnto ((EulerLiftedPressure.coefficientOperator A hA C hbound) ↑u) = solenoidalSpace.orthogonalProjectionOnto f

A forcing in the ambient L² space has one solenoidal solution of the projected metric equation. No inverse or solution is supplied as an input.

theorem EulerMeanSolenoidal.metric_solution_residual_gradient (A : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hA : MeasureTheory.AEStronglyMeasurable A MeasureTheory.volume) (C : NNReal) (hbound : ∀ (x : EulerSmoothLimit.Space), ‖A x‖ ≤ ↑C) (f : ↥L2) (u : ↥solenoidalSpace) (hu : solenoidalSpace.orthogonalProjectionOnto ((EulerLiftedPressure.coefficientOperator A hA C hbound) ↑u) = solenoidalSpace.orthogonalProjectionOnto f) : f - (EulerLiftedPressure.coefficientOperator A hA C hbound) ↑u ∈ gradientSpace

The residual of the solved projected equation is a genuine weak gradient.