Literal scalar multiplication of smooth ordinary L² fields and all of their genuine spatial derivatives.

def EulerOrdinarySobolev.scaleField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (c : ℝ) (A : EulerLpTranslation.SmoothL2Field V) : EulerLpTranslation.SmoothL2Field V

Scale field, given by mapField (c • ContinuousLinearMap.id ℝ V) A.

Equations

• EulerOrdinarySobolev.scaleField c A = EulerLpTranslation.SmoothL2Field.mapField (c • ContinuousLinearMap.id ℝ V) A

@[simp]

theorem EulerOrdinarySobolev.scaleField_field {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (c : ℝ) (A : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : (scaleField c A).field x = c • A.field x

theorem EulerOrdinarySobolev.scaleField_toLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (c : ℝ) (A : EulerLpTranslation.SmoothL2Field V) : (scaleField c A).toLp = c • A.toLp

theorem EulerOrdinarySobolev.scaleField_jetLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (c : ℝ) (A : EulerLpTranslation.SmoothL2Field V) (n : ℕ) : (scaleField c A).jetLp n = c • A.jetLp n

theorem EulerOrdinarySobolev.scaleField_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (c : ℝ) (A : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : fderiv ℝ (scaleField c A).field x = c • fderiv ℝ A.field x

theorem EulerOrdinarySobolev.scaleField_one {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) : scaleField 1 A = A

theorem EulerOrdinarySobolev.scaleField_continuous {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] (c : ℝ) (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (n : ℕ) : Continuous fun (t : K) => (scaleField c (A t)).jetLp n

theorem EulerOrdinarySobolev.tensorNorm_scaleField (c : ℝ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) : tensorNorm q (scaleField c A) = |c| * tensorNorm q A

theorem EulerOrdinarySobolev.tensorNorm_scaleField_le (c : ℝ) (hc : 0 ≤ c) (hc1 : c ≤ 1) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) : tensorNorm q (scaleField c A) ≤ tensorNorm q A