Actual smooth L² multiplication by bounded smooth coefficients

The coefficient derivatives are genuine uniform-norm jets. The product derivatives are actual Fréchet derivatives, proved square integrable by the Leibniz estimate. The derivative identity remains a literal function equality.

theorem EulerLpSmoothCoefficientProduct.product_memLp {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)) (t : K) (f : EulerLpTranslation.SmoothL2Field V) (n : ℕ) : MeasureTheory.MemLp (iteratedFDeriv ℝ n fun (x : EulerSmoothLimit.Space) => ((A.field t) x) (f.field x)) 2 MeasureTheory.volume

noncomputable def EulerLpSmoothCoefficientProduct.product {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)) (t : K) (f : EulerLpTranslation.SmoothL2Field V) : EulerLpTranslation.SmoothL2Field W

Product, bundling field, smooth, integrable.

Equations

• EulerLpSmoothCoefficientProduct.product A t f = { field := fun (x : EulerSmoothLimit.Space) => ((A.field t) x) (f.field x), smooth := ⋯, integrable := ⋯ }

@[simp]

theorem EulerLpSmoothCoefficientProduct.product_field {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)) (t : K) (f : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : (product A t f).field x = ((A.field t) x) (f.field x)

theorem EulerLpSmoothCoefficientProduct.product_toLp {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)) (t : K) (f : EulerLpTranslation.SmoothL2Field V) : (product A t f).toLp = (EulerLpOperatorField.full MeasureTheory.volume (A.field t)) f.toLp

noncomputable def EulerLpSmoothCoefficientProduct.leftDerivative {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)) : EulerMeanCoefficients.SmoothCoefficientPath K (V →L[ℝ] EulerSmoothLimit.Space →L[ℝ] W)

Left derivative, given by SmoothCoefficientPath.map (flipₗᵢ ℝ Space V W).toContinuousLinearEquiv.toContinuousLinearMap A.derivative.

Equations

• EulerLpSmoothCoefficientProduct.leftDerivative A = EulerMeanCoefficients.SmoothCoefficientPath.map (↑↑(ContinuousLinearMap.flipₗᵢ ℝ EulerSmoothLimit.Space V W)) A.derivative

noncomputable def EulerLpSmoothCoefficientProduct.rightDerivative {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)) : EulerMeanCoefficients.SmoothCoefficientPath K ((EulerSmoothLimit.Space →L[ℝ] V) →L[ℝ] EulerSmoothLimit.Space →L[ℝ] W)

Right derivative, given by SmoothCoefficientPath.map (compL ℝ Space V W) A.

Equations

• EulerLpSmoothCoefficientProduct.rightDerivative A = EulerMeanCoefficients.SmoothCoefficientPath.map (ContinuousLinearMap.compL ℝ EulerSmoothLimit.Space V W) A

theorem EulerLpSmoothCoefficientProduct.product_derivative_field {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)) (t : K) (f : EulerLpTranslation.SmoothL2Field V) : (product A t f).derivative.field = ((product (rightDerivative A) t f.derivative).addField (product (leftDerivative A) t f)).field

theorem EulerLpSmoothCoefficientProduct.jetLp_congr {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (f g : EulerLpTranslation.SmoothL2Field V) (h : f.field = g.field) (n : ℕ) : f.jetLp n = g.jetLp n

theorem EulerLpSmoothCoefficientProduct.product_derivative_jetLp {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)) (t : K) (f : EulerLpTranslation.SmoothL2Field V) (n : ℕ) : (product A t f).derivative.jetLp n = (product (rightDerivative A) t f.derivative).jetLp n + (product (leftDerivative A) t f).jetLp n