Actual full cylinder gradients from the coordinate derivative Sobolev norms.

theorem EulerCylinderGradient.vector_word_pointwise_le_H6 (period : ℝ) [Fact (0 < period)] (q : ℕ) {m : ℕ} (hm : m ≤ 3) (w : Fin m → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ j ≤ 6, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerCylinderSobolev.iteratedFieldDerivative period w f x‖ ≤ ↑q * EulerCylinderSobolev.cylinderEmbeddingConstant period * (85 * EulerCylinderSobolev.liftSobolevNorm period 6 f)

All low-order real vector derivative words are bounded by the actual H⁶ norm.

theorem EulerCylinderGradient.tangent_coordinate_norm_le (v : EulerLiftedGradientSpace.LiftTangent) (i : Fin 4) : ‖(EulerCylinderCoordinates.coordinateEquiv.symm v).ofLp i‖ ≤ ‖v‖

theorem EulerCylinderGradient.linear_norm_le_standard_sum {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (A : EulerLiftedGradientSpace.LiftTangent →L[ℝ] F) : ‖A‖ ≤ ∑ i : Fin 4, ‖A (EulerCylinderSobolev.standardDirection i)‖

The full product-tangent operator norm is bounded by its four coordinate values.

theorem EulerCylinderGradient.fieldFDeriv_norm_le_standard_sum (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerLiftedWeakDerivative.fieldFDeriv period f x‖ ≤ ∑ i : Fin 4, ‖EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) f x‖

theorem EulerCylinderGradient.fieldFDeriv_memLp_of_coordinates (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hD : ∀ (i : Fin 4), MeasureTheory.MemLp (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) f) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (EulerLiftedWeakDerivative.fieldFDeriv period f) 2 (EulerLiftedGradientSpace.liftMeasure period)

Actual full gradient integrability follows from the four genuine coordinate derivatives.

theorem EulerCylinderGradient.fieldFDeriv_L2_le_coordinate_sum (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hD : ∀ (i : Fin 4), MeasureTheory.MemLp (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) f) 2 (EulerLiftedGradientSpace.liftMeasure period)) : ‖MeasureTheory.MemLp.toLp (EulerLiftedWeakDerivative.fieldFDeriv period f) ⋯‖ ≤ ∑ i : Fin 4, (MeasureTheory.eLpNorm (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) f) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal

The full-gradient L² norm is quantitatively bounded by the coordinate-gradient L² sum.