Coefficient-only estimates for the nonzero-terminal transverse construction. Both primitives, the actual affine trial, and the fixed-coordinate form are estimated in their genuine Bochner and operator norms.

theorem EulerTransverseEndpointBounds.initialPrimitive_norm_le_time {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) : ‖EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT‖ ≤ T

theorem EulerTransverseEndpointBounds.constantFieldOperator_norm_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) : ‖EulerInitialTimePrimitive.constantFieldOperator T hT‖ ≤ 1 + T

theorem EulerTransverseEndpointBounds.multiplier_sub_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A B : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ‖EulerTimeLp.timeMultiplier T hT A - EulerTimeLp.timeMultiplier T hT B‖ ≤ ‖A - B‖

theorem EulerTransverseEndpointBounds.product_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (J : ↥(EulerTimeLp.TimeLp T U) →L[ℝ] ↥(EulerTimeLp.TimeLp T U)) (hJ : ‖J‖ ≤ T) (A A₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ‖EulerTimeLp.timeMultiplier T hT A₁ ∘SL J + EulerTimeLp.timeMultiplier T hT A‖ ≤ T * ‖A₁‖ + ‖A‖

theorem EulerTransverseEndpointBounds.product_sub_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (J : ↥(EulerTimeLp.TimeLp T U) →L[ℝ] ↥(EulerTimeLp.TimeLp T U)) (hJ : ‖J‖ ≤ T) (A A₁ B B₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ‖EulerTimeLp.timeMultiplier T hT A₁ ∘SL J + EulerTimeLp.timeMultiplier T hT A - (EulerTimeLp.timeMultiplier T hT B₁ ∘SL J + EulerTimeLp.timeMultiplier T hT B)‖ ≤ T * ‖A₁ - B₁‖ + ‖A - B‖

theorem EulerTransverseEndpointBounds.fixedFrameDerivative_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ‖EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT A A₁‖ ≤ T * ‖A₁‖ + ‖A‖

theorem EulerTransverseEndpointBounds.fixedFrameDerivative_sub_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ B B₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ‖EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT A A₁ - EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT B B₁‖ ≤ T * ‖A₁ - B₁‖ + ‖A - B‖

theorem EulerTransverseEndpointBounds.potential_norm_le {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (J : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (hJ : ‖J‖ ≤ T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : ‖ContinuousLinearMap.adjoint J ∘SL EulerTimeLp.timeMultiplier T hT H ∘SL J‖ ≤ T ^ 2 * ‖H‖

theorem EulerTransverseEndpointBounds.dirichlet_norm_le {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (J : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (hJ : ‖J‖ ≤ T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : ‖EulerTransverseVariationalInverse.dirichletOperator J (EulerTimeLp.timeMultiplier T hT H)‖ ≤ 1 + T ^ 2 * ‖H‖

theorem EulerTransverseEndpointBounds.dirichlet_sub_norm_le {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (J : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (hJ : ‖J‖ ≤ T) (H H' : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : ‖EulerTransverseVariationalInverse.dirichletOperator J (EulerTimeLp.timeMultiplier T hT H) - EulerTransverseVariationalInverse.dirichletOperator J (EulerTimeLp.timeMultiplier T hT H')‖ ≤ T ^ 2 * ‖H - H'‖

theorem EulerTransverseEndpointBounds.energyOperator_norm_le {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : ‖EulerTransverseEndpointEnergy.energyOperator T hT H‖ ≤ 1 + T ^ 2 * ‖H‖

theorem EulerTransverseEndpointBounds.energyOperator_sub_norm_le {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (H H' : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : ‖EulerTransverseEndpointEnergy.energyOperator T hT H - EulerTransverseEndpointEnergy.energyOperator T hT H'‖ ≤ T ^ 2 * ‖H - H'‖

noncomputable def EulerTransverseEndpointBounds.affineCost (T : ℝ) : ℝ

The affine coordinate trial costs a fixed polynomial in time and its reciprocal.

Equations

• EulerTransverseEndpointBounds.affineCost T = (1 + T) * |T⁻¹|

theorem EulerTransverseEndpointBounds.affineTrial_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ‖EulerTransverseEndpointParameter.affineTrial T hT A A₁‖ ≤ affineCost T * (T * ‖A₁‖ + ‖A‖)

theorem EulerTransverseEndpointBounds.affineTrial_sub_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ B B₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ‖EulerTransverseEndpointParameter.affineTrial T hT A A₁ - EulerTransverseEndpointParameter.affineTrial T hT B B₁‖ ≤ affineCost T * (T * ‖A₁ - B₁‖ + ‖A - B‖)