Physical reconstruction preserves the small amplitude of a lifted correction. All spatial derivatives are actual derivatives of κF e evaluated on the phase graph and pulled through the inverse parent flow.

theorem EulerCylinderPhysicalTensor.physicalField_gevrey (P k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P e x)) (A S : ℝ) (hb : ∀ (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain P), ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w e x‖ ≤ A * S ^ n * ↑n.factorial ^ 2) (n : ℕ) (x : EulerLiftedGradientSpace.Vector3) : ‖iteratedFDeriv ℝ n (physicalField P k m e) x‖ ≤ A * EulerGevrey.majorant (frequencyFactor k m * S) 0 n

noncomputable def EulerPacketPhysicalGevrey.graphReconstruction {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Graph reconstruction, given by κ • D.F.field t x (physicalField P k D.m₀ (e t) x).

Equations

• EulerPacketPhysicalGevrey.graphReconstruction D P κ k e t x = κ • ((D.F.field t) x) (EulerCylinderPhysicalTensor.physicalField P k D.m₀ (e t) x)

theorem EulerPacketPhysicalGevrey.graphReconstruction_contDiff {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (he : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (e t) x)) (t : ↑(Set.Icc 0 D.T)) : ContDiff ℝ (↑⊤) (graphReconstruction D P κ k e t)

theorem EulerPacketPhysicalGevrey.graphReconstruction_gevrey {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (he : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (e t) x)) (R C A S : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hA : 0 ≤ A) (hS : 0 ≤ S) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w (e t) x‖ ≤ A * S ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (graphReconstruction D P κ k e t) x‖ ≤ |κ| * 3 * C * A * EulerGevrey.majorant (R + EulerCylinderPhysicalTensor.frequencyFactor k D.m₀ * S) 0 n

noncomputable def EulerPacketPhysicalGevrey.physicalReconstruction {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Physical reconstruction, given by graphReconstruction D P κ k e t (Y t x).

Equations

• EulerPacketPhysicalGevrey.physicalReconstruction D P κ k e Y t x = EulerPacketPhysicalGevrey.graphReconstruction D P κ k e t (Y t x)

noncomputable def EulerPacketPhysicalGevrey.physicalRadius {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k R C S : ℝ) : ℝ

Physical radius, given by sourceInverseRadius C R*(9*C^2*(R+frequencyFactor k D.m₀*S)+2).

Equations

• EulerPacketPhysicalGevrey.physicalRadius D k R C S = EulerPacketInverseFlowGevrey.sourceInverseRadius C R * (9 * C ^ 2 * (R + EulerCylinderPhysicalTensor.frequencyFactor k D.m₀ * S) + 2)

theorem EulerPacketPhysicalGevrey.physicalReconstruction_gevrey {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (he : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (e t) x)) (R C A S : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hA : 0 ≤ A) (hS : 0 ≤ S) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w (e t) x‖ ≤ A * S ^ n * ↑n.factorial ^ 2) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hY : ∀ (t : ↑(Set.Icc 0 D.T)), Differentiable ℝ (Y t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (physicalReconstruction D P κ k e Y t) x‖ ≤ |κ| * 3 * C * A * physicalRadius D k R C S ^ n * ↑n.factorial ^ 2