Divergence-free truncation by a radial vector potential

For a smooth divergence-free velocity u, the radial homotopy formula produces a vector potential. Cutting off that potential and taking its curl gives compact smooth divergence-free velocities that agree with u on any prescribed ball. This construction does not assume Sobolev regularity of u.

def Euler.ComparatorBridge.negativeCrossPotential (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (i : Fin 3) (x : EulerSmoothLimit.Space) : ℝ

The coordinate potential -x × u(x).

Equations

• Euler.ComparatorBridge.negativeCrossPotential u i x = x.ofLp (i + 2) * (u x).ofLp (i + 1) - x.ofLp (i + 1) * (u x).ofLp (i + 2)

theorem Euler.ComparatorBridge.negativeCrossPotential_smooth (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (i : Fin 3) : ContDiff ℝ (↑⊤) (negativeCrossPotential u i)

theorem Euler.ComparatorBridge.partialDerivative_negativeCrossPotential (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : Differentiable ℝ u) (i j : Fin 3) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.partialDerivative (negativeCrossPotential u i) j x = (EuclideanSpace.single j 1).ofLp (i + 2) * (u x).ofLp (i + 1) + x.ofLp (i + 2) * ((fderiv ℝ u x) (EuclideanSpace.single j 1)).ofLp (i + 1) - ((EuclideanSpace.single j 1).ofLp (i + 1) * (u x).ofLp (i + 2) + x.ofLp (i + 1) * ((fderiv ℝ u x) (EuclideanSpace.single j 1)).ofLp (i + 2))

theorem Euler.ComparatorBridge.curl_negativeCrossPotential (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : Differentiable ℝ u) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.curl (negativeCrossPotential u) x = 2 • u x + (fderiv ℝ u x) x - EulerSmoothLimit.divergence u x • x

The elementary curl identity behind the radial homotopy formula.

noncomputable def Euler.ComparatorBridge.radialAverage (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

The radial average whose negative cross product is a vector potential.

Equations

• Euler.ComparatorBridge.radialAverage u x = ∫ (t : ℝ) in 0..1, t • u (t • x)

theorem Euler.ComparatorBridge.radialIntegrand_smooth (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ ↑⊤ fun (xt : EulerSmoothLimit.Space × ℝ) => xt.2 • u (xt.2 • xt.1)

A smooth velocity gives a jointly smooth radial integrand.

theorem Euler.ComparatorBridge.radialAverage_smooth (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (radialAverage u)

theorem Euler.ComparatorBridge.radialIntegrand_parameterDerivative (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (x : EulerSmoothLimit.Space) (t : ℝ) : EulerCompactParameterIntegral.parameterDerivative (fun (xt : EulerSmoothLimit.Space × ℝ) => xt.2 • u (xt.2 • xt.1)) (x, t) = t ^ 2 • fderiv ℝ u (t • x)

theorem Euler.ComparatorBridge.fderiv_radialAverage (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (x : EulerSmoothLimit.Space) : fderiv ℝ (radialAverage u) x = ∫ (t : ℝ) in 0..1, t ^ 2 • fderiv ℝ u (t • x)

theorem Euler.ComparatorBridge.radialDerivative_continuous (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (x : EulerSmoothLimit.Space) : Continuous fun (t : ℝ) => t ^ 2 • fderiv ℝ u (t • x)

theorem Euler.ComparatorBridge.divergence_radialAverage (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (radialAverage u) x = 0

theorem Euler.ComparatorBridge.radialAverage_radial_identity (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (x : EulerSmoothLimit.Space) : 2 • radialAverage u x + (fderiv ℝ (radialAverage u) x) x = u x

Differentiating t² u(tx) proves the radial homotopy identity.

noncomputable def Euler.ComparatorBridge.radialPotential (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) : Fin 3 → EulerSmoothLimit.Space → ℝ

The concrete radial vector potential, in the development's curl convention.

Equations

• Euler.ComparatorBridge.radialPotential u = Euler.ComparatorBridge.negativeCrossPotential (Euler.ComparatorBridge.radialAverage u)

theorem Euler.ComparatorBridge.radialPotential_smooth (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (i : Fin 3) : ContDiff ℝ (↑⊤) (radialPotential u i)

theorem Euler.ComparatorBridge.curl_radialPotential (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.curl (radialPotential u) x = u x

The radial construction recovers every smooth divergence-free velocity.

noncomputable def Euler.ComparatorBridge.potentialTruncation (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (χ : EulerSmoothLimit.Space → ℝ) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Cut off the constructed potential, then take its actual curl.

Equations

• Euler.ComparatorBridge.potentialTruncation u χ = EulerVectorCalculus.curl fun (i : Fin 3) (x : EulerSmoothLimit.Space) => χ x * Euler.ComparatorBridge.radialPotential u i x

theorem Euler.ComparatorBridge.potentialTruncation_smooth (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) : ContDiff ℝ (↑⊤) (potentialTruncation u χ)

theorem Euler.ComparatorBridge.potentialTruncation_divergence (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (potentialTruncation u χ) x = 0

theorem Euler.ComparatorBridge.potentialTruncation_support (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (χ : EulerSmoothLimit.Space → ℝ) : tsupport (potentialTruncation u χ) ⊆ tsupport χ

theorem Euler.ComparatorBridge.potentialTruncation_compact (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (χ : EulerSmoothLimit.Space → ℝ) (hχ : HasCompactSupport χ) : HasCompactSupport (potentialTruncation u χ)

theorem Euler.ComparatorBridge.potentialTruncation_eq (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (χ : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) (hχ : χ =ᶠ[nhds x] 1) : potentialTruncation u χ x = u x

theorem Euler.ComparatorBridge.exists_compact_solenoidal_truncation (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (r R : ℝ) (hr : 0 < r) (hrR : r < R) : ∃ (w : EulerSmoothLimit.Space → EulerSmoothLimit.Space), ContDiff ℝ (↑⊤) w ∧ HasCompactSupport w ∧ tsupport w ⊆ Metric.closedBall 0 R ∧ (∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence w x = 0) ∧ ∀ x ∈ Metric.ball 0 r, w x = u x

No all-order integrability is needed to construct compact solenoidal extensions agreeing with a smooth divergence-free field on a ball.

theorem Euler.ComparatorBridge.partialDerivative_mul (f g : EulerSmoothLimit.Space → ℝ) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) (j : Fin 3) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.partialDerivative (fun (y : EulerSmoothLimit.Space) => f y * g y) j x = f x * EulerVectorCalculus.partialDerivative g j x + EulerVectorCalculus.partialDerivative f j x * g x

theorem Euler.ComparatorBridge.curl_mul_apply (χ : EulerSmoothLimit.Space → ℝ) (ψ : Fin 3 → EulerSmoothLimit.Space → ℝ) (hχ : Differentiable ℝ χ) (hψ : ∀ (i : Fin 3), Differentiable ℝ (ψ i)) (x : EulerSmoothLimit.Space) (i : Fin 3) : (EulerVectorCalculus.curl (fun (j : Fin 3) (y : EulerSmoothLimit.Space) => χ y * ψ j y) x).ofLp i = χ x * (EulerVectorCalculus.curl ψ x).ofLp i + EulerVectorCalculus.partialDerivative χ (i + 1) x * ψ (i + 2) x - EulerVectorCalculus.partialDerivative χ (i + 2) x * ψ (i + 1) x

theorem Euler.ComparatorBridge.norm_radialPotential_le (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (i : Fin 3) (x : EulerSmoothLimit.Space) : ‖radialPotential u i x‖ ≤ 2 * ‖x‖ * ‖radialAverage u x‖

theorem Euler.ComparatorBridge.potentialTruncation_error_bound (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (x : EulerSmoothLimit.Space) : ‖potentialTruncation u χ x - χ x • u x‖ ≤ 12 * ‖fderiv ℝ χ x‖ * ‖x‖ * ‖radialAverage u x‖

Cutting off the potential introduces only a zeroth-order error in the radial average, with no derivative of the original velocity in the bound.

theorem Euler.ComparatorBridge.potentialTruncation_norm_bound (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (C : ℝ) (hχbound : ∀ (x : EulerSmoothLimit.Space), ‖χ x‖ ≤ 1) (hderiv : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ χ x‖ * ‖x‖ ≤ C) (x : EulerSmoothLimit.Space) : ‖potentialTruncation u χ x‖ ≤ ‖u x‖ + 12 * C * ‖radialAverage u x‖

theorem Euler.ComparatorBridge.potentialTruncation_energy_bound (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (huL2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (hχcompact : HasCompactSupport χ) (C : ℝ) (hχbound : ∀ (x : EulerSmoothLimit.Space), ‖χ x‖ ≤ 1) (hderiv : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ χ x‖ * ‖x‖ ≤ C) : MeasureTheory.MemLp (potentialTruncation u χ) 2 MeasureTheory.volume ∧ ∫ (x : EulerSmoothLimit.Space), ‖potentialTruncation u χ x‖ ^ 2 ≤ (2 + 1152 * C ^ 2) * ∫ (x : EulerSmoothLimit.Space), ‖u x‖ ^ 2

A cutoff controlled in the scale-invariant derivative norm gives a uniform finite-energy truncation. The numerical constant is inessential.

noncomputable def Euler.ComparatorBridge.scaledCutoff (χ : EulerSmoothLimit.Space → ℝ) (R : ℝ) (x : EulerSmoothLimit.Space) : ℝ

A fixed bump is dilated, so its weighted derivative bound is independent of the truncation radius.

Equations

• Euler.ComparatorBridge.scaledCutoff χ R x = χ (R⁻¹ • x)

theorem Euler.ComparatorBridge.scaledCutoff_smooth (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (R : ℝ) : ContDiff ℝ (↑⊤) (scaledCutoff χ R)

theorem Euler.ComparatorBridge.scaledCutoff_compact (χ : EulerSmoothLimit.Space → ℝ) (hχ : HasCompactSupport χ) (R : ℝ) (hR : R ≠ 0) : HasCompactSupport (scaledCutoff χ R)

theorem Euler.ComparatorBridge.scaledCutoff_derivative_position_bound (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (C : ℝ) (hC : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ χ x‖ * ‖x‖ ≤ C) (R : ℝ) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (scaledCutoff χ R) x‖ * ‖x‖ ≤ C

theorem Euler.ComparatorBridge.exists_derivative_position_bound (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (hχcompact : HasCompactSupport χ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ χ x‖ * ‖x‖ ≤ C

noncomputable def Euler.ComparatorBridge.unitTruncationBump : ContDiffBump 0

Unit truncation bump, given by ⟨1, 2, by norm_num, by norm_num⟩.

Equations

• Euler.ComparatorBridge.unitTruncationBump = NavierStokesAndEuler.SmoothCutoff.baseBump EulerSmoothLimit.Space

noncomputable def Euler.ComparatorBridge.truncationCutoff (R : ℝ) : EulerSmoothLimit.Space → ℝ

Truncation cutoff, given by scaledCutoff unitTruncationBump R.

Equations

• Euler.ComparatorBridge.truncationCutoff R = NavierStokesAndEuler.SmoothCutoff.cutoff EulerSmoothLimit.Space R

theorem Euler.ComparatorBridge.truncationCutoff_smooth (R : ℝ) : ContDiff ℝ (↑⊤) (truncationCutoff R)

theorem Euler.ComparatorBridge.truncationCutoff_norm_le (R : ℝ) (x : EulerSmoothLimit.Space) : ‖truncationCutoff R x‖ ≤ 1

theorem Euler.ComparatorBridge.truncationCutoff_compact (R : ℝ) (hR : 0 < R) : HasCompactSupport (truncationCutoff R)

theorem Euler.ComparatorBridge.truncationCutoff_support (R : ℝ) (hR : 0 < R) : tsupport (truncationCutoff R) ⊆ Metric.closedBall 0 (2 * R)

theorem Euler.ComparatorBridge.truncationCutoff_eventually_one (R : ℝ) (hR : 0 < R) (x : EulerSmoothLimit.Space) (hx : ‖x‖ < R) : truncationCutoff R =ᶠ[nhds x] 1

noncomputable def Euler.ComparatorBridge.finiteEnergyTruncation (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (R : ℝ) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

The truncation family used by the finite-energy flow argument.

Equations

• Euler.ComparatorBridge.finiteEnergyTruncation u R = Euler.ComparatorBridge.potentialTruncation u (Euler.ComparatorBridge.truncationCutoff R)

theorem Euler.ComparatorBridge.finiteEnergyTruncation_smooth (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (R : ℝ) : ContDiff ℝ (↑⊤) (finiteEnergyTruncation u R)

theorem Euler.ComparatorBridge.finiteEnergyTruncation_divergence (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (R : ℝ) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (finiteEnergyTruncation u R) x = 0

theorem Euler.ComparatorBridge.finiteEnergyTruncation_compact (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (R : ℝ) (hR : 0 < R) : HasCompactSupport (finiteEnergyTruncation u R)

theorem Euler.ComparatorBridge.finiteEnergyTruncation_support (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (R : ℝ) (hR : 0 < R) : tsupport (finiteEnergyTruncation u R) ⊆ Metric.closedBall 0 (2 * R)

theorem Euler.ComparatorBridge.finiteEnergyTruncation_eq (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (R : ℝ) (hR : 0 < R) (x : EulerSmoothLimit.Space) (hx : ‖x‖ < R) : finiteEnergyTruncation u R x = u x

theorem Euler.ComparatorBridge.unitTruncationBump_derivative_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (↑unitTruncationBump) x‖ * ‖x‖ ≤ C

noncomputable def Euler.ComparatorBridge.truncationEnergyConstant : ℝ

A fixed finite constant independent of the velocity and cutoff radius.

Equations

• Euler.ComparatorBridge.truncationEnergyConstant = 2 + 1152 * Euler.ComparatorBridge.unitTruncationBump_derivative_bound.choose ^ 2

theorem Euler.ComparatorBridge.truncationEnergyConstant_nonneg : 0 ≤ truncationEnergyConstant

theorem Euler.ComparatorBridge.finiteEnergyTruncation_energy_bound (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) (huL2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) (R : ℝ) (hR : 0 < R) : MeasureTheory.MemLp (finiteEnergyTruncation u R) 2 MeasureTheory.volume ∧ ∫ (x : EulerSmoothLimit.Space), ‖finiteEnergyTruncation u R x‖ ^ 2 ≤ truncationEnergyConstant * ∫ (x : EulerSmoothLimit.Space), ‖u x‖ ^ 2

The concrete compact solenoidal truncations have uniformly controlled energy, using only the original velocity's finite energy and smoothness.