Bounded actual derivative-word blocks on the complete Sobolev scale.

def EulerSobolevWordBlocks.wordBlock (period : ℝ) [Fact (0 < period)] (q n : ℕ) : (Fin n → Fin 4) → ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + n)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

A derivative word as an actual bounded map H^(q+n)→Hq, with its literal differentiation order.

Equations

• EulerSobolevWordBlocks.wordBlock period q 0 x_2 = ContinuousLinearMap.id ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
• EulerSobolevWordBlocks.wordBlock period q n.succ w = EulerSobolevWordBlocks.wordBlock period q n (Fin.init w) ∘SL EulerCylinderSobolevSpace.derivativeOperator period (q + n) (w (Fin.last n))

theorem EulerSobolevWordBlocks.wordBlock_bound (period : ℝ) [Fact (0 < period)] (q n : ℕ) (w : Fin n → Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + n))) : ‖(wordBlock period q n w) u‖ ≤ ‖u‖

Actual word differentiation is contractive between the corresponding array norms.

theorem EulerSobolevWordBlocks.wordBlock_value (period : ℝ) [Fact (0 < period)] (q n : ℕ) (w : Fin n → Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + n))) : EulerCylinderSobolevSpace.value period ((wordBlock period q n w) u) = EulerCylinderSobolevSpace.word period u ⋯ w

The field underlying a derivative block is exactly its genuine derivative-word coordinate.

theorem EulerSobolevWordBlocks.wordBlock_translation (period : ℝ) [Fact (0 < period)] (q n : ℕ) (w : Fin n → Fin 4) (a : EulerLiftedGradientSpace.LiftDomain period) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + n))) : (wordBlock period q n w) ((EulerCylinderSobolevSpace.sobolevTranslation period (q + n) a) u) = (EulerCylinderSobolevSpace.sobolevTranslation period q a) ((wordBlock period q n w) u)

Every derivative block commutes with actual cylinder translation.

theorem EulerSobolevWordBlocks.wordBlock_heat (period : ℝ) [Fact (0 < period)] (q n : ℕ) (w : Fin n → Fin 4) (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + n))) : (wordBlock period q n w) ((EulerSobolevHeat.heatOperator period (q + n) v) u) = (EulerSobolevHeat.heatOperator period q v) ((wordBlock period q n w) u)

Every actual derivative block commutes with the Gaussian heat semigroup.

theorem EulerSobolevWordBlocks.truncate_wordBlock (period : ℝ) [Fact (0 < period)] (q n : ℕ) (w : Fin n → Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + n))) : (EulerCylinderSobolevSpace.truncateOperator period q) ((wordBlock period (q + 1) n w) u) = (wordBlock period q n w) ((EulerCylinderSobolevSpace.restrictOperator period ⋯) u)

Truncating a derivative block agrees with taking the same word after truncating its input.