Continuity of actual L² product jets #
The ordinary derivative product rule reduces each spatial order to lower orders with differentiated bounded coefficients. This proves continuity of the genuine L² jets, including for operator-valued derivatives.
theorem
EulerLpSmoothCoefficientProduct.jetLp_zero_from_value
{V : Type u}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(f : EulerLpTranslation.SmoothL2Field V)
:
theorem
EulerLpSmoothCoefficientProduct.jetLp_succ_from_derivative
{V : Type u}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(f : EulerLpTranslation.SmoothL2Field V)
(n : ℕ)
:
f.jetLp (n + 1) = (ContinuousLinearMap.compLpL 2 MeasureTheory.volume
↑↑(continuousMultilinearCurryRightEquiv' ℝ n EulerSmoothLimit.Space V).symm)
(f.derivative.jetLp n)
theorem
EulerLpSmoothCoefficientProduct.continuous_product_value
{K : Type v}
[TopologicalSpace K]
[CompactSpace K]
{V W : Type u}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
(A : EulerMeanCoefficients.SmoothCoefficientPath K (V →L[ℝ] W))
(f : K → EulerLpTranslation.SmoothL2Field V)
(hf : Continuous fun (t : K) => (f t).jetLp 0)
:
Continuous fun (t : K) => (product A t (f t)).toLp
theorem
EulerLpSmoothCoefficientProduct.continuous_product_jet
{K : Type v}
[TopologicalSpace K]
[CompactSpace K]
{V W : Type u}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
(A : EulerMeanCoefficients.SmoothCoefficientPath K (V →L[ℝ] W))
(f : K → EulerLpTranslation.SmoothL2Field V)
(hf : ∀ (n : ℕ), Continuous fun (t : K) => (f t).jetLp n)
(n : ℕ)
:
Continuous fun (t : K) => (product A t (f t)).jetLp n
Every actual product jet is continuous in L², with no product-regularity hypothesis.