Continuous operators and exact norm comparisons on the actual complete cylinder Sobolev spaces.

noncomputable def EulerCylinderSobolevSpace.arrayOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) : ↥(SobolevSpace period q) →L[ℝ] SobolevWord q → ↥(EulerLiftedGradientSpace.LiftL2 period)

The continuous inclusion of the Sobolev space into its finite derivative array.

Equations

• EulerCylinderSobolevSpace.arrayOperator period q = (↑(EulerCylinderSobolevSpace.sobolevSubspace period q)).subtypeL

noncomputable def EulerCylinderSobolevSpace.valueOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) : ↥(SobolevSpace period q) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Continuous evaluation of the underlying L² field.

Equations

• EulerCylinderSobolevSpace.valueOperator period q = ContinuousLinearMap.proj (EulerCylinderSobolevSpace.emptyWord q) ∘SL EulerCylinderSobolevSpace.arrayOperator period q

noncomputable def EulerCylinderSobolevSpace.wordOperator (period : ℝ) [Fact (0 < period)] {q : ℕ} (w : SobolevWord q) : ↥(SobolevSpace period q) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Continuous evaluation of one actual derivative coordinate.

Equations

• EulerCylinderSobolevSpace.wordOperator period w = ContinuousLinearMap.proj w ∘SL EulerCylinderSobolevSpace.arrayOperator period q

theorem EulerCylinderSobolevSpace.word_norm_le (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) (w : SobolevWord q) : ‖↑u w‖ ≤ ‖u‖

The L² norm of each genuine derivative is bounded by the complete Sobolev norm.

theorem EulerCylinderSobolevSpace.value_norm_le (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) : ‖value period u‖ ≤ ‖u‖

The underlying L² evaluation is contractive.

noncomputable def EulerCylinderSobolevSpace.sumNorm (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) : ℝ

The sum of actual derivative norms, in the source's Sobolev convention.

Equations

• EulerCylinderSobolevSpace.sumNorm period u = ∑ w : EulerCylinderSobolevSpace.SobolevWord q, ‖↑u w‖

theorem EulerCylinderSobolevSpace.norm_le_sumNorm (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) : ‖u‖ ≤ sumNorm period u

The complete-array norm is bounded by the source's derivative sum.

theorem EulerCylinderSobolevSpace.sumNorm_le_card_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) : sumNorm period u ≤ ↑(Fintype.card (SobolevWord q)) * ‖u‖

The source's derivative sum is bounded by a fixed Sobolev-order multiple of the complete norm.

theorem EulerCylinderSobolevSpace.sumNorm_eq_jet (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) : sumNorm period u = (toJet period u).sobolevNorm

The derivative sum is exactly the norm of the reconstructed genuine strong jet.

noncomputable def EulerCylinderSobolevSpace.liftOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) : ↥(SobolevSpace period q) →L[ℝ] ↥(SobolevSpace period q)

A translation-commuting L² operator acts on every actual derivative coordinate.

Equations

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

@[simp]

theorem EulerCylinderSobolevSpace.liftOperator_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) (u : ↥(SobolevSpace period q)) (w : SobolevWord q) : ↑((liftOperator period q A hA) u) w = A (↑u w)

A lifted operator applies the same L² operator to each derivative coordinate.

theorem EulerCylinderSobolevSpace.liftOperator_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) (u : ↥(SobolevSpace period q)) : ‖(liftOperator period q A hA) u‖ ≤ ‖A‖ * ‖u‖

The lifted Sobolev operator has the same uniform bound as its L² action.

theorem EulerCylinderSobolevSpace.norm_liftOperator_le (period : ℝ) [Fact (0 < period)] (q : ℕ) (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) : ‖liftOperator period q A hA‖ ≤ ‖A‖

The operator norm bound for an operator lifted to the complete Sobolev space.

@[simp]

theorem EulerCylinderSobolevSpace.value_liftOperator (period : ℝ) [Fact (0 < period)] {q : ℕ} (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) (u : ↥(SobolevSpace period q)) : value period ((liftOperator period q A hA) u) = A (value period u)

The action on the underlying field is exactly the original L² operator.

theorem EulerCylinderSobolevSpace.translations_commute (period : ℝ) [Fact (0 < period)] (a b : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerLiftedGradientSpace.translation period a) ((EulerLiftedGradientSpace.translation period b) f) = (EulerLiftedGradientSpace.translation period b) ((EulerLiftedGradientSpace.translation period a) f)

Translations commute in the cylinder's additive group.

noncomputable def EulerCylinderSobolevSpace.sobolevTranslation (period : ℝ) [Fact (0 < period)] (q : ℕ) (a : EulerLiftedGradientSpace.LiftDomain period) : ↥(SobolevSpace period q) →L[ℝ] ↥(SobolevSpace period q)

Actual cylinder translation as a bounded operator on the complete Sobolev space.

Equations

• EulerCylinderSobolevSpace.sobolevTranslation period q a = EulerCylinderSobolevSpace.liftOperator period q (EulerLiftedGradientSpace.translation period a).toContinuousLinearMap ⋯

theorem EulerCylinderSobolevSpace.sobolevTranslation_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (a : EulerLiftedGradientSpace.LiftDomain period) (u : ↥(SobolevSpace period q)) : ‖(sobolevTranslation period q a) u‖ = ‖u‖

Cylinder translation preserves the complete Sobolev norm exactly.

theorem EulerCylinderSobolevSpace.sobolevTranslation_continuous (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) : Continuous fun (a : EulerLiftedGradientSpace.LiftDomain period) => (sobolevTranslation period q a) u

The translation action is strongly continuous in the complete Sobolev topology.