Genuine restrictions between any two finite cylinder Sobolev orders.

def EulerCylinderSobolevSpace.restrictIndex {p q : ℕ} (h : q ≤ p) (w : SobolevWord q) : SobolevWord p

The same derivative word at a larger Sobolev order.

Equations

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

noncomputable def EulerCylinderSobolevSpace.restrictOperator (period : ℝ) [Fact (0 < period)] {p q : ℕ} (h : q ≤ p) : ↥(SobolevSpace period p) →L[ℝ] ↥(SobolevSpace period q)

Restriction is a bounded linear map between the actual complete Sobolev spaces.

Equations

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

@[simp]

theorem EulerCylinderSobolevSpace.restrictOperator_apply (period : ℝ) [Fact (0 < period)] {p q : ℕ} (h : q ≤ p) (u : ↥(SobolevSpace period p)) (w : SobolevWord q) : ↑((restrictOperator period h) u) w = ↑u (restrictIndex h w)

@[simp]

theorem EulerCylinderSobolevSpace.value_restrictOperator (period : ℝ) [Fact (0 < period)] {p q : ℕ} (h : q ≤ p) (u : ↥(SobolevSpace period p)) : value period ((restrictOperator period h) u) = value period u

theorem EulerCylinderSobolevSpace.restrictOperator_bound (period : ℝ) [Fact (0 < period)] {p q : ℕ} (h : q ≤ p) (u : ↥(SobolevSpace period p)) : ‖(restrictOperator period h) u‖ ≤ ‖u‖

@[simp]

theorem EulerCylinderSobolevSpace.restrictOperator_self (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) : (restrictOperator period ⋯) u = u

@[simp]

theorem EulerCylinderSobolevSpace.restrictOperator_comp (period : ℝ) [Fact (0 < period)] {p q r : ℕ} (hqp : q ≤ p) (hrq : r ≤ q) (u : ↥(SobolevSpace period p)) : (restrictOperator period hrq) ((restrictOperator period hqp) u) = (restrictOperator period ⋯) u

@[simp]

theorem EulerCylinderSobolevSpace.restrictOperator_truncate (period : ℝ) [Fact (0 < period)] {p q : ℕ} (h : q ≤ p) (u : ↥(SobolevSpace period (p + 1))) : (restrictOperator period h) ((truncateOperator period p) u) = (restrictOperator period ⋯) u

@[simp]

theorem EulerCylinderSobolevSpace.truncate_restrictOperator (period : ℝ) [Fact (0 < period)] {p q : ℕ} (h : q + 1 ≤ p) (u : ↥(SobolevSpace period p)) : (truncateOperator period q) ((restrictOperator period h) u) = (restrictOperator period ⋯) u

theorem EulerCylinderSobolevSpace.restrictOperator_derivative (period : ℝ) [Fact (0 < period)] {p q : ℕ} (h : q ≤ p) (i : Fin 4) (u : ↥(SobolevSpace period (p + 1))) : (restrictOperator period h) ((derivativeOperator period p i) u) = (derivativeOperator period q i) ((restrictOperator period ⋯) u)

Actual restriction and spatial differentiation commute.

theorem EulerCylinderSobolevSpace.restrictOperator_translation (period : ℝ) [Fact (0 < period)] {p q : ℕ} (h : q ≤ p) (a : EulerLiftedGradientSpace.LiftDomain period) (u : ↥(SobolevSpace period p)) : (restrictOperator period h) ((sobolevTranslation period p a) u) = (sobolevTranslation period q a) ((restrictOperator period h) u)

Restriction commutes with every genuine cylinder translation.