The genuine descended derivative tensors of a smooth cylinder field lie in cylinder L² whenever its actual coordinate words do. The bound keeps the ordered-word sum; there is no extra alphabet factor.

theorem EulerCylinderJetLp.cover_periodic (P : ℝ) {V : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain P → V) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) : f (EulerLiftedGradientSpace.coveringMap P (z.1, ↑c + z.2)) = f (EulerLiftedGradientSpace.coveringMap P z)

noncomputable def EulerCylinderJetLp.tensor (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerLiftedGradientSpace.LiftDomain P → V) (n : ℕ) (q : EulerLiftedGradientSpace.LiftDomain P) : EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] V

Tensor, given by jetSeries P (fun z => f (coveringMap P z)) q n.

Equations

• EulerCylinderJetLp.tensor P f n q = EulerCylinderCoverDescent.jetSeries P (fun (z : EulerLiftedGradientSpace.LiftTangent) => f (EulerLiftedGradientSpace.coveringMap P z)) q n

theorem EulerCylinderJetLp.tensor_continuous (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q)) (n : ℕ) : Continuous (tensor P f n)

theorem EulerCylinderJetLp.tensor_norm_le (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q)) (n : ℕ) (q : EulerLiftedGradientSpace.LiftDomain P) : ‖tensor P f n q‖ ≤ ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ ^ n * ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w f q‖

theorem EulerCylinderJetLp.tensor_memLp (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q)) (n : ℕ) (hLp : ∀ (w : Fin n → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative P w f) 2 (EulerLiftedGradientSpace.liftMeasure P)) : MeasureTheory.MemLp (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P)

theorem EulerCylinderJetLp.tensor_eLpNorm_le (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q)) (n : ℕ) (hLp : ∀ (w : Fin n → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative P w f) 2 (EulerLiftedGradientSpace.liftMeasure P)) : (MeasureTheory.eLpNorm (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ ^ n * ∑ w : Fin n → Fin 4, (MeasureTheory.eLpNorm (EulerCylinderSobolev.iteratedFieldDerivative P w f) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal