Every ordinary spatial derivative tensor of the actual physical graph field is a continuous L² path. The proof controls differences by the genuine continuous cylinder-word graph paths.

The physical tensor estimate controls differences of actual L² representatives, which supplies time continuity without a domination premise.

theorem EulerCylinderPhysicalTensor.physicalTensor_norm_le_of_ae (P k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (n : ℕ) (u : (Fin n → Fin 4) → ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume)) (hu : ∀ (w : Fin n → Fin 4), ↑↑(u w) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderSobolev.iteratedFieldDerivative P w f (EulerGraphPressurePotential.cylinderGraph P k m x)) (v : ↥(MeasureTheory.Lp (EulerLiftedGradientSpace.Vector3 [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3) 2 MeasureTheory.volume)) (hv : ↑↑v =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n (physicalField P k m f)) : ‖v‖ ≤ frequencyFactor k m ^ n * ∑ w : Fin n → Fin 4, ‖u w‖

theorem EulerCylinderPhysicalTensor.physicalTensor_difference_norm_le (P k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f g : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P g x)) (n : ℕ) (u v : (Fin n → Fin 4) → ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume)) (hu : ∀ (w : Fin n → Fin 4), ↑↑(u w) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderSobolev.iteratedFieldDerivative P w f (EulerGraphPressurePotential.cylinderGraph P k m x)) (hv : ∀ (w : Fin n → Fin 4), ↑↑(v w) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderSobolev.iteratedFieldDerivative P w g (EulerGraphPressurePotential.cylinderGraph P k m x)) (F G : ↥(MeasureTheory.Lp (EulerLiftedGradientSpace.Vector3 [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3) 2 MeasureTheory.volume)) (hF : ↑↑F =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n (physicalField P k m f)) (hG : ↑↑G =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n (physicalField P k m g)) : ‖F - G‖ ≤ frequencyFactor k m ^ n * ∑ w : Fin n → Fin 4, ‖u w - v w‖

theorem EulerAllOrderCorrectionData.FieldTower.physicalTensorValue_sub_norm_le {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (n : ℕ) (t s : ↑(Set.Icc 0 T)) : ‖A.physicalTensorValue k m n t - A.physicalTensorValue k m n s‖ ≤ EulerCylinderPhysicalTensor.frequencyFactor k m ^ n * ∑ w : Fin n → Fin 4, ‖(A.canonicalGraphWordPath (EulerCylinderPhysicalTensor.physicalPhase P k m) ⋯ n w) t - (A.canonicalGraphWordPath (EulerCylinderPhysicalTensor.physicalPhase P k m) ⋯ n w) s‖

theorem EulerAllOrderCorrectionData.FieldTower.physicalTensorValue_continuous {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (n : ℕ) : Continuous (A.physicalTensorValue k m n)

noncomputable def EulerAllOrderCorrectionData.FieldTower.physicalTensorPath {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (n : ℕ) : C(↑(Set.Icc 0 T), ↥(MeasureTheory.Lp (EulerLiftedGradientSpace.Vector3 [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3) 2 MeasureTheory.volume))

The physical tensor path is constructed from the actual graph field; continuity is a theorem rather than an additional packet hypothesis.

Equations

• A.physicalTensorPath k m n = { toFun := A.physicalTensorValue k m n, continuous_toFun := ⋯ }

theorem EulerAllOrderCorrectionData.FieldTower.physicalTensorPath_ae {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (n : ℕ) (t : ↑(Set.Icc 0 T)) : ↑↑((A.physicalTensorPath k m n) t) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n (A.physicalPointField k m t)