A fixed polynomial frequency loss for every actual physical spatial derivative of a reconstructed lifted field.
noncomputable def
EulerPacketPhysicalGevrey.physicalRadiusCost
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(R C S : ℝ)
:
Physical radius cost, given by sourceInverseRadius C R*(9*C^2*(R + (‖coordinateEquiv.symm.toContinuousLinearMap‖*(1+‖D.m₀‖))*S)+2).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketPhysicalGevrey.physicalRadiusCost_nonneg
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(R C S : ℝ)
(hR : 0 ≤ R)
(hS : 0 ≤ S)
:
theorem
EulerPacketPhysicalGevrey.physicalRadius_le_linear
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(k R C S : ℝ)
(hk : 1 ≤ k)
(hR : 0 ≤ R)
(hS : 0 ≤ S)
:
noncomputable def
EulerPacketPhysicalGevrey.physicalFixedCost
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(R C S : ℝ)
(n : ℕ)
:
Physical fixed cost, given by 3*C*(physicalRadiusCost D R C S)^n*(n.factorial : ℝ)^2.
Equations
- EulerPacketPhysicalGevrey.physicalFixedCost D R C S n = 3 * C * EulerPacketPhysicalGevrey.physicalRadiusCost D R C S ^ n * ↑n.factorial ^ 2
Instances For
theorem
EulerPacketPhysicalGevrey.physicalFixedCost_nonneg
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(R C S : ℝ)
(n : ℕ)
(hR : 0 ≤ R)
(hC : 0 ≤ C)
(hS : 0 ≤ S)
:
theorem
EulerPacketPhysicalGevrey.physicalReconstruction_power_bound
{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)
(hk : 1 ≤ k)
(hκ : |κ| ≤ 1)
(n : ℕ)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
‖iteratedFDeriv ℝ n (physicalReconstruction D P κ k e Y t) x‖ ≤ physicalFixedCost D R C S n * A * k ^ n