Actual pointwise mixed derivatives from the finite weighted Sobolev norms of one coherent field tower. No pointwise estimate is assumed.

theorem EulerAllOrderCorrectionData.FieldTower.pointField_wordAtLevel {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (s q n : ℕ) (hq : 3 ≤ q) (hn : n + q ≤ s) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerCylinderSobolev.iteratedFieldDerivative P w (A.pointField t) x = (EulerSobolevPointEvaluation.pointEvaluation P x) ((EulerCylinderSobolevSpace.restrictOperator P hq) ((EulerSobolevWordLevel.wordAtLevel P q n w hn) ((A.realization s) t)))

The canonical representative has exactly the mixed derivative represented by the genuine Sobolev word at any retained high order.

theorem EulerAllOrderCorrectionData.FieldTower.pointField_wordSum_le_block {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (s q n : ℕ) (hq : 3 ≤ q) (hn : n + q ≤ s) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w (A.pointField t) x‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * EulerH6Pressure.blockNorm P (EulerCylinderSobolevSpace.toJet P ((A.realization s) t)) q n

The sum of all mixed pointwise words is bounded by the actual external Sobolev block, with a fixed base-order evaluation constant.

theorem EulerAllOrderCorrectionData.FieldTower.pointField_wordSum_weighted {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (s q N n : ℕ) (hq : 3 ≤ q) (hns : n + q ≤ s) (hnN : n ≤ N) (ρ : ℝ) (hρ : 0 < ρ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerPacketWeights.weight ρ n * ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w (A.pointField t) x‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * EulerSobolevGevreyOperators.weightedNorm P q N ρ ((A.realization s) t)

Selecting the actual nth summand of a weighted Sobolev norm gives the full pointwise mixed-word bound, without an alphabet factor.

theorem EulerAllOrderCorrectionData.FieldTower.pointField_wordSum_gevrey {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (s q N n : ℕ) (hq : 3 ≤ q) (hns : n + q ≤ s) (hnN : n ≤ N) (ρ C : ℝ) (hρ : 0 < ρ) (t : ↑(Set.Icc 0 T)) (hC : EulerSobolevGevreyOperators.weightedNorm P q N ρ ((A.realization s) t) ≤ C) (x : EulerLiftedGradientSpace.LiftDomain P) : ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w (A.pointField t) x‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * C * ρ⁻¹ ^ n * ↑n.factorial ^ 2

A genuine weighted Hq bound gives the literal pointwise Gevrey estimate for every spatial/angular word, with radius reciprocal 1/ρ.

theorem EulerAllOrderCorrectionData.FieldTower.pointField_word_gevrey {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (s q N n : ℕ) (hq : 3 ≤ q) (hns : n + q ≤ s) (hnN : n ≤ N) (ρ C : ℝ) (hρ : 0 < ρ) (t : ↑(Set.Icc 0 T)) (hC : EulerSobolevGevreyOperators.weightedNorm P q N ρ ((A.realization s) t) ≤ C) (w : Fin n → Fin 4) (x : EulerLiftedGradientSpace.LiftDomain P) : ‖EulerCylinderSobolev.iteratedFieldDerivative P w (A.pointField t) x‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * C * ρ⁻¹ ^ n * ↑n.factorial ^ 2