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 := SubmoduleClass.module (EulerCylinderSobolevSpace.SobolevSpace period q), norm_smul_le := ⋯ }

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.

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.