Same-radius mixed cylinder bounds for the physical frame and forcing

The translated coefficient is lifted through actual norm-one maps. Only its coefficient radius pays the finite alphabet and fixed Sobolev order. The input field's external-word radius is preserved by the true product estimate, using bounds only at the base translation.

The same-radius fixed-Sobolev product estimate needs bounds only at the base parameter.

theorem EulerParameterWordGevrey.block_clm_apply_gevrey_at {P : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [Fintype ι] (directions : ι → P) (q : ℕ) (A : P → E →L[ℝ] F) (f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (x : P) (Rc R C D : ℝ) (hRc : 0 ≤ Rc) (hRcR : Rc ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (hcoeff : ∀ (n : ℕ), coefficientBlock directions q A n x ≤ C * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfield : ∀ (n : ℕ), block directions q f n x ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : block directions q (fun (y : P) => (A y) (f y)) n x ≤ 3 * C * D * EulerGevrey.majorant R d n

A frozen-parameter product estimate. The field radius is unchanged.

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity1 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup (E →L[ℝ] F)

Cache the standard NormedAddCommGroup (E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity2 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ (E →L[ℝ] F)

Cache the standard NormedSpace ℝ (E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity3 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

Cache the standard NormedAddCommGroup (Space →ᵇ E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity3 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity4 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

Cache the standard NormedSpace ℝ (Space →ᵇ E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity4 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity5 {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

Cache the standard NormedAddCommGroup C(K,Space →ᵇ E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity5 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity6 {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

Cache the standard NormedSpace ℝ C(K,Space →ᵇ E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity6 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity7 (period : ℝ) [Fact (0 < period)] {E : Type u_1} [NormedAddCommGroup E] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 period E)

Cache the standard NormedAddCommGroup (CylinderL2 period E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity7 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity8 (period : ℝ) [Fact (0 < period)] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 period E)

Cache the standard NormedSpace ℝ (CylinderL2 period E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity8 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity9 (period : ℝ) [Fact (0 < period)] {F : Type u_2} [NormedAddCommGroup F] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 period F)

Cache the standard NormedAddCommGroup (CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity9 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity10 (period : ℝ) [Fact (0 < period)] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 period F)

Cache the standard NormedSpace ℝ (CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity10 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity11 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {K : Type u_3} [NormedAddCommGroup E] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))

Cache the standard NormedAddCommGroup C(K,CylinderL2 period E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity11 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity12 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))

Cache the standard NormedSpace ℝ C(K,CylinderL2 period E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity12 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity13 (period : ℝ) [Fact (0 < period)] {F : Type u_2} {K : Type u_3} [NormedAddCommGroup F] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F))

Cache the standard NormedAddCommGroup C(K,CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity13 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity14 (period : ℝ) [Fact (0 < period)] {F : Type u_2} {K : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F))

Cache the standard NormedSpace ℝ C(K,CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity14 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity15 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup (C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F)))

Cache the standard NormedAddCommGroup (C(K,CylinderL2 period E) →L[ℝ] C(K,CylinderL2 period F)) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity15 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangularRegularity16 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ (C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F)))

Cache the standard NormedSpace ℝ (C(K,CylinderL2 period E) →L[ℝ] C(K,CylinderL2 period F)) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangularRegularity16 period = inferInstance

noncomputable def EulerLpCylinderRectangular.mixedMultiplier (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (a : EulerLiftedGradientSpace.LiftTangent) : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F))

The actual rectangular multiplier family under all four covering translations.

Equations

• EulerLpCylinderRectangular.mixedMultiplier period A a = (EulerLpCylinderRectangular.fullMultiplierMap period) (EulerMeanCoefficients.translateCoefficientPath A a.1)

theorem EulerLpCylinderRectangular.mixedMultiplier_contDiff (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) : ContDiff ℝ (↑⊤) (mixedMultiplier period A)

theorem EulerLpCylinderRectangular.mixedMultiplier_bound (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (n : ℕ) (C : ℝ) (hb : ∀ (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) a‖ ≤ C) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (mixedMultiplier period A) a‖ ≤ C

The genuine mixed multiplier jets have exactly the bounded-field coefficient bound.

theorem EulerLpCylinderRectangular.product_orbit_contDiff (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) u) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) (((fullMultiplierMap period) A) u)

Applying the physical frame or projected-forcing coefficient preserves actual mixed smoothness.

theorem EulerLpCylinderRectangular.product_orbit_block_bound (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} {ι : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] [Fintype ι] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) u) (Rc C R D : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hD : 0 ≤ D) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hbA : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbu : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) u) n 0 ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) (((fullMultiplierMap period) A) u)) n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C * D * EulerGevrey.majorant R d n

True fixed-Hq mixed word bounds for actual coefficient application. The field radius R is identical on both sides.

theorem EulerLpCylinderRectangular.supported_product_orbit_contDiff (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS))) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) u)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (((supportedMultiplierMap period S hS) A) u))