Actual fixed-Hq mixed-word estimates for unit terminal data. The spatial radius is unchanged; the coordinate/velocity use two shifts and the true time derivative uses three. Every inverse guard is source-only.
theorem
EulerCylinderDirichlet.Coefficients.EndpointBudget.constant_unit_bound
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{D : Coefficients T U E}
{ι : Type u_3}
[Fintype ι]
{q : ℕ}
(L : D.EndpointBudget ι q)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y) n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (ContinuousMap.const (↑(Set.Icc 0 T)) (T⁻¹ • Y)))
n 0 ≤ T⁻¹ * EulerGevrey.majorant L.R d n
theorem
EulerCylinderDirichlet.Coefficients.EndpointBudget.forcing_unit_bound
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{D : Coefficients T U E}
{ι : Type u_3}
[Fintype ι]
{q : ℕ}
(L : D.EndpointBudget ι q)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y) n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((endpointForcing P D) Y))
n 0 ≤ endpointForcingCost ι q T L.Rc L.C₁ * EulerGevrey.majorant L.R d n
theorem
EulerCylinderDirichlet.Coefficients.EndpointBudget.coordinate_unit_bound
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{D : Coefficients T U E}
{ι : Type u_3}
[Fintype ι]
{q : ℕ}
(L : D.EndpointBudget ι q)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y) n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((endpointCoordinate P D) Y))
n 0 ≤ L.coordinateCost * EulerGevrey.majorant L.R (d + 2) n
theorem
EulerCylinderDirichlet.Coefficients.EndpointBudget.acceleration_unit_bound
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{D : Coefficients T U E}
{ι : Type u_3}
[Fintype ι]
{q : ℕ}
(L : D.EndpointBudget ι q)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y) n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((endpointAcceleration P D) Y))
n 0 ≤ EulerGevrey.majorant L.R (d + 3) n
theorem
EulerCylinderDirichlet.Coefficients.EndpointBudget.velocity_unit_bound
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{D : Coefficients T U E}
{ι : Type u_3}
[Fintype ι]
{q : ℕ}
(L : D.EndpointBudget ι q)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y) n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((endpointVelocity P D) Y))
n 0 ≤ L.velocityCost * EulerGevrey.majorant L.R (d + 2) n
theorem
EulerCylinderDirichlet.Coefficients.EndpointBudget.derivative_unit_bound
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{D : Coefficients T U E}
{ι : Type u_3}
[Fintype ι]
{q : ℕ}
(L : D.EndpointBudget ι q)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(d : ℕ)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y) n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((endpointDerivative P D) Y))
n 0 ≤ L.derivativeCost * EulerGevrey.majorant L.R (d + 3) n