The Comparator solution satisfies the weak projected Euler equation

The test family is the dense family of compact smooth solenoidal fields. Only pointwise identification of the supplied smooth L² fields with the Comparator velocity is assumed; no time regularity of those fields is used.

The Euler equation tested against compact vector fields

Differentiation under the compact spatial integral uses joint smoothness on positive times. It does not assume an L² time derivative or any pressure decay.

Pressure cancellation against compactly supported solenoidal vector tests.

The scalar pressure needs only ordinary smoothness. In particular, neither the pressure nor its gradient is assumed to be globally square integrable.

theorem EulerComparatorPressure.compact_vector_gradient_integration_by_parts (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hφ : ContDiff ℝ (↑⊤) φ) (hc : HasCompactSupport φ) (p : EulerSmoothLimit.Space → ℝ) (hp : ContDiff ℝ (↑⊤) p) : ∫ (x : EulerSmoothLimit.Space), inner ℝ (φ x) (gradient p x) = -∫ (x : EulerSmoothLimit.Space), p x * EulerSmoothLimit.divergence φ x

Integration by parts with compact support on the vector test, rather than on the scalar potential.

theorem EulerComparatorPressure.compact_solenoidal_pressure_pairing_zero (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hφ : ContDiff ℝ (↑⊤) φ) (hc : HasCompactSupport φ) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence φ x = 0) (p : EulerSmoothLimit.Space → ℝ) (hp : ContDiff ℝ (↑⊤) p) : ∫ (x : EulerSmoothLimit.Space), inner ℝ (φ x) (gradient p x) = 0

An arbitrary smooth scalar pressure cancels against a compact smooth divergence-free vector test.

theorem Euler.EulerExistenceAndSmoothnessR3.velocity_test_pairing_hasDerivAt {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (φ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hφ : Continuous φ) (hφc : HasCompactSupport φ) (t₀ : ℝ) (ht₀ : 0 < t₀) : HasDerivAt (fun (t : ℝ) => ∫ (x : EuclideanSpace ℝ (Fin 3)), inner ℝ (φ x) (v x t)) (∫ (x : EuclideanSpace ℝ (Fin 3)), inner ℝ (φ x) (-(fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t₀) x) (v x t₀) - gradient (fun (x : EuclideanSpace ℝ (Fin 3)) => p x t₀) x)) t₀

The pointwise Euler equation differentiates every compactly supported continuous vector test pairing. Pressure is retained in this first identity.

theorem Euler.EulerExistenceAndSmoothnessR3.velocity_solenoidal_test_pairing_hasDerivAt {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (φ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence φ x = 0) (t₀ : ℝ) (ht₀ : 0 < t₀) : HasDerivAt (fun (t : ℝ) => ∫ (x : EuclideanSpace ℝ (Fin 3)), inner ℝ (φ x) (v x t)) (-∫ (x : EuclideanSpace ℝ (Fin 3)), inner ℝ (φ x) ((fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t₀) x) (v x t₀))) t₀

Pressure disappears from the test-pairing derivative when the compact smooth vector test is divergence-free.

theorem Euler.ComparatorBridge.comparator_clamped_compact_pairing_hasDerivAt {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) {T : ℝ} (hT : 0 < T) (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (s : ↑(Set.Icc 0 T)), (A s).field = fun (x : EulerSmoothLimit.Space) => v x ↑s) (g : ↥EulerMeanSolenoidal.L2) (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence φ x = 0) (hg : ↑↑g =ᵐ[MeasureTheory.volume] φ) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => inner ℝ g (A (Set.projIcc 0 T ⋯ r)).toLp) (-∫ (x : EulerSmoothLimit.Space), inner ℝ (φ x) ((fderiv ℝ (fun (x : EulerSmoothLimit.Space) => v x t) x) (v x t))) t

Replacing the Comparator velocity by any pointwise equal smooth L² representatives preserves the tested time equation, including its clamped interval parameterization. No time regularity of the representatives is assumed.

Compact smooth solenoidal tests determine ordinary L² solenoidal fields

The curl-curl identity reduces the orthogonal complement of compact smooth curls inside the solenoidal space to globally weakly harmonic L² fields.

theorem Euler.ComparatorBridge.weakHarmonicOn_univ_eq_zero (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanHarmonic.WeakHarmonicOn Set.univ u) : u = 0

A distributionally harmonic vector field on all of ℝ³ vanishes if it lies in L².

noncomputable def Euler.ComparatorBridge.compactCurlMap : EulerMeanGradientTest.Test →ₗ[ℝ] ↥EulerMeanSolenoidal.L2

Taking the L² class of a compact smooth curl is a linear operation.

Equations

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

def Euler.ComparatorBridge.compactCurlGenerators : Set ↥EulerMeanSolenoidal.L2

L² classes of curls of genuine compactly supported smooth vector fields.

Equations

• Euler.ComparatorBridge.compactCurlGenerators = Set.range fun (f : EulerMeanGradientTest.Test) => EulerMeanCurlIntegration.testValue (EulerMeanVectorIdentities.curlTest f)

noncomputable def Euler.ComparatorBridge.compactCurlSpace : Submodule ℝ ↥EulerMeanSolenoidal.L2

The closed linear space generated by compactly supported smooth curls.

Equations

• Euler.ComparatorBridge.compactCurlSpace = (Submodule.span ℝ Euler.ComparatorBridge.compactCurlGenerators).topologicalClosure

theorem Euler.ComparatorBridge.compactCurlSpace_closed : IsClosed ↑compactCurlSpace

instance Euler.ComparatorBridge.instCompleteSpaceSubtypeAEEqFunSpaceVolumeMemAddSubgroupL2SubmoduleRealCompactCurlSpace : CompleteSpace ↥compactCurlSpace

theorem Euler.ComparatorBridge.compactCurl_mem_solenoidal (f : EulerMeanGradientTest.Test) : EulerMeanCurlIntegration.testValue (EulerMeanVectorIdentities.curlTest f) ∈ EulerMeanSolenoidal.solenoidalSpace

theorem Euler.ComparatorBridge.compactCurl_mem (f : EulerMeanGradientTest.Test) : EulerMeanCurlIntegration.testValue (EulerMeanVectorIdentities.curlTest f) ∈ compactCurlSpace

theorem Euler.ComparatorBridge.compactCurlSpace_le_solenoidal : compactCurlSpace ≤ EulerMeanSolenoidal.solenoidalSpace

theorem Euler.ComparatorBridge.weakHarmonicOn_univ_of_compactCurl_pairing_zero (u : ↥EulerMeanSolenoidal.L2) (hu : u ∈ EulerMeanSolenoidal.solenoidalSpace) (htest : ∀ (f : EulerMeanGradientTest.Test), inner ℝ u (EulerMeanCurlIntegration.testValue (EulerMeanVectorIdentities.curlTest f)) = 0) : EulerMeanHarmonic.WeakHarmonicOn Set.univ u

A solenoidal field annihilating compact smooth curls is weakly harmonic.

theorem Euler.ComparatorBridge.compactCurlSpace_eq_solenoidal : compactCurlSpace = EulerMeanSolenoidal.solenoidalSpace

Compact smooth curls span the entire solenoidal Hilbert space densely.

theorem Euler.ComparatorBridge.closure_compactCurlGenerators : closure compactCurlGenerators = ↑EulerMeanSolenoidal.solenoidalSpace

Linearity makes the closure of the generator set itself the full solenoidal space.

def Euler.ComparatorBridge.compactSolenoidalTests : Set ↥EulerMeanSolenoidal.solenoidalSpace

Compact smooth curl classes regarded as a subset of the solenoidal Hilbert space.

Equations

• Euler.ComparatorBridge.compactSolenoidalTests = {u : ↥EulerMeanSolenoidal.solenoidalSpace | ↑u ∈ Euler.ComparatorBridge.compactCurlGenerators}

theorem Euler.ComparatorBridge.compactSolenoidalTests_representation (u : ↥EulerMeanSolenoidal.solenoidalSpace) (hu : u ∈ compactSolenoidalTests) : ∃ (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space), ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ (∀ (x : EuclideanSpace ℝ (Fin 3)), divergence φ x = 0) ∧ ↑↑↑u =ᵐ[MeasureTheory.volume] φ

Every member is represented by an actual compact smooth divergence-free field.

theorem Euler.ComparatorBridge.compactSolenoidalTests_testValue (u : ↥EulerMeanSolenoidal.solenoidalSpace) (hu : u ∈ compactSolenoidalTests) : ∃ (f : EulerMeanGradientTest.Test), (∀ (x : EuclideanSpace ℝ (Fin 3)), divergence (↑f) x = 0) ∧ EulerMeanCurlIntegration.testValue f = ↑u

A bundled compact smooth solenoidal test has the prescribed L² class.

theorem Euler.ComparatorBridge.compactSolenoidalTests_dense : Dense compactSolenoidalTests

The compact test fields form a dense subset of the actual solenoidal L² space.

theorem Euler.ComparatorBridge.solenoidal_eq_zero_of_compact_test_pairing_zero (u : ↥EulerMeanSolenoidal.L2) (hu : u ∈ EulerMeanSolenoidal.solenoidalSpace) (htest : ∀ (f : EulerMeanGradientTest.Test), (∀ (x : EuclideanSpace ℝ (Fin 3)), divergence (↑f) x = 0) → inner ℝ u (EulerMeanCurlIntegration.testValue f) = 0) : u = 0

Pairings against compact smooth solenoidal tests determine a solenoidal field.

Pairing the projected Euler right-hand side

A solenoidal L² test field removes the Helmholtz projection from the Euler right-hand side. For a smooth divergence-free test field, this gives the ordinary spatial integral against advection. Compactly supported smooth tests automatically satisfy the required L² assumption.

theorem EulerCompactProjectedPairing.inner_solenoidalProjection (φ b : ↥EulerMeanSolenoidal.L2) (hφ : φ ∈ EulerMeanSolenoidal.solenoidalSpace) : inner ℝ φ (EulerMeanSolenoidal.solenoidalProjection b) = inner ℝ φ b

The Helmholtz projection can be removed in a solenoidal pairing.

theorem EulerCompactProjectedPairing.inner_projectedRhs (φ : ↥EulerMeanSolenoidal.L2) (hφ : φ ∈ EulerMeanSolenoidal.solenoidalSpace) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : inner ℝ φ (EulerOrdinarySobolev.projectedRhs A).toLp = -inner ℝ φ (EulerOrdinarySobolev.advectionField A A).toLp

A solenoidal test sees precisely negative advection in the projected Euler right-hand side.

theorem EulerCompactProjectedPairing.inner_projectedRhs_eq_integral (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hLp : MeasureTheory.MemLp φ 2 MeasureTheory.volume) (hφ : MeasureTheory.MemLp.toLp φ hLp ∈ EulerMeanSolenoidal.solenoidalSpace) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : inner ℝ (MeasureTheory.MemLp.toLp φ hLp) (EulerOrdinarySobolev.projectedRhs A).toLp = -∫ (x : EulerSmoothLimit.Space), inner ℝ (φ x) ((fderiv ℝ A.field x) (A.field x))

Integral form of the projected pairing for an arbitrary solenoidal L² representative.

theorem EulerCompactProjectedPairing.smooth_inner_projectedRhs_eq_integral (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hs : ContDiff ℝ (↑⊤) φ) (hLp : MeasureTheory.MemLp φ 2 MeasureTheory.volume) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence φ x = 0) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : inner ℝ (MeasureTheory.MemLp.toLp φ hLp) (EulerOrdinarySobolev.projectedRhs A).toLp = -∫ (x : EulerSmoothLimit.Space), inner ℝ (φ x) ((fderiv ℝ A.field x) (A.field x))

Smooth divergence-free L² tests remove the pressure projection.

theorem EulerCompactProjectedPairing.compact_inner_projectedRhs_eq_integral (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hs : ContDiff ℝ (↑⊤) φ) (hc : HasCompactSupport φ) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence φ x = 0) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : inner ℝ (MeasureTheory.MemLp.toLp φ ⋯) (EulerOrdinarySobolev.projectedRhs A).toLp = -∫ (x : EulerSmoothLimit.Space), inner ℝ (φ x) ((fderiv ℝ A.field x) (A.field x))

In particular, every compactly supported smooth divergence-free test has the projected Euler pairing required by the Comparator bridge.

theorem Euler.ComparatorBridge.comparator_compact_rep_pairing_hasDerivAt {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) {T : ℝ} (hT : 0 < T) (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (s : ↑(Set.Icc 0 T)), (A s).field = fun (x : EulerSmoothLimit.Space) => v x ↑s) (g : ↥EulerMeanSolenoidal.solenoidalSpace) (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence φ x = 0) (hg : ↑↑↑g =ᵐ[MeasureTheory.volume] φ) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => inner ℝ (↑g) (A (Set.projIcc 0 T ⋯ r)).toLp) (inner ℝ (↑g) (EulerOrdinarySobolev.projectedRhs (A ⟨t, ⋯⟩)).toLp) t

An arbitrary compact smooth solenoidal representative has the clamped weak projected derivative used by the Sobolev time-upgrade theorem.

theorem Euler.ComparatorBridge.comparator_projected_pairing_hasDerivAt {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) {T : ℝ} (hT : 0 < T) (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (s : ↑(Set.Icc 0 T)), (A s).field = fun (x : EulerSmoothLimit.Space) => v x ↑s) (g : ↥EulerMeanSolenoidal.solenoidalSpace) (hg : g ∈ compactSolenoidalTests) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => inner ℝ (↑g) (A (Set.projIcc 0 T ⋯ r)).toLp) (inner ℝ (↑g) (EulerOrdinarySobolev.projectedRhs (A ⟨t, ⋯⟩)).toLp) t

The exact weak projected derivative on the dense compact solenoidal test family. This is derived from the Comparator Euler equation itself.