Pointwise evaluation of actual smooth coefficient multiplication in finite cylinder Sobolev spaces.

theorem EulerSobolevPointMultiplication.pointEvaluation_coefficient (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (G : EulerSpatialSobolevInverse.SmoothCoefficient period) (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q G) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (x : EulerLiftedGradientSpace.LiftDomain period) : (EulerSobolevPointEvaluation.pointEvaluation period x) ((EulerCylinderSobolevSpace.restrictOperator period hq) ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) u)) = (G.coefficient x) ((EulerSobolevPointEvaluation.pointEvaluation period x) ((EulerCylinderSobolevSpace.restrictOperator period hq) u))

Bounded evaluation of a genuine Sobolev coefficient product equals the literal pointwise matrix product.