Actual continuous representatives and point evaluation as bounded linear maps on cylinder H3.

noncomputable def EulerSobolevPointEvaluation.representative (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3

The actual continuous representative of a genuine cylinder H3 field.

Equations

• EulerSobolevPointEvaluation.representative period u = Classical.choose ⋯

theorem EulerSobolevPointEvaluation.representative_continuous (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) : Continuous (representative period u)

The chosen representative is actually continuous.

theorem EulerSobolevPointEvaluation.representative_ae (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] representative period u

The chosen representative agrees almost everywhere with the actual L² field.

theorem EulerSobolevPointEvaluation.representative_eq (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hg : Continuous g) (hrep : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) : representative period u = g

Continuous representatives of the same actual L² field agree pointwise.

theorem EulerSobolevPointEvaluation.representative_bound (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖representative period u x‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 3 * ‖u‖

The actual representative obeys the pointwise H3 evaluation bound at every point.

theorem EulerSobolevPointEvaluation.representative_add (period : ℝ) [Fact (0 < period)] (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) : representative period (u + v) = fun (x : EulerLiftedGradientSpace.LiftDomain period) => representative period u x + representative period v x

Addition of actual H3 fields gives pointwise addition of their continuous representatives.

theorem EulerSobolevPointEvaluation.representative_smul (period : ℝ) [Fact (0 < period)] (c : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) : representative period (c • u) = fun (x : EulerLiftedGradientSpace.LiftDomain period) => c • representative period u x

Scalar multiplication of actual H3 fields gives pointwise scalar multiplication of their continuous representatives.

noncomputable def EulerSobolevPointEvaluation.pointEvaluation (period : ℝ) [Fact (0 < period)] (x : EulerLiftedGradientSpace.LiftDomain period) : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3) →L[ℝ] EulerLiftedGradientSpace.Vector3

Evaluation of the actual continuous representative is a bounded linear map on cylinder H3.

Equations

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

theorem EulerSobolevPointEvaluation.pointEvaluation_eq (period : ℝ) [Fact (0 < period)] (x : EulerLiftedGradientSpace.LiftDomain period) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hg : Continuous g) (hrep : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) : (pointEvaluation period x) u = g x

The bounded evaluation operator returns the value of every actual continuous representative.