Finite spatial Sobolev jets in the actual lifted L² space. Jet entries are actual strong translation derivatives and therefore genuine weak derivatives. The pressure jet is constructed, rather than assumed, from coercivity and pointwise smooth coefficient data.

@[instance_reducible]

noncomputable def EulerSpatialSobolevInverse.coefficientValueNormedGroup : NormedAddCommGroup (EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)

The existing Mathlib normed group instance for matrix coefficients, named to keep inference shallow.

Equations

• EulerSpatialSobolevInverse.coefficientValueNormedGroup = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

noncomputable def EulerSpatialSobolevInverse.coefficientValueNormedSpace : NormedSpace ℝ (EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)

The existing Mathlib real normed-space instance for matrix coefficients.

Equations

• EulerSpatialSobolevInverse.coefficientValueNormedSpace = ContinuousLinearMap.toNormedSpace

@[instance_reducible]

noncomputable def EulerSpatialSobolevInverse.coefficientFirstNormedGroup : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)

The existing Mathlib normed group instance for first coefficient derivatives.

Equations

• EulerSpatialSobolevInverse.coefficientFirstNormedGroup = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

noncomputable def EulerSpatialSobolevInverse.coefficientFirstNormedSpace : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)

The existing Mathlib real normed-space instance for first coefficient derivatives.

Equations

• EulerSpatialSobolevInverse.coefficientFirstNormedSpace = ContinuousLinearMap.toNormedSpace

structure EulerSpatialSobolevInverse.SmoothCoefficient (period : ℝ) : Type

A bounded smooth pointwise coefficient field with quantitative first and second derivatives.

• coefficient : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3

  The actual pointwise coefficient matrix field.

• smooth (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period self.coefficient x)
• bound : NNReal

  A uniform operator-norm bound for the coefficient field.

• norm_bound (x : EulerLiftedGradientSpace.LiftDomain period) : ‖self.coefficient x‖ ≤ ↑self.bound
• firstBound : NNReal

  A uniform norm bound for the first covering derivative.

• norm_first (x : EulerLiftedGradientSpace.LiftDomain period) : ‖fderiv ℝ (EulerMetricTransport.localFieldLift period self.coefficient x) 0‖ ≤ ↑self.firstBound
• secondBound : NNReal

  A uniform norm bound for the second covering derivative.

• norm_second (x : EulerLiftedGradientSpace.LiftDomain period) (y : EulerLiftedGradientSpace.LiftTangent) : ‖fderiv ℝ (fderiv ℝ (EulerMetricTransport.localFieldLift period self.coefficient x)) y‖ ≤ ↑self.secondBound

theorem EulerSpatialSobolevInverse.SmoothCoefficient.measurable {period : ℝ} [Fact (0 < period)] (A : SmoothCoefficient period) : MeasureTheory.AEStronglyMeasurable A.coefficient (EulerLiftedGradientSpace.liftMeasure period)

noncomputable def EulerSpatialSobolevInverse.SmoothCoefficient.operator {period : ℝ} [Fact (0 < period)] (A : SmoothCoefficient period) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Actual multiplication by the coefficient field in L².

Equations

• A.operator = EulerLiftedPressure.coefficientOperator A.coefficient ⋯ A.bound ⋯

theorem EulerSpatialSobolevInverse.SmoothCoefficient.operator_ae {period : ℝ} [Fact (0 < period)] (A : SmoothCoefficient period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↑↑(A.operator f) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => (A.coefficient x) (↑↑f x)

theorem EulerSpatialSobolevInverse.SmoothCoefficient.operator_norm {period : ℝ} [Fact (0 < period)] (A : SmoothCoefficient period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖A.operator f‖ ≤ ↑A.bound * ‖f‖

noncomputable def EulerSpatialSobolevInverse.SmoothCoefficient.pressure {period : ℝ} [Fact (0 < period)] (A : SmoothCoefficient period) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The Lax–Milgram pressure associated with this actual coefficient.

Equations

• A.pressure κ m c hc hpos f = EulerPressureSpatialRegularity.liftedPressure period κ m A.coefficient ⋯ A.bound ⋯ c hc hpos f

theorem EulerSpatialSobolevInverse.SmoothCoefficient.pressure_norm {period : ℝ} [Fact (0 < period)] (A : SmoothCoefficient period) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖A.pressure κ m c hc hpos f‖ ≤ c⁻¹ * ‖f‖

theorem EulerSpatialSobolevInverse.SmoothCoefficient.derivative_operator_eq {period : ℝ} [Fact (0 < period)] (A B : SmoothCoefficient period) (a : EulerLiftedGradientSpace.LiftTangent) (hB : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), B.coefficient x = EulerTransportDerivatives.fieldDerivative period a A.coefficient x) : EulerLiftedPressure.coefficientOperator (EulerPressureSpatialRegularity.translatedCoefficientDerivative period a A.coefficient 0) ⋯ (A.firstBound * ‖a‖₊) ⋯ = B.operator

theorem EulerSpatialSobolevInverse.SmoothCoefficient.operator_translation_hasDerivAt {period : ℝ} [Fact (0 < period)] (A : SmoothCoefficient period) (a : EulerLiftedGradientSpace.LiftTangent) : HasDerivAt (fun (t : ℝ) => EulerLiftedPressure.coefficientOperator (EulerPressureSpatialRegularity.translatedCoefficient period (EulerPressureSpatialRegularity.translationPath period a t) A.coefficient) ⋯ A.bound ⋯) (EulerLiftedPressure.coefficientOperator (EulerPressureSpatialRegularity.translatedCoefficientDerivative period a A.coefficient 0) ⋯ (A.firstBound * ‖a‖₊) ⋯) 0

theorem EulerSpatialSobolevInverse.SmoothCoefficient.product_hasDerivAt {period : ℝ} [Fact (0 < period)] (A B : SmoothCoefficient period) (a : EulerLiftedGradientSpace.LiftTangent) (hB : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), B.coefficient x = EulerTransportDerivatives.fieldDerivative period a A.coefficient x) (f f' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f) f' 0) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) (A.operator f)) (A.operator f' + B.operator f) 0

theorem EulerSpatialSobolevInverse.SmoothCoefficient.pressure_hasDerivAt {period : ℝ} [Fact (0 < period)] (A B : SmoothCoefficient period) (a : EulerLiftedGradientSpace.LiftTangent) (hB : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), B.coefficient x = EulerTransportDerivatives.fieldDerivative period a A.coefficient x) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (f f' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f) f' 0) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) (A.pressure κ m c hc hpos f)) (A.pressure κ m c hc hpos (f' - B.operator (A.pressure κ m c hc hpos f))) 0

inductive EulerSpatialSobolevInverse.SpatialJet (period : ℝ) [Fact (0 < period)] (directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent) : ℕ → ↥(EulerLiftedGradientSpace.LiftL2 period) → Type

A finite tree of actual strong translation derivatives of an L² field.

• zero {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : SpatialJet period directions 0 f
• succ {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (derivatives : Fin 4 → ↥(EulerLiftedGradientSpace.LiftL2 period)) (lower : (i : Fin 4) → SpatialJet period directions n (derivatives i)) (hasDeriv : ∀ (i : Fin 4), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (directions i) t)) f) (derivatives i) 0) : SpatialJet period directions (n + 1) f

inductive EulerSpatialSobolevInverse.CoefficientJet (period : ℝ) (directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent) : ℕ → SmoothCoefficient period → Type

A finite tree of actual coefficient derivatives, with bounded smooth data at every node.

• zero {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} (A : SmoothCoefficient period) : CoefficientJet period directions 0 A
• succ {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} (derivatives : Fin 4 → SmoothCoefficient period) (lower : (i : Fin 4) → CoefficientJet period directions n (derivatives i)) (derivative_eq : ∀ (i : Fin 4) (x : EulerLiftedGradientSpace.LiftDomain period), (derivatives i).coefficient x = EulerTransportDerivatives.fieldDerivative period (directions i) A.coefficient x) : CoefficientJet period directions (n + 1) A

def EulerSpatialSobolevInverse.SpatialJet.truncate {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions (n + 1) f) : SpatialJet period directions n f

Forget the highest derivative order of a genuine spatial jet.

Equations

• x.truncate = EulerSpatialSobolevInverse.SpatialJet.zero f
• (EulerSpatialSobolevInverse.SpatialJet.succ df lower hd).truncate = EulerSpatialSobolevInverse.SpatialJet.succ df (fun (i : Fin 4) => (lower i).truncate) hd

def EulerSpatialSobolevInverse.SpatialJet.sobolevNorm {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions n f) : ℝ

The sum of all derivative-word L² norms represented by the jet.

Equations

• (EulerSpatialSobolevInverse.SpatialJet.zero f).sobolevNorm = ‖f‖
• (EulerSpatialSobolevInverse.SpatialJet.succ derivatives lower hasDeriv).sobolevNorm = ‖f‖ + ∑ i : Fin 4, (lower i).sobolevNorm

theorem EulerSpatialSobolevInverse.SpatialJet.nonneg {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions n f) : 0 ≤ J.sobolevNorm

theorem EulerSpatialSobolevInverse.SpatialJet.value_norm_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions n f) : ‖f‖ ≤ J.sobolevNorm

theorem EulerSpatialSobolevInverse.SpatialJet.truncate_norm_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions (n + 1) f) : J.truncate.sobolevNorm ≤ J.sobolevNorm

theorem EulerSpatialSobolevInverse.SpatialJet.lower_norm_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (df : Fin 4 → ↥(EulerLiftedGradientSpace.LiftL2 period)) (lower : (i : Fin 4) → SpatialJet period directions n (df i)) (hd : ∀ (i : Fin 4), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (directions i) t)) f) (df i) 0) (i : Fin 4) : (lower i).sobolevNorm ≤ (succ df lower hd).sobolevNorm

def EulerSpatialSobolevInverse.SpatialJet.add {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions n f) (K : SpatialJet period directions n g) : SpatialJet period directions n (f + g)

Addition preserves the actual strong derivatives recorded in a spatial jet.

Equations

• One or more equations did not get rendered due to their size.
• (EulerSpatialSobolevInverse.SpatialJet.zero f).add (EulerSpatialSobolevInverse.SpatialJet.zero g) = EulerSpatialSobolevInverse.SpatialJet.zero (f + g)

def EulerSpatialSobolevInverse.SpatialJet.sub {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions n f) (K : SpatialJet period directions n g) : SpatialJet period directions n (f - g)

Subtraction preserves the actual strong derivatives recorded in a spatial jet.

Equations

• One or more equations did not get rendered due to their size.
• (EulerSpatialSobolevInverse.SpatialJet.zero f).sub (EulerSpatialSobolevInverse.SpatialJet.zero g) = EulerSpatialSobolevInverse.SpatialJet.zero (f - g)

theorem EulerSpatialSobolevInverse.SpatialJet.add_norm_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions n f) (K : SpatialJet period directions n g) : (J.add K).sobolevNorm ≤ J.sobolevNorm + K.sobolevNorm

theorem EulerSpatialSobolevInverse.SpatialJet.sub_norm_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions n f) (K : SpatialJet period directions n g) : (J.sub K).sobolevNorm ≤ J.sobolevNorm + K.sobolevNorm

def EulerSpatialSobolevInverse.CoefficientJet.truncate {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} (J : CoefficientJet period directions (n + 1) A) : CoefficientJet period directions n A

Forget the highest derivative level while retaining the original coefficient.

Equations

• x.truncate = EulerSpatialSobolevInverse.CoefficientJet.zero A
• (EulerSpatialSobolevInverse.CoefficientJet.succ dA lower hd).truncate = EulerSpatialSobolevInverse.CoefficientJet.succ dA (fun (i : Fin 4) => (lower i).truncate) hd

@[irreducible]

def EulerSpatialSobolevInverse.CoefficientJet.productConstant {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} (J : CoefficientJet period directions n A) : ℝ

A finite polynomial bound for multiplication in the jet Sobolev norm.

Equations

• One or more equations did not get rendered due to their size.
• (EulerSpatialSobolevInverse.CoefficientJet.zero A).productConstant = ↑A.bound

theorem EulerSpatialSobolevInverse.CoefficientJet.productConstant_nonneg {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} (J : CoefficientJet period directions n A) : 0 ≤ J.productConstant

@[irreducible]

def EulerSpatialSobolevInverse.SpatialJet.multiply {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : CoefficientJet period directions n A) (J : SpatialJet period directions n f) : SpatialJet period directions n (A.operator f)

Construct every finite-order derivative of actual coefficient multiplication.

Equations

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

theorem EulerSpatialSobolevInverse.SpatialJet.multiply_norm_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : CoefficientJet period directions n A) (J : SpatialJet period directions n f) : (multiply K J).sobolevNorm ≤ K.productConstant * J.sobolevNorm

@[irreducible]

def EulerSpatialSobolevInverse.CoefficientJet.pressureConstant {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} (J : CoefficientJet period directions n A) (c : ℝ) : ℝ

The explicit finite-order inverse constant obtained from coercivity and coefficient products.

Equations

• One or more equations did not get rendered due to their size.
• (EulerSpatialSobolevInverse.CoefficientJet.zero A).pressureConstant c = c⁻¹

theorem EulerSpatialSobolevInverse.CoefficientJet.pressureConstant_nonneg {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} (J : CoefficientJet period directions n A) (c : ℝ) (hc : 0 < c) : 0 ≤ J.pressureConstant c

@[irreducible]

def EulerSpatialSobolevInverse.SpatialJet.solvePressure {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : CoefficientJet period directions n A) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (J : SpatialJet period directions n f) : SpatialJet period directions n (A.pressure κ m c hc hpos f)

Construct a genuine pressure Sobolev jet at every finite order.

Equations

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

theorem EulerSpatialSobolevInverse.SpatialJet.solvePressure_norm_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {n : ℕ} {A : SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : CoefficientJet period directions n A) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (J : SpatialJet period directions n f) : (solvePressure K κ m c hc hpos J).sobolevNorm ≤ K.pressureConstant c * J.sobolevNorm

@[irreducible]

def EulerSpatialSobolevInverse.SpatialJet.word {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions s f) {n : ℕ} (w : Fin n → Fin 4) : ↥(EulerLiftedGradientSpace.LiftL2 period)

A derivative word, ordered with its head differentiated last; invalid orders return zero.

Equations

• J.word w_2 = f
• (EulerSpatialSobolevInverse.SpatialJet.zero f).word w_2 = 0
• (EulerSpatialSobolevInverse.SpatialJet.succ derivatives lower hasDeriv).word w_2 = (lower (w_2 (Fin.last n_2))).word (Fin.init w_2)

@[simp]

theorem EulerSpatialSobolevInverse.SpatialJet.word_zero {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions s f) (w : Fin 0 → Fin 4) : J.word w = f

@[simp]

theorem EulerSpatialSobolevInverse.SpatialJet.word_succ {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (df : Fin 4 → ↥(EulerLiftedGradientSpace.LiftL2 period)) (lower : (i : Fin 4) → SpatialJet period directions s (df i)) (hd : ∀ (i : Fin 4), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (directions i) t)) f) (df i) 0) (w : Fin (n + 1) → Fin 4) : (succ df lower hd).word w = (lower (w (Fin.last n))).word (Fin.init w)

theorem EulerSpatialSobolevInverse.SpatialJet.word_hasDerivAt {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions s f) (hn : n < s) (w : Fin n → Fin 4) (i : Fin 4) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (directions i) t)) (J.word w)) (J.word (Fin.cons i w)) 0

def EulerSpatialSobolevInverse.SpatialJet.wordSnocEquiv (n : ℕ) : (Fin (n + 1) → Fin 4) ≃ Fin 4 × (Fin n → Fin 4)

Split a coordinate word into its last direction and its initial word.

Equations

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

theorem EulerSpatialSobolevInverse.SpatialJet.sum_word_succ {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (df : Fin 4 → ↥(EulerLiftedGradientSpace.LiftL2 period)) (lower : (i : Fin 4) → SpatialJet period directions s (df i)) (hd : ∀ (i : Fin 4), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (directions i) t)) f) (df i) 0) : ∑ w : Fin (n + 1) → Fin 4, ‖(succ df lower hd).word w‖ = ∑ i : Fin 4, ∑ w : Fin n → Fin 4, ‖(lower i).word w‖

The sum over words of positive length is the sum over final directions and initial words.

theorem EulerSpatialSobolevInverse.SpatialJet.sobolevNorm_eq_sum_words {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : SpatialJet period directions s f) : J.sobolevNorm = ∑ n ∈ Finset.range (s + 1), ∑ w : Fin n → Fin 4, ‖J.word w‖

The recursive jet norm equals the explicit sum of the norms of all coordinate words.