Actual bounded continuous representatives from smooth L² jets

The bounded map into uniform-norm fields is built from the already proved Sobolev point evaluation. A finite coordinate reconstruction extends it to any finite-dimensional real target. It is used only for qualitative closure; the sharp word estimates use their previously proved direct bounds.

theorem EulerMeanSobolevBoundedField.instMeanSobolevBoundedField1 : Fact (0 < 1)

noncomputable def EulerMeanSobolevBoundedField.sobolevField (u : ↥(EulerCylinderSobolevSpace.SobolevSpace 1 3)) : BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space

The genuine cylinder Sobolev representative, restricted to ordinary space.

Equations

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

theorem EulerMeanSobolevBoundedField.sobolevField_norm (u : ↥(EulerCylinderSobolevSpace.SobolevSpace 1 3)) : ‖sobolevField u‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant 1 3 * ‖u‖

noncomputable def EulerMeanSobolevBoundedField.sobolevLinear : ↥(EulerCylinderSobolevSpace.SobolevSpace 1 3) →ₗ[ℝ] BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space

Sobolev linear, bundling toFun, map_add, map_smul.

Equations

• EulerMeanSobolevBoundedField.sobolevLinear = { toFun := EulerMeanSobolevBoundedField.sobolevField, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerMeanSobolevBoundedField.sobolevMap : ↥(EulerCylinderSobolevSpace.SobolevSpace 1 3) →L[ℝ] BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space

Sobolev evaluation is bounded in the uniform norm, not just pointwise.

Equations

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

noncomputable def EulerMeanSobolevBoundedField.spaceField (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space

Space field, given by sobolevMap (ordinarySobolev 3 A.toLp A.translation_contDiff).

Equations

• EulerMeanSobolevBoundedField.spaceField A = EulerMeanSobolevBoundedField.sobolevMap (EulerMeanSmoothRepresentative.ordinarySobolev 3 A.toLp ⋯)

@[simp]

theorem EulerMeanSobolevBoundedField.spaceField_apply (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : (spaceField A) x = A.field x

theorem EulerMeanSobolevBoundedField.continuous_spaceField {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) : Continuous fun (t : K) => spaceField (A t)

noncomputable def EulerMeanSobolevBoundedField.scalarEmbedding : ℝ →L[ℝ] EulerSmoothLimit.Space

Scalar embedding, given by (ContinuousLinearMap.id ℝ ℝ).smulRight (EuclideanSpace.single (0 : Fin 3) 1).

Equations

• EulerMeanSobolevBoundedField.scalarEmbedding = (ContinuousLinearMap.id ℝ ℝ).smulRight (EuclideanSpace.single 0 1)

noncomputable def EulerMeanSobolevBoundedField.scalarField (A : EulerLpTranslation.SmoothL2Field ℝ) : BoundedContinuousFunction EulerSmoothLimit.Space ℝ

Scalar field, given by (EuclideanSpace.proj (0 : Fin 3) : Space →L[ℝ] ℝ).compLeftContinuousBounded Space (spaceField (mapField scalarEmbedding A)).

Equations

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

@[simp]

theorem EulerMeanSobolevBoundedField.scalarField_apply (A : EulerLpTranslation.SmoothL2Field ℝ) (x : EulerSmoothLimit.Space) : (scalarField A) x = A.field x

theorem EulerMeanSobolevBoundedField.continuous_scalarField {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field ℝ) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) : Continuous fun (t : K) => scalarField (A t)

noncomputable def EulerMeanSobolevBoundedField.coordinate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (i : Fin (Module.finrank ℝ V)) : V →L[ℝ] ℝ

Coordinate, given by ((Module.finBasis ℝ V).coord i).toContinuousLinearMap.

Equations

• EulerMeanSobolevBoundedField.coordinate i = LinearMap.toContinuousLinearMap ((Module.finBasis ℝ V).coord i)

noncomputable def EulerMeanSobolevBoundedField.coordinateVector {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (i : Fin (Module.finrank ℝ V)) : ℝ →L[ℝ] V

Coordinate vector, given by (ContinuousLinearMap.id ℝ ℝ).smulRight (Module.finBasis ℝ V i).

Equations

• EulerMeanSobolevBoundedField.coordinateVector i = (ContinuousLinearMap.id ℝ ℝ).smulRight ((Module.finBasis ℝ V) i)

noncomputable def EulerMeanSobolevBoundedField.finiteField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : EulerLpTranslation.SmoothL2Field V) : BoundedContinuousFunction EulerSmoothLimit.Space V

Reconstruct a bounded field from the finitely many actual scalar coordinates.

Equations

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

@[simp]

theorem EulerMeanSobolevBoundedField.finiteField_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : (finiteField A) x = A.field x

theorem EulerMeanSobolevBoundedField.continuous_finiteField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {K : Type u_2} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) : Continuous fun (t : K) => finiteField (A t)

Continuity of the real L² spatial jets implies continuity in the uniform field norm.