Genuine fixed-Sobolev bounds for the cylinder history inverse #
The actual mixed translation orbit has identical fixed-base word norms at every translation. Thus the forcing needs a bound only at zero. Coefficient jets lift to L² operator paths with constant one, and the true fixed-space inverse adds one shift while preserving the external radius.
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds1
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
:
Cache the standard NormedAddCommGroup (CylinderL2 P U) instance to shorten typeclass
synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds2
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
:
Cache the standard NormedSpace ℝ (CylinderL2 P U) instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds3
(P : ℝ)
[Fact (0 < P)]
{E : Type u_2}
[NormedAddCommGroup E]
:
Cache the standard NormedAddCommGroup (CylinderL2 P E) instance to shorten typeclass
synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds4
(P : ℝ)
[Fact (0 < P)]
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedSpace ℝ (CylinderL2 P E) instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds5
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedAddCommGroup (CylinderL2 P U →L[ℝ] CylinderL2 P E) instance to
shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds6
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedSpace ℝ (CylinderL2 P U →L[ℝ] CylinderL2 P E) instance to shorten
typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds7
(P : ℝ)
[Fact (0 < P)]
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedAddCommGroup (CylinderL2 P E →L[ℝ] CylinderL2 P E) instance to
shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds8
(P : ℝ)
[Fact (0 < P)]
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedSpace ℝ (CylinderL2 P E →L[ℝ] CylinderL2 P E) instance to shorten
typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds9
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,CylinderL2 P U →L[ℝ] CylinderL2 P E)
instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds10
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
NormedSpace ℝ
C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))
Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,CylinderL2 P U →L[ℝ] CylinderL2 P E)
instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds11
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,CylinderL2 P E →L[ℝ] CylinderL2 P E)
instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletTimeBounds12
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
NormedSpace ℝ
C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))
Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,CylinderL2 P E →L[ℝ] CylinderL2 P E)
instance to shorten typeclass synthesis.
Instances For
theorem
EulerCylinderDirichlet.Coefficients.accelerationLp_block_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 ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Rc C₀ C₁ CH Cf R : ℝ)
(hRc : 0 ≤ Rc)
(hC₀ : 0 ≤ C₀)
(hC₁ : 0 ≤ C₁)
(hCH : 0 ≤ CH)
(hCf : 0 ≤ Cf)
(hbQ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q) a‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n)
(hbQ₁ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q₁) a‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n)
(hbH :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.H) a‖ ≤ CH * EulerGevrey.majorant Rc 0 n)
(hRweak :
2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH D.lower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hRstrong :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.lower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf :
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) f)
(d : ℕ)
(hfb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) f)
n 0 ≤ Cf * EulerGevrey.majorant R d n)
(n : ℕ)
(a : EulerLiftedGradientSpace.LiftTangent)
:
EulerParameterWordGevrey.block directions q
(fun (b : EulerLiftedGradientSpace.LiftTangent) =>
(EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P b).toContinuousLinearMap)
((accelerationLp P D) f))
n a ≤ EulerGevrey.majorant R (d + 2) n
The actual cylinder acceleration in time L², with the same external radius.
theorem
EulerCylinderDirichlet.Coefficients.continuousVelocity_block_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 ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Rc C₀ C₁ CH Cf R : ℝ)
(hRc : 0 ≤ Rc)
(hC₀ : 0 ≤ C₀)
(hC₁ : 0 ≤ C₁)
(hCH : 0 ≤ CH)
(hCf : 0 ≤ Cf)
(hbQ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q) a‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n)
(hbQ₁ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q₁) a‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n)
(hbH :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.H) a‖ ≤ CH * EulerGevrey.majorant Rc 0 n)
(hRweak :
2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH D.lower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hRstrong :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.lower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hT1 : T ≤ 1)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f)
(d : ℕ)
(hfb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) n 0 ≤ Cf * EulerGevrey.majorant R d n)
(n : ℕ)
(a : EulerLiftedGradientSpace.LiftTangent)
:
EulerParameterWordGevrey.block directions q
(fun (b : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P b) ((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)))
n a ≤ EulerFixedEvolutionSobolev.traceCost T * EulerGevrey.majorant R (d + 2) n
The actual continuous velocity trace from cylinder forcing.
theorem
EulerCylinderDirichlet.Coefficients.accelerationPath_block_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 ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Rc C₀ C₁ CH Cf R : ℝ)
(hRc : 0 ≤ Rc)
(hC₀ : 0 ≤ C₀)
(hC₁ : 0 ≤ C₁)
(hCH : 0 ≤ CH)
(hCf : 0 ≤ Cf)
(hbQ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q) a‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n)
(hbQ₁ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q₁) a‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n)
(hbH :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.H) a‖ ≤ CH * EulerGevrey.majorant Rc 0 n)
(hRweak :
2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH D.lower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hRstrong :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.lower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hT1 : T ≤ 1)
(hRuniform :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.lower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf
(EulerFixedEvolutionSobolev.traceCost T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f)
(d : ℕ)
(hfb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) n 0 ≤ Cf * EulerGevrey.majorant R d n)
(n : ℕ)
(a : EulerLiftedGradientSpace.LiftTangent)
:
EulerParameterWordGevrey.block directions q
(fun (b : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P b) (accelerationPath P D f))
n a ≤ EulerGevrey.majorant R (d + 3) n
Time-uniform acceleration of the actual history solution, including both endpoints.