Jointly continuous scalar representatives of actual smooth cylinder L² paths.
noncomputable def
EulerCylinderScalarPrimitive.scalarPointField
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(t : K)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
A fixed norm-one embedding lets the existing bounded H3 evaluation recover the genuine scalar field without making a new representative choice.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCylinderScalarPrimitive.scalarPointField_joint_continuous
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
:
Continuous fun (z : K × EulerLiftedGradientSpace.LiftDomain P) => scalarPointField P p hp z.1 z.2
theorem
EulerCylinderScalarPrimitive.scalarPointField_smooth
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(t : K)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (scalarPointField P p hp t) x)
theorem
EulerCylinderScalarPrimitive.scalarPointField_continuous
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(t : K)
:
Continuous (scalarPointField P p hp t)
theorem
EulerCylinderScalarPrimitive.scalarPointField_ae
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(t : K)
:
↑↑(p t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] scalarPointField P p hp t
theorem
EulerCylinderScalarPrimitive.scalarPointField_eq
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(t : K)
(f : EulerLiftedGradientSpace.LiftDomain P → ℝ)
(hf : Continuous f)
(hrep : ↑↑(p t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f)
:
Any continuous scalar representative is this same jointly continuous field.