Pointwise physical graph bounds for the actual packet fields. The estimates use the constructed Sobolev tower and its canonical representative.
theorem
EulerPacketCylinderField.Field.toFieldTower_pointField_raw
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(t : ↑(Set.Icc 0 T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
theorem
EulerPacketCylinderField.Field.raw_graph_eq_pointField
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(t : ↑(Set.Icc 0 T))
(k : ℝ)
(m : EulerSmoothLimit.Space)
:
(fun (x : EulerSmoothLimit.Space) => raw (↑t, x, k * inner ℝ m x)) = EulerCylinderPhysicalTensor.physicalField P k m (G.toFieldTower.pointField t)
theorem
EulerPacketCylinderField.Field.WordBound.pointField_wordSum_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
{q d : ℕ}
{R A : ℝ}
(hG : G.WordBound q R A d)
(hq : 3 ≤ q)
(t : ↑(Set.Icc 0 T))
(n : ℕ)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w (G.toFieldTower.pointField t) x‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * A * EulerGevrey.majorant R d n
theorem
EulerPacketCylinderField.Field.WordBound.raw_graph_tensor_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
{q d : ℕ}
{R A : ℝ}
(hG : G.WordBound q R A d)
(hq : 3 ≤ q)
(t : ↑(Set.Icc 0 T))
(k : ℝ)
(m : EulerSmoothLimit.Space)
(n : ℕ)
(x : EulerSmoothLimit.Space)
:
‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => raw (↑t, y, k * inner ℝ m y)) x‖ ≤ EulerCylinderPhysicalTensor.frequencyFactor k m ^ n * (EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * A * EulerGevrey.majorant R d n)
theorem
EulerPacketCylinderField.Field.WordBound.raw_graph_norm_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
{q : ℕ}
{R A : ℝ}
(hG : G.WordBound q R A 0)
(hq : 3 ≤ q)
(t : ↑(Set.Icc 0 T))
(k : ℝ)
(m x : EulerSmoothLimit.Space)
:
theorem
EulerPacketCylinderField.Field.WordBound.raw_graph_fderiv_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
{q : ℕ}
{R A : ℝ}
(hG : G.WordBound q R A 0)
(hq : 3 ≤ q)
(t : ↑(Set.Icc 0 T))
(k : ℝ)
(m x : EulerSmoothLimit.Space)
:
theorem
EulerPacketCylinderField.Field.WordBound.raw_physical_fderiv_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
{q : ℕ}
{R A : ℝ}
(hG : G.WordBound q R A 0)
(hq : 3 ≤ q)
(t : ↑(Set.Icc 0 T))
(k : ℝ)
(m : EulerSmoothLimit.Space)
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
(hY : DifferentiableAt ℝ Y x)
:
Composing the real graph field with a differentiable inverse map preserves the amplitude and contributes its actual derivative norm.