Exact differentiated projected-pressure equations for actual translation Sobolev jets.
theorem
EulerPressureJetIdentities.gradientSpace_translation_derivative
(period : ℝ)
[Fact (0 < period)]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(a : EulerLiftedGradientSpace.LiftTangent)
{f f' : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(hf : f ∈ EulerLiftedGradientSpace.gradientSpace period κ m)
(hder :
HasDerivAt
(fun (t : ℝ) =>
(EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f)
f' 0)
:
Strong derivatives preserve the actual closed lifted gradient subspace.
theorem
EulerPressureJetIdentities.SpatialJet.word_unique
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{s t n : ℕ}
{f g : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(J : EulerSpatialSobolevInverse.SpatialJet period directions s f)
(K : EulerSpatialSobolevInverse.SpatialJet period directions t g)
(hfg : f = g)
(hn : n ≤ s)
(hm : n ≤ t)
(w : Fin n → Fin 4)
:
Actual strong derivative words are independent of the chosen derivative witness tree.
theorem
EulerPressureJetIdentities.SpatialJet.word_mem_gradientSpace
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{s n : ℕ}
{f : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(J : EulerSpatialSobolevInverse.SpatialJet period directions s f)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(hf : f ∈ EulerLiftedGradientSpace.gradientSpace period κ m)
(hn : n ≤ s)
(w : Fin n → Fin 4)
:
Every valid word of a gradient-valued Sobolev jet remains in the gradient subspace.
theorem
EulerPressureJetIdentities.SpatialJet.word_mem_divergenceFreeSpace
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{s n : ℕ}
{f : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(J : EulerSpatialSobolevInverse.SpatialJet period directions s f)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(hf : f ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m)
(hn : n ≤ s)
(w : Fin n → Fin 4)
:
Every valid word of a solenoidal Sobolev jet remains genuinely weakly solenoidal.
def
EulerPressureJetIdentities.SpatialJet.map
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
(L : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))
(hL :
∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)),
(EulerLiftedGradientSpace.translation period a) (L f) = L ((EulerLiftedGradientSpace.translation period a) f))
{s : ℕ}
{f : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(J : EulerSpatialSobolevInverse.SpatialJet period directions s f)
:
EulerSpatialSobolevInverse.SpatialJet period directions s (L f)
A bounded operator commuting with actual translations maps genuine spatial jets.
Equations
- One or more equations did not get rendered due to their size.
- EulerPressureJetIdentities.SpatialJet.map L hL (EulerSpatialSobolevInverse.SpatialJet.zero f) = EulerSpatialSobolevInverse.SpatialJet.zero (L f)
Instances For
theorem
EulerPressureJetIdentities.SpatialJet.map_word
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{s n : ℕ}
{f : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(J : EulerSpatialSobolevInverse.SpatialJet period directions s f)
(L : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))
(hL :
∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)),
(EulerLiftedGradientSpace.translation period a) (L f) = L ((EulerLiftedGradientSpace.translation period a) f))
(w : Fin n → Fin 4)
:
theorem
EulerPressureJetIdentities.SpatialJet.pressure_word_projected_equation
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{s n : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
{f : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(K : EulerSpatialSobolevInverse.CoefficientJet period directions s A)
(J : EulerSpatialSobolevInverse.SpatialJet period directions s f)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(c : ℝ)
(hc : 0 < c)
(hpos :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v)
(hn : n ≤ s)
(w : Fin n → Fin 4)
:
(EulerLiftedGradientSpace.gradientProjection period κ m)
((EulerSpatialSobolevInverse.SpatialJet.multiply K
(EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J)).word
w) = (EulerLiftedGradientSpace.gradientProjection period κ m) (J.word w)
At every derivative word, the actual projected equation differentiates exactly.
theorem
EulerPressureJetIdentities.SpatialJet.pressure_word_inverse
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{s n : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
{f : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(K : EulerSpatialSobolevInverse.CoefficientJet period directions s A)
(J : EulerSpatialSobolevInverse.SpatialJet period directions s f)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(c : ℝ)
(hc : 0 < c)
(hpos :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v)
(hn : n ≤ s)
(w : Fin n → Fin 4)
:
(EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J).word w = A.pressure κ m c hc hpos
(J.word w - ((EulerSpatialSobolevInverse.SpatialJet.multiply K
(EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J)).word
w - A.operator ((EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J).word w)))
The actual derivative word is the coercive inverse applied to its differentiated source minus the genuine product commutator.
theorem
EulerPressureJetIdentities.SpatialJet.pressure_word_norm_le
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{s n : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
{f : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(K : EulerSpatialSobolevInverse.CoefficientJet period directions s A)
(J : EulerSpatialSobolevInverse.SpatialJet period directions s f)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(c : ℝ)
(hc : 0 < c)
(hpos :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v)
(hn : n ≤ s)
(w : Fin n → Fin 4)
:
‖(EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J).word w‖ ≤ c⁻¹ * (‖J.word w‖ + ‖(EulerSpatialSobolevInverse.SpatialJet.multiply K
(EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J)).word
w - A.operator ((EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J).word w)‖)
The rigorous triangular pressure estimate before its product commutator is summed.