Source-only guards for the affine-terminal cylinder inverse. The affine forcing is bounded for unit terminal data; no terminal amplitude, derivative shift, or recursive grade occurs in the radius conditions.

noncomputable def EulerCylinderDirichlet.Coefficients.endpointForcingCost (ι : Type u_1) [Fintype ι] (q : ℕ) (T Rc C₁ : ℝ) : ℝ

Endpoint forcing cost, given by 6*sobolevCoefficientAmplitude ι q Rc C₁*T⁻¹.

Equations

• EulerCylinderDirichlet.Coefficients.endpointForcingCost ι q T Rc C₁ = 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C₁ * T⁻¹

structure EulerCylinderDirichlet.Coefficients.EndpointBudget {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 : ℕ) : Type

Endpoint budget data, collecting Rc, C₀, C₁, CH, R, Rc_nonneg and their compatibility conditions.

• Rc : ℝ

  Rc of EndpointBudget, of type ℝ.

• C₀ : ℝ

  C₀ of EndpointBudget, of type ℝ.

• C₁ : ℝ

  First-derivative bound coefficient of EndpointBudget, of type ℝ.

• CH : ℝ

  CH of EndpointBudget, of type ℝ.

• R : ℝ

  Radius parameter of EndpointBudget, of type ℝ.

• Rc_nonneg : 0 ≤ self.Rc
• C₀_nonneg : 0 ≤ self.C₀
• C₁_nonneg : 0 ≤ self.C₁
• CH_nonneg : 0 ≤ self.CH
• time_le_one : T ≤ 1
• frame_smooth : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q)
• frameDerivative_smooth : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁)
• hessian_smooth : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H)
• frame_bound (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q) a‖ ≤ self.C₀ * EulerGevrey.majorant self.Rc 0 n
• frameDerivative_bound (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q₁) a‖ ≤ self.C₁ * EulerGevrey.majorant self.Rc 0 n
• hessian_bound (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.H) a‖ ≤ self.CH * EulerGevrey.majorant self.Rc 0 n
• weak_radius : 2 * EulerTransverseFixedSobolev.blockCost ι q T self.Rc self.C₀ self.C₁ self.CH D.lower (endpointForcingCost ι q T self.Rc self.C₁) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι self.Rc + 1) ≤ self.R
• strong_radius : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.lower self.Rc self.C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q self.Rc self.C₀ self.C₁ (endpointForcingCost ι q T self.Rc self.C₁) 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι self.Rc + 1) ≤ self.R
• uniform_radius : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.lower self.Rc self.C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q self.Rc self.C₀ self.C₁ (endpointForcingCost ι q T self.Rc self.C₁) (EulerFixedEvolutionSobolev.traceCost T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι self.Rc + 1) ≤ self.R

theorem EulerCylinderDirichlet.Coefficients.EndpointBudget.forcingCost_nonneg {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) : 0 ≤ endpointForcingCost ι q T L.Rc L.C₁

theorem EulerCylinderDirichlet.Coefficients.EndpointBudget.radius_bounds {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) : 1 ≤ L.R ∧ EulerParameterWordGevrey.sobolevCoefficientRadius ι L.Rc ≤ L.R

noncomputable def EulerCylinderDirichlet.Coefficients.EndpointBudget.coordinateCost {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) : ℝ

Coordinate cost, given by T⁻¹+traceCost T.

Equations

• _L.coordinateCost = T⁻¹ + EulerFixedEvolutionSobolev.traceCost T

noncomputable def EulerCylinderDirichlet.Coefficients.EndpointBudget.velocityCost {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) : ℝ

Velocity cost, given by 3*sobolevCoefficientAmplitude ι q L.Rc L.C₀*L.coordinateCost.

Equations

• L.velocityCost = 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q L.Rc L.C₀ * L.coordinateCost

noncomputable def EulerCylinderDirichlet.Coefficients.EndpointBudget.derivativeCost {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) : ℝ

Derivative cost, given by 3*sobolevCoefficientAmplitude ι q L.Rc L.C₁*L.coordinateCost + 3*sobolevCoefficientAmplitude ι q L.Rc L.C₀.

Equations

• L.derivativeCost = 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q L.Rc L.C₁ * L.coordinateCost + 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q L.Rc L.C₀

theorem EulerCylinderDirichlet.Coefficients.EndpointBudget.coordinateCost_nonneg {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) : 0 ≤ L.coordinateCost