Actual coordinate derivatives and truncations between the complete cylinder Sobolev spaces.

def EulerCylinderSobolevSpace.truncateIndex {q : ℕ} (w : SobolevWord q) : SobolevWord (q + 1)

An old word viewed in the next Sobolev order.

Equations

• EulerCylinderSobolevSpace.truncateIndex w = ⟨⟨↑w.fst, ⋯⟩, w.snd⟩

def EulerCylinderSobolevSpace.derivativeIndex {q : ℕ} (i : Fin 4) (w : SobolevWord q) : SobolevWord (q + 1)

Appending a direction indexes a derivative of the corresponding underlying derivative field.

Equations

• EulerCylinderSobolevSpace.derivativeIndex i w = ⟨⟨↑w.fst + 1, ⋯⟩, Fin.snoc w.snd i⟩

noncomputable def EulerCylinderSobolevSpace.truncateOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) : ↥(SobolevSpace period (q + 1)) →L[ℝ] ↥(SobolevSpace period q)

Continuous truncation forgets the highest derivative level.

Equations

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

noncomputable def EulerCylinderSobolevSpace.derivativeOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) (i : Fin 4) : ↥(SobolevSpace period (q + 1)) →L[ℝ] ↥(SobolevSpace period q)

A coordinate derivative is a bounded map from H^(q+1) to H^q.

Equations

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

@[simp]

theorem EulerCylinderSobolevSpace.truncateOperator_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period (q + 1))) (w : SobolevWord q) : ↑((truncateOperator period q) u) w = ↑u (truncateIndex w)

Truncation acts by the literal inclusion of derivative-word coordinates.

@[simp]

theorem EulerCylinderSobolevSpace.derivativeOperator_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (i : Fin 4) (u : ↥(SobolevSpace period (q + 1))) (w : SobolevWord q) : ↑((derivativeOperator period q i) u) w = ↑u (derivativeIndex i w)

A derivative acts by appending its direction to each word.

theorem EulerCylinderSobolevSpace.truncateOperator_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period (q + 1))) : ‖(truncateOperator period q) u‖ ≤ ‖u‖

Truncation is contractive in the complete derivative-array norm.

theorem EulerCylinderSobolevSpace.derivativeOperator_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (i : Fin 4) (u : ↥(SobolevSpace period (q + 1))) : ‖(derivativeOperator period q i) u‖ ≤ ‖u‖

One coordinate derivative has operator bound one between successive Sobolev levels.

@[simp]

theorem EulerCylinderSobolevSpace.value_truncateOperator (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period (q + 1))) : value period ((truncateOperator period q) u) = value period u

Truncation leaves the underlying L² field unchanged.

theorem EulerCylinderSobolevSpace.derivativeOperator_hasDerivAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (i : Fin 4) (u : ↥(SobolevSpace period (q + 1))) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (value period u)) (value period ((derivativeOperator period q i) u)) 0

The derivative operator really differentiates the underlying L² translation orbit.

theorem EulerCylinderSobolevSpace.derivativeOperator_translation (period : ℝ) [Fact (0 < period)] {q : ℕ} (i : Fin 4) (a : EulerLiftedGradientSpace.LiftDomain period) (u : ↥(SobolevSpace period (q + 1))) : (derivativeOperator period q i) ((sobolevTranslation period (q + 1) a) u) = (sobolevTranslation period q a) ((derivativeOperator period q i) u)

Coordinate differentiation commutes with actual Sobolev translation.