Actual continuous L² paths for every ordered cylinder derivative.
noncomputable def
EulerCylinderSmoothOrbit.wordPath
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
{n : ℕ}
(w : Fin n → Fin 4)
:
The actual uniform-time derivative word, evaluated at the untranslated path.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCylinderSmoothOrbit.wordPath_apply
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
{n : ℕ}
(w : Fin n → Fin 4)
(t : K)
:
theorem
EulerCylinderSmoothOrbit.wordPath_translation
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
{n : ℕ}
(w : Fin n → Fin 4)
(a : EulerLiftedGradientSpace.LiftTangent)
:
theorem
EulerCylinderSmoothOrbit.wordPath_orbit
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
{n : ℕ}
(w : Fin n → Fin 4)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (wordPath P p w)
theorem
EulerCylinderSmoothOrbit.wordPath_ae
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
{n : ℕ}
(w : Fin n → Fin 4)
(t : K)
:
↑↑((wordPath P p w) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerCylinderSobolev.iteratedFieldDerivative P w (pointField P p hp t)
theorem
EulerCylinderSmoothOrbit.pointField_wordPath
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
{n : ℕ}
(w : Fin n → Fin 4)
(t : K)
:
pointField P (wordPath P p w) ⋯ t = EulerCylinderSobolev.iteratedFieldDerivative P w (pointField P p hp t)
The new path represents the literal derivative of the old classical field.
theorem
EulerCylinderSmoothOrbit.wordPath_eq_sobolev
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(q : ℕ)
{n : ℕ}
(w : Fin n → Fin 4)
(t : K)
:
EulerCylinderSobolevSpace.value P ((EulerSobolevWordBlocks.wordBlock P q n w) ((sobolevPath P (q + n) p hp) t)) = (wordPath P p w) t
noncomputable def
EulerCylinderSmoothOrbit.derivativePath
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(i : Fin 4)
:
A single spatial or angular derivative retains an actual continuous-time L² path.
Equations
- EulerCylinderSmoothOrbit.derivativePath P p i = EulerCylinderSmoothOrbit.wordPath P p fun (x : Fin 1) => i
Instances For
theorem
EulerCylinderSmoothOrbit.derivativePath_translation
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(i : Fin 4)
(a : EulerLiftedGradientSpace.LiftTangent)
:
theorem
EulerCylinderSmoothOrbit.derivativePath_orbit
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(i : Fin 4)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (derivativePath P p i)
theorem
EulerCylinderSmoothOrbit.pointField_derivativePath
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(i : Fin 4)
(t : K)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
pointField P (derivativePath P p i) ⋯ t x = (EulerLiftedWeakDerivative.fieldFDeriv P (pointField P p hp t) x) (EulerCylinderSobolev.standardDirection i)
theorem
EulerCylinderSmoothOrbit.derivativePath_block_bound
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(i : Fin 4)
(q n : ℕ)
(a : EulerLiftedGradientSpace.LiftTangent)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (b : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P b) (derivativePath P p i))
n a ≤ EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) (n + 1) a
Differentiation uses one external word, with no dimension-dependent radius loss.
theorem
EulerCylinderSmoothOrbit.derivativePath_majorant
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(i : Fin 4)
(q : ℕ)
(R D : ℝ)
(d : ℕ)
(hb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) n 0 ≤ D * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (derivativePath P p i))
n 0 ≤ D * EulerGevrey.majorant R (d + 1) n
theorem
EulerCylinderSmoothOrbit.wordPath_hasDerivWithinAt
(P : ℝ)
[Fact (0 < P)]
(T : ℝ)
(hT : 0 ≤ T)
(u f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) u)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT u) (f t) (Set.Icc 0 T) ↑t)
{n : ℕ}
(w : Fin n → Fin 4)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (wordPath P u w)) ((wordPath P f w) t) (Set.Icc 0 T) ↑t
Every constructed derivative path has the derivative of the actual time equation.