Actual pointwise squared metric energy for the difference of viscous corrections.
Exact identification of the nonlinear Sobolev transport with the operator used in metric energy.
theorem
EulerSobolevMetricTransport.transportBilinear_eq_transportOperator
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(hκ : |κ| ≤ 1)
(hm : ‖m‖ ≤ 1)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
EulerCylinderSobolevSpace.value period
(((EulerSobolevTransport.transportBilinear period hq (EulerSobolevTransport.velocityComponents κ m) ⋯) u) v) = (transportOperator period ⋯ κ m ((EulerCylinderSobolevSpace.truncateOperator period q) u))
((EulerCylinderSobolevSpace.restrictOperator period ⋯) v)
The derivative-losing nonlinear transport has exactly the H¹ transport used in the proved metric pairing bound.
@[instance_reducible]
noncomputable def
EulerSobolevDifferenceEnergy.energySobolevGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
The existing Sobolev normed-group instance for the actual difference-energy calculation.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerSobolevDifferenceEnergy.energySobolevSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The existing real Sobolev module instance for the actual difference-energy calculation.
Equations
Instances For
theorem
EulerSobolevDifferenceEnergy.difference_transport_bound
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(t : T)
(K : EulerSpatialSobolevInverse.SmoothCoefficient period)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(Kx Z R : ℝ)
(hKx : ↑K.firstBound ≤ Kx)
(hZ : ‖D.approximation t‖ ≤ Z)
(hu : ‖u‖ ≤ R)
(hsym :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (a b : EulerLiftedGradientSpace.Vector3),
inner ℝ ((K.coefficient x) a) b = inner ℝ a ((K.coefficient x) b))
(hz :
EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
(hud : EulerCylinderSobolevSpace.value period u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
:
|inner ℝ (K.operator (EulerCylinderSobolevSpace.value period (u - v)))
(EulerCylinderSobolevSpace.value period
(((EulerSobolevTransport.transportBilinear period hq (EulerSobolevTransport.velocityComponents D.κ D.direction)
⋯)
(D.approximation t + u))
(u - v)))| ≤ Kx * EulerCorrectionStabilityConstants.velocityBound period q Z R * ‖EulerCylinderSobolevSpace.value period (u - v)‖ ^ 2
Actual Hq transport has the uniform variable-metric pairing bound used for viscosity differences.
theorem
EulerSobolevDifferenceEnergy.difference_heat_bound
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 2 ≤ q)
(K : EulerSpatialSobolevInverse.SmoothCoefficient period)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(c Kx : ℝ)
(hc : 0 < c)
(hKx : ↑K.firstBound ≤ Kx)
(hpos :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (a : EulerLiftedGradientSpace.Vector3),
c ^ 2 * ‖a‖ ^ 2 ≤ inner ℝ ((K.coefficient x) a) a)
:
inner ℝ (K.operator (EulerCylinderSobolevSpace.value period u))
((EulerSobolevHeatGenerator.laplacianEvaluation period q hq) u) ≤ 2 * Kx ^ 2 / c ^ 2 * ‖EulerCylinderSobolevSpace.value period u‖ ^ 2
The actual Sobolev Laplacian has the fixed metric heat bound obtained by integration by parts.