Scalar amplitudes for actual terminal L² data. A unit-input estimate for a genuine linear endpoint map gives the identical coefficient/radius guard for every nonnegative amplitude, including zero.
theorem
EulerLpCylinderTranslation.constantPath_block_le
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
{U : Type u_2}
{ι : Type u_4}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup U]
[NormedSpace ℝ U]
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(q : ℕ)
(Y : ↥(CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (translate P a) Y)
(n : ℕ)
(a : EulerLiftedGradientSpace.LiftTangent)
:
EulerParameterWordGevrey.block directions q
(fun (b : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P b) (ContinuousMap.const K Y)) n a ≤ EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (translate P b) Y) n a
Embedding terminal data as a constant time path has block norm at most one.
theorem
EulerLpCylinderTranslation.terminal_amplitude_bound
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
{U : Type u_2}
{V : Type u_3}
{ι : Type u_4}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup U]
[NormedSpace ℝ U]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(q : ℕ)
(S : ↥(CylinderL2 P U) →L[ℝ] C(K, ↥(CylinderL2 P V)))
(hs :
∀ (Y : ↥(CylinderL2 P U)),
(ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (translate P a) Y) →
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) (S Y))
(R C : ℝ)
(d e : ℕ)
(hunit :
∀ (Y : ↥(CylinderL2 P U)),
(ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (translate P a) Y) →
(∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (translate P a) Y) n 0 ≤ EulerGevrey.majorant R d n) →
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) (S Y)) n 0 ≤ C * EulerGevrey.majorant R e n)
(Y : ↥(CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (translate P a) Y)
(A : ℝ)
(hA : 0 ≤ A)
(hb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (translate P a) Y) n
0 ≤ A * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) (S Y)) n 0 ≤ C * A * EulerGevrey.majorant R e n