Ordinary derivative tensors of the actual graph field lie in spatial L², with explicit frequency loss and the genuine graph-word norms.

theorem EulerCylinderPhysicalTensor.graphWord_memLp (P k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (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)) (w : Fin n → Fin 4) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderSobolev.iteratedFieldDerivative P w f (EulerGraphPressurePotential.cylinderGraph P k m x)) 2 MeasureTheory.volume

theorem EulerCylinderPhysicalTensor.physicalTensor_memLp (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)) : MeasureTheory.MemLp (iteratedFDeriv ℝ n (physicalField P k m f)) 2 MeasureTheory.volume

noncomputable def EulerCylinderPhysicalTensor.physicalTensorLp (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)) : ↥(MeasureTheory.Lp (EulerLiftedGradientSpace.Vector3 [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3) 2 MeasureTheory.volume)

Physical tensor Lᵖ, given by (physicalTensor_memLp P k m f hf n u hu).toLp (iteratedFDeriv ℝ n (physicalField P k m f)).

Equations

• EulerCylinderPhysicalTensor.physicalTensorLp P k m f hf n u hu = MeasureTheory.MemLp.toLp (iteratedFDeriv ℝ n (EulerCylinderPhysicalTensor.physicalField P k m f)) ⋯

theorem EulerCylinderPhysicalTensor.physicalTensorLp_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)) : ↑↑(physicalTensorLp P k m f hf n u hu) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n (physicalField P k m f)

theorem EulerCylinderPhysicalTensor.physicalTensorLp_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 : ℕ) (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)) : ‖physicalTensorLp P k m f hf n u hu‖ ≤ frequencyFactor k m ^ n * ∑ w : Fin n → Fin 4, ‖u w‖