Canonical spatial fields and all their actual derivative tensors are in physical L². Their bounds have only explicit polynomial frequency loss.

noncomputable def EulerCylinderPhysicalTensor.physicalPhase (P k : ℝ) (m x : EulerLiftedGradientSpace.Vector3) : AddCircle P

Physical phase, given by (k*inner ℝ m x : ℝ).

Equations

• EulerCylinderPhysicalTensor.physicalPhase P k m x = ↑(k * inner ℝ m x)

theorem EulerCylinderPhysicalTensor.physicalPhase_continuous (P k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : Continuous (physicalPhase P k m)

theorem EulerCylinderPhysicalTensor.frequencyFactor_le_linear (k : ℝ) (hk : 1 ≤ k) (m : EulerLiftedGradientSpace.Vector3) : frequencyFactor k m ≤ ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (1 + ‖m‖) * k

noncomputable def EulerAllOrderCorrectionData.FieldTower.physicalPointField {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (t : ↑(Set.Icc 0 T)) : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3

Physical point field, given by physicalField P k m (A.pointField t).

Equations

• A.physicalPointField k m t = EulerCylinderPhysicalTensor.physicalField P k m (A.pointField t)

theorem EulerAllOrderCorrectionData.FieldTower.physicalPointField_smooth {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (A.physicalPointField k m t)

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

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

Physical tensor value, constructed using physicalTensorLp.

Equations

• One or more equations did not get rendered due to their size.

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

theorem EulerAllOrderCorrectionData.FieldTower.physicalTensorValue_norm_le {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (n : ℕ) (t : ↑(Set.Icc 0 T)) : ‖A.physicalTensorValue k m n t‖ ≤ EulerCylinderPhysicalTensor.frequencyFactor k m ^ n * 4 ^ n * √(2 / P + 2 * P) * ‖(A.realization (n + 1)) t‖