The actual physical graph field is smooth. Its ordinary spatial derivative tensors are bounded by cylinder derivative words, with an explicit polynomial frequency loss.

noncomputable def EulerCylinderPhysicalTensor.graphCoordinates (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4

Graph coordinates, given by coordinateEquiv.symm.toContinuousLinearMap.comp (graphMap k m).

Equations

• EulerCylinderPhysicalTensor.graphCoordinates k m = ↑EulerCylinderCoordinates.coordinateEquiv.symm ∘SL EulerGraphPullback.graphMap k m

theorem EulerCylinderPhysicalTensor.coordinateEquiv_graphCoordinates (k : ℝ) (m x : EulerLiftedGradientSpace.Vector3) : EulerCylinderCoordinates.coordinateEquiv ((graphCoordinates k m) x) = (EulerGraphPullback.graphMap k m) x

noncomputable def EulerCylinderPhysicalTensor.frequencyFactor (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : ℝ

Frequency factor, given by ‖coordinateEquiv.symm.toContinuousLinearMap‖*(1+|k| * ‖m‖).

Equations

• EulerCylinderPhysicalTensor.frequencyFactor k m = ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (1 + |k| * ‖m‖)

theorem EulerCylinderPhysicalTensor.frequencyFactor_nonneg (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : 0 ≤ frequencyFactor k m

theorem EulerCylinderPhysicalTensor.graphMap_norm_le (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : ‖EulerGraphPullback.graphMap k m‖ ≤ 1 + |k| * ‖m‖

theorem EulerCylinderPhysicalTensor.graphCoordinates_norm_le (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : ‖graphCoordinates k m‖ ≤ frequencyFactor k m

noncomputable def EulerCylinderPhysicalTensor.physicalField (P k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3

Physical field, defined pointwise by f (cylinderGraph P k m x).

Equations

• EulerCylinderPhysicalTensor.physicalField P k m f x = f (EulerGraphPressurePotential.cylinderGraph P k m x)

theorem EulerCylinderPhysicalTensor.physicalField_eq_euclidean (P k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) : physicalField P k m f = EulerCylinderSobolev.euclideanLift P f 0 ∘ ⇑(graphCoordinates k m)

theorem EulerCylinderPhysicalTensor.physicalField_contDiff (P k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) : ContDiff ℝ (↑⊤) (physicalField P k m f)

theorem EulerCylinderPhysicalTensor.physicalTensor_norm_le (P k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (n : ℕ) (x : EulerLiftedGradientSpace.Vector3) : ‖iteratedFDeriv ℝ n (physicalField P k m f) x‖ ≤ frequencyFactor k m ^ n * ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w f (EulerGraphPressurePotential.cylinderGraph P k m x)‖