A complete cylinder Sobolev space constructed from closed graphs of actual L² derivatives.

@[reducible, inline]

abbrev EulerCylinderSobolevSpace.SobolevWord (q : ℕ) : Type

A coordinate derivative word of length at most the Sobolev order.

Equations

• EulerCylinderSobolevSpace.SobolevWord q = ((n : Fin (q + 1)) × (Fin ↑n → Fin 4))

@[reducible, inline]

abbrev EulerCylinderSobolevSpace.SobolevEdge (q : ℕ) : Type

An edge joining a derivative word to one further coordinate derivative.

Equations

• EulerCylinderSobolevSpace.SobolevEdge q = ((n : Fin q) × (Fin ↑n → Fin 4) × Fin 4)

def EulerCylinderSobolevSpace.emptyWord (q : ℕ) : SobolevWord q

The empty derivative word.

Equations

• EulerCylinderSobolevSpace.emptyWord q = ⟨⟨0, ⋯⟩, Fin.elim0⟩

def EulerCylinderSobolevSpace.edgeParent {q : ℕ} (e : SobolevEdge q) : SobolevWord q

The lower endpoint of a derivative edge.

Equations

• EulerCylinderSobolevSpace.edgeParent e = ⟨⟨↑e.fst, ⋯⟩, e.snd.1⟩

def EulerCylinderSobolevSpace.edgeChild {q : ℕ} (e : SobolevEdge q) : SobolevWord q

The upper endpoint obtained by prepending one derivative direction.

Equations

• EulerCylinderSobolevSpace.edgeChild e = ⟨⟨↑e.fst + 1, ⋯⟩, Fin.cons e.snd.2 e.snd.1⟩

def EulerCylinderSobolevSpace.closedDerivativeGraph (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) : ClosedSubmodule ℝ (↥(EulerLiftedGradientSpace.LiftL2 period) × ↥(EulerLiftedGradientSpace.LiftL2 period))

The closed graph of the actual strong translation derivative.

Equations

• EulerCylinderSobolevSpace.closedDerivativeGraph period a = { toSubmodule := EulerClosedTranslationGraph.translationDerivativeGraph period a, isClosed' := ⋯ }

noncomputable def EulerCylinderSobolevSpace.edgeEvaluation (period : ℝ) [Fact (0 < period)] {q : ℕ} (e : SobolevEdge q) : (SobolevWord q → ↥(EulerLiftedGradientSpace.LiftL2 period)) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period) × ↥(EulerLiftedGradientSpace.LiftL2 period)

Evaluation of the two endpoints of a derivative edge is continuous linear.

Equations

• EulerCylinderSobolevSpace.edgeEvaluation period e = (ContinuousLinearMap.proj (EulerCylinderSobolevSpace.edgeParent e)).prod (ContinuousLinearMap.proj (EulerCylinderSobolevSpace.edgeChild e))

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

The closed linear space of finite arrays satisfying every genuine derivative compatibility.

Equations

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

@[reducible, inline]

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

The actual cylinder Sobolev space, with the complete finite-array norm.

Equations

• EulerCylinderSobolevSpace.SobolevSpace period q = EulerCylinderSobolevSpace.sobolevSubspace period q

@[instance_reducible]

noncomputable instance EulerCylinderSobolevSpace.sobolevNormedAddCommGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(SobolevSpace period q)

The Sobolev norm is the norm inherited from the underlying submodule of derivative arrays.

Equations

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

@[instance_reducible]

noncomputable instance EulerCylinderSobolevSpace.sobolevNormedSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(SobolevSpace period q)

Scalar multiplication uses the same inherited norm as the derivative array.

Equations

• EulerCylinderSobolevSpace.sobolevNormedSpace period q = { toModule := (EulerCylinderSobolevSpace.SobolevSpace period q).normedSpace.toModule, norm_smul_le := ⋯ }

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instNormedAddCommGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instNormedAddCommGroup period q = inferInstance

instance EulerCylinderSobolevSpace.SobolevSpace.instIsTopologicalAddGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : IsTopologicalAddGroup ↥(SobolevSpace period q)

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instUniformSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : UniformSpace ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instUniformSpace period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instMulActionWithZero (period : ℝ) [Fact (0 < period)] (q : ℕ) : MulActionWithZero ℝ ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instMulActionWithZero period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instZero (period : ℝ) [Fact (0 < period)] (q : ℕ) : Zero ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instZero period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instModule (period : ℝ) [Fact (0 < period)] (q : ℕ) : Module ℝ ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instModule period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instTopologicalSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : TopologicalSpace ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instTopologicalSpace period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instSeminormedAddCommGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : SeminormedAddCommGroup ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instSeminormedAddCommGroup period q = NormedAddCommGroup.toSeminormedAddCommGroup

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instDistribMulAction (period : ℝ) [Fact (0 < period)] (q : ℕ) : DistribMulAction ℝ ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instDistribMulAction period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instSMulWithZero (period : ℝ) [Fact (0 < period)] (q : ℕ) : SMulWithZero ℝ ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instSMulWithZero period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instAddMonoid (period : ℝ) [Fact (0 < period)] (q : ℕ) : AddMonoid ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instAddMonoid period q = inferInstance

instance EulerCylinderSobolevSpace.SobolevSpace.instContinuousSub (period : ℝ) [Fact (0 < period)] (q : ℕ) : ContinuousSub ↥(SobolevSpace period q)

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instSMulZeroClass (period : ℝ) [Fact (0 < period)] (q : ℕ) : SMulZeroClass ℝ ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instSMulZeroClass period q = inferInstance

instance EulerCylinderSobolevSpace.SobolevSpace.instIsBoundedSMul (period : ℝ) [Fact (0 < period)] (q : ℕ) : IsBoundedSMul ℝ ↥(SobolevSpace period q)

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instMulAction (period : ℝ) [Fact (0 < period)] (q : ℕ) : MulAction ℝ ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instMulAction period q = inferInstance

instance EulerCylinderSobolevSpace.SobolevSpace.instNormSMulClass (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormSMulClass ℝ ↥(SobolevSpace period q)

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instAddCommMonoid (period : ℝ) [Fact (0 < period)] (q : ℕ) : AddCommMonoid ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instAddCommMonoid period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instSMul (period : ℝ) [Fact (0 < period)] (q : ℕ) : SMul ℝ ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instSMul period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instMetricSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : MetricSpace ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instMetricSpace period q = inferInstance

instance EulerCylinderSobolevSpace.SobolevSpace.instContinuousSMul (period : ℝ) [Fact (0 < period)] (q : ℕ) : ContinuousSMul ℝ ↥(SobolevSpace period q)

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instSeminormedAddGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : SeminormedAddGroup ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instSeminormedAddGroup period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instNorm (period : ℝ) [Fact (0 < period)] (q : ℕ) : Norm ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instNorm period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instNeg (period : ℝ) [Fact (0 < period)] (q : ℕ) : Neg ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instNeg period q = inferInstance

instance EulerCylinderSobolevSpace.SobolevSpace.instContinuousAdd (period : ℝ) [Fact (0 < period)] (q : ℕ) : ContinuousAdd ↥(SobolevSpace period q)

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instAdd (period : ℝ) [Fact (0 < period)] (q : ℕ) : Add ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instAdd period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instAddCommGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : AddCommGroup ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instAddCommGroup period q = inferInstance

instance EulerCylinderSobolevSpace.SobolevSpace.instContinuousConstSMul (period : ℝ) [Fact (0 < period)] (q : ℕ) : ContinuousConstSMul ℝ ↥(SobolevSpace period q)

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instAddGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : AddGroup ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instAddGroup period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instNormedAddGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddGroup ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instNormedAddGroup period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instPseudoMetricSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : PseudoMetricSpace ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instPseudoMetricSpace period q = inferInstance

instance EulerCylinderSobolevSpace.SobolevSpace.instContinuousNeg (period : ℝ) [Fact (0 < period)] (q : ℕ) : ContinuousNeg ↥(SobolevSpace period q)

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instDistribSMul (period : ℝ) [Fact (0 < period)] (q : ℕ) : DistribSMul ℝ ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instDistribSMul period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instSub (period : ℝ) [Fact (0 < period)] (q : ℕ) : Sub ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instSub period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instNormedSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instNormedSpace period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instSubNegMonoid (period : ℝ) [Fact (0 < period)] (q : ℕ) : SubNegMonoid ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instSubNegMonoid period q = inferInstance

@[reducible]

noncomputable instance EulerCylinderSobolevSpace.SobolevSpace.instAddZeroClass (period : ℝ) [Fact (0 < period)] (q : ℕ) : AddZeroClass ↥(SobolevSpace period q)

Equations

• EulerCylinderSobolevSpace.SobolevSpace.instAddZeroClass period q = inferInstance

instance EulerCylinderSobolevSpace.SobolevSpace.instIsUniformAddGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : IsUniformAddGroup ↥(SobolevSpace period q)

theorem EulerCylinderSobolevSpace.sobolev_complete (period : ℝ) [Fact (0 < period)] (q : ℕ) : CompleteSpace ↥(SobolevSpace period q)

Completeness follows from closedness of the derivative graphs in a finite product of L² spaces.

instance EulerCylinderSobolevSpace.SobolevSpace.instCompleteSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : CompleteSpace ↥(SobolevSpace period q)

Shortcut for the completeness of the cylinder Sobolev space.

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

The underlying L² field of a Sobolev derivative array.

Equations

• EulerCylinderSobolevSpace.value period u = ↑u (EulerCylinderSobolevSpace.emptyWord q)

def EulerCylinderSobolevSpace.word (period : ℝ) [Fact (0 < period)] {q n : ℕ} (u : ↥(SobolevSpace period q)) (hn : n ≤ q) (w : Fin n → Fin 4) : ↥(EulerLiftedGradientSpace.LiftL2 period)

A valid derivative word in the array.

Equations

• EulerCylinderSobolevSpace.word period u hn w = ↑u ⟨⟨n, ⋯⟩, w⟩

theorem EulerCylinderSobolevSpace.word_hasDerivAt (period : ℝ) [Fact (0 < period)] {q n : ℕ} (u : ↥(SobolevSpace period q)) (hn : n < q) (w : Fin n → Fin 4) (i : Fin 4) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (word period u ⋯ w)) (word period u ⋯ (Fin.cons i w)) 0

The defining compatibility is a genuine strong derivative of an L² translation orbit.

noncomputable def EulerCylinderSobolevSpace.ofJet (period : ℝ) [Fact (0 < period)] {q : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f) : ↥(SobolevSpace period q)

Every finite strong derivative jet defines an element of the complete Sobolev space.

Equations

• EulerCylinderSobolevSpace.ofJet period J = ⟨fun (w : EulerCylinderSobolevSpace.SobolevWord q) => J.word w.snd, ⋯⟩

@[simp]

theorem EulerCylinderSobolevSpace.value_ofJet (period : ℝ) [Fact (0 < period)] {q : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f) : value period (ofJet period J) = f

The underlying field of the array constructed from a jet is unchanged.

theorem EulerCylinderSobolevSpace.word_has_jet (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) (r n : ℕ) (h : n + r ≤ q) (w : Fin n → Fin 4) : Nonempty (EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection r (word period u ⋯ w))

Every compatible array has a genuine jet of any remaining depth at every word.

noncomputable def EulerCylinderSobolevSpace.toJet (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q (value period u)

A genuine full-depth strong derivative jet reconstructed from a Sobolev array.

Equations

• EulerCylinderSobolevSpace.toJet period u = Classical.choice ⋯

theorem EulerCylinderSobolevSpace.jet_word_eq (period : ℝ) [Fact (0 < period)] {q n : ℕ} (u : ↥(SobolevSpace period q)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q (value period u)) (hn : n ≤ q) (w : Fin n → Fin 4) : J.word w = word period u hn w

Any genuine jet with the correct underlying field agrees with every array coordinate.

theorem EulerCylinderSobolevSpace.toJet_word (period : ℝ) [Fact (0 < period)] {q n : ℕ} (u : ↥(SobolevSpace period q)) (hn : n ≤ q) (w : Fin n → Fin 4) : (toJet period u).word w = word period u hn w

Reconstructing a jet preserves each genuine derivative coordinate.

theorem EulerCylinderSobolevSpace.value_injective (period : ℝ) [Fact (0 < period)] {q : ℕ} : Function.Injective (value period)

A Sobolev array is uniquely determined by its underlying L² field.

@[simp]

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

Reconstructing a jet and then its array is the identity.