Time dependence of the radial truncation

The radial average and potential truncation preserve joint smoothness. For a velocity smooth only on nonnegative times, the square-time pullback is globally smooth. Pulling this family back along the continuous square root recovers the original truncation, which is sufficient for the continuous-in-time spatial-jet interface of SmoothTimeField.

theorem Euler.ComparatorBridge.radialAverage_family_smooth (v : EulerSmoothLimit.Space × ℝ → EulerSmoothLimit.Space) (hv : ContDiff ℝ (↑⊤) v) : ContDiff ℝ ↑⊤ fun (xt : EulerSmoothLimit.Space × ℝ) => radialAverage (fun (y : EulerSmoothLimit.Space) => v (y, xt.2)) xt.1

Radial integration preserves joint smoothness with an auxiliary parameter.

theorem Euler.ComparatorBridge.radialPotential_family_smooth (v : EulerSmoothLimit.Space × ℝ → EulerSmoothLimit.Space) (hv : ContDiff ℝ (↑⊤) v) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (xt : EulerSmoothLimit.Space × ℝ) => radialPotential (fun (y : EulerSmoothLimit.Space) => v (y, xt.2)) i xt.1

The radial vector potential is jointly smooth in space and the parameter.

theorem Euler.ComparatorBridge.spatial_fderiv_family_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : EulerSmoothLimit.Space × ℝ → E) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ ↑⊤ fun (xt : EulerSmoothLimit.Space × ℝ) => fderiv ℝ (fun (y : EulerSmoothLimit.Space) => f (y, xt.2)) xt.1

Spatial derivatives of a smooth joint family are jointly smooth.

theorem Euler.ComparatorBridge.curl_family_smooth (ψ : Fin 3 → EulerSmoothLimit.Space × ℝ → ℝ) (hψ : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (ψ i)) : ContDiff ℝ ↑⊤ fun (xt : EulerSmoothLimit.Space × ℝ) => EulerVectorCalculus.curl (fun (i : Fin 3) (y : EulerSmoothLimit.Space) => ψ i (y, xt.2)) xt.1

Curl, applied in the spatial variables only, preserves joint smoothness.

theorem Euler.ComparatorBridge.potentialTruncation_family_smooth (v : EulerSmoothLimit.Space × ℝ → EulerSmoothLimit.Space) (hv : ContDiff ℝ (↑⊤) v) (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) : ContDiff ℝ ↑⊤ fun (xt : EulerSmoothLimit.Space × ℝ) => potentialTruncation (fun (y : EulerSmoothLimit.Space) => v (y, xt.2)) χ xt.1

A fixed smooth cutoff gives a jointly smooth family of solenoidal truncations.

theorem Euler.ComparatorBridge.nonnegative_time_square_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : EulerSmoothLimit.Space × ℝ → E) (hv : ContDiffOn ℝ (↑⊤) v (Set.univ ×ˢ Set.Ici 0)) : ContDiff ℝ ↑⊤ fun (xt : EulerSmoothLimit.Space × ℝ) => v (xt.1, xt.2 ^ 2)

Squaring the time parameter turns smoothness on the closed half-space into global smoothness, including at time zero.

theorem Euler.ComparatorBridge.potentialTruncation_square_family_smooth (v : EulerSmoothLimit.Space × ℝ → EulerSmoothLimit.Space) (hv : ContDiffOn ℝ (↑⊤) v (Set.univ ×ˢ Set.Ici 0)) (χ : EulerSmoothLimit.Space → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) : ContDiff ℝ ↑⊤ fun (xt : EulerSmoothLimit.Space × ℝ) => potentialTruncation (fun (y : EulerSmoothLimit.Space) => v (y, xt.2 ^ 2)) χ xt.1

The radial truncation of a Comparator-smooth field has a globally smooth square-time parametrization.

noncomputable def Euler.ComparatorBridge.sqrtTimeMap (T : ℝ) : C(↑(Set.Icc 0 T), ↑(Set.Icc 0 √T))

The continuous time map used to recover the original compact time interval.

Equations

• Euler.ComparatorBridge.sqrtTimeMap T = { toFun := fun (t : ↑(Set.Icc 0 T)) => ⟨√↑t, ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem Euler.ComparatorBridge.sqrtTimeMap_apply (T : ℝ) (t : ↑(Set.Icc 0 T)) : ↑((sqrtTimeMap T) t) = √↑t

theorem Euler.ComparatorBridge.potentialTruncation_square_sqrt (v : EulerSmoothLimit.Space × ℝ → EulerSmoothLimit.Space) (χ : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) {t : ℝ} (ht : 0 ≤ t) : potentialTruncation (fun (y : EulerSmoothLimit.Space) => v (y, √t ^ 2)) χ x = potentialTruncation (fun (y : EulerSmoothLimit.Space) => v (y, t)) χ x

Continuous square-root reparametrization recovers the exact original family.