Quantitative genuine coefficient calculus for the fixed mean inverse

The actual fixed operator has a polynomial amplitude depending on the time interval and coefficient bounds. The factorial radius and derivative shift are preserved by the coefficient-to-time-operator constructions.

Polynomial factorial bounds for the full mean variational form

All quantities are actual iterated Fréchet derivatives. The initial trace operator contributes through its proved operator norm, just as the time primitive does. The estimates keep the coefficient amplitudes outside the factorial radius.

theorem EulerMeanFormGevrey.meanOperator_contDiff {P : Type u_1} {W : Type u_3} {X : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : W →L[ℝ] W) (R : W →L[ℝ] X) (H : P → W →L[ℝ] W) (C : P → X →L[ℝ] X) {n : WithTop ℕ∞} (hH : ContDiff ℝ n H) (hC : ContDiff ℝ n C) : ContDiff ℝ n fun (p : P) => EulerMeanVariationalOperator.meanOperator J R (H p) (C p)

The full physical form is a smooth polynomial in its genuine coefficient operators.

noncomputable def EulerMeanFormGevrey.baseAmplitude {W : Type u_3} {X : Type u_4} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] (J : W →L[ℝ] W) (R : W →L[ℝ] X) (CH CC : ℝ) : ℝ

A polynomial amplitude for the original kinetic, potential, and boundary form.

Equations

• EulerMeanFormGevrey.baseAmplitude J R CH CC = 1 + ‖J‖ ^ 2 * CH + ‖R‖ ^ 2 * CC

theorem EulerMeanFormGevrey.baseAmplitude_nonneg {W : Type u_3} {X : Type u_4} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] (J : W →L[ℝ] W) (R : W →L[ℝ] X) (CH CC : ℝ) (hCH : 0 ≤ CH) (hCC : 0 ≤ CC) : 0 ≤ baseAmplitude J R CH CC

theorem EulerMeanFormGevrey.meanOperator_bound {P : Type u_1} {W : Type u_3} {X : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : W →L[ℝ] W) (R : W →L[ℝ] X) (H : P → W →L[ℝ] W) (C : P → X →L[ℝ] X) (hH : ContDiff ℝ (↑⊤) H) (hC : ContDiff ℝ (↑⊤) C) (r CH CC : ℝ) (hr : 0 ≤ r) (hCH : 0 ≤ CH) (hCC : 0 ≤ CC) (hHb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant r 0 n) (hCb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n C x‖ ≤ CC * EulerGevrey.majorant r 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (p : P) => EulerMeanVariationalOperator.meanOperator J R (H p) (C p)) x‖ ≤ baseAmplitude J R CH CC * EulerGevrey.majorant r 0 n

The actual physical mean operator has the stated all-order factorial bound.

theorem EulerMeanFormGevrey.pullbackMeanOperator_contDiff {P : Type u_1} {V : Type u_2} {W : Type u_3} {X : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : W →L[ℝ] W) (R : W →L[ℝ] X) (H : P → W →L[ℝ] W) (C : P → X →L[ℝ] X) (D : P → V →L[ℝ] W) {n : WithTop ℕ∞} (hD : ContDiff ℝ n D) (hH : ContDiff ℝ n H) (hC : ContDiff ℝ n C) : ContDiff ℝ n fun (p : P) => EulerHilbertCoerciveTransport.transportedOperator (D p) (EulerMeanVariationalOperator.meanOperator J R (H p) (C p))

Pullback by the genuine coordinate derivative preserves coefficient regularity.

theorem EulerMeanFormGevrey.pullbackMeanOperator_bound {P : Type u_1} {V : Type u_2} {W : Type u_3} {X : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : W →L[ℝ] W) (R : W →L[ℝ] X) (H : P → W →L[ℝ] W) (C : P → X →L[ℝ] X) (D : P → V →L[ℝ] W) (hD : ContDiff ℝ (↑⊤) D) (hH : ContDiff ℝ (↑⊤) H) (hC : ContDiff ℝ (↑⊤) C) (r CD CH CC : ℝ) (hr : 0 ≤ r) (hCD : 0 ≤ CD) (hCH : 0 ≤ CH) (hCC : 0 ≤ CC) (hDb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n D x‖ ≤ CD * EulerGevrey.majorant r 0 n) (hHb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant r 0 n) (hCb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n C x‖ ≤ CC * EulerGevrey.majorant r 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (p : P) => EulerHilbertCoerciveTransport.transportedOperator (D p) (EulerMeanVariationalOperator.meanOperator J R (H p) (C p))) x‖ ≤ 9 * CD ^ 2 * baseAmplitude J R CH CC * EulerGevrey.majorant r 0 n

The full actual fixed-space mean operator obeys a polynomial factorial bound.

theorem EulerMeanFormGevrey.pullbackMeanForcing_bound {P : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (J : W →L[ℝ] W) (D : P → V →L[ℝ] W) (f : P → W) (hD : ContDiff ℝ (↑⊤) D) (hf : ContDiff ℝ (↑⊤) f) (r CD CF : ℝ) (hr : 0 ≤ r) (hCD : 0 ≤ CD) (hCF : 0 ≤ CF) (d : ℕ) (hDb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n D x‖ ≤ CD * EulerGevrey.majorant r 0 n) (hfb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ CF * EulerGevrey.majorant r d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (p : P) => -(ContinuousLinearMap.adjoint (J ∘SL D p)) (f p)) x‖ ≤ 3 * (‖J‖ * CD) * CF * EulerGevrey.majorant r d n

The genuine forcing pullback has the matching factorial shift.

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey3 : NormedAddCommGroup (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey4 : NormedSpace ℝ (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey5 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey6 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T, L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey6 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey7 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey8 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T, solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientGevrey.instMeanFixedCoefficientGevrey8 T = inferInstance

theorem EulerMeanFixedCoefficientGevrey.baseAmplitude_time_bound (T : ℝ) (hT : 0 ≤ T) (CH CC : ℝ) (hCH : 0 ≤ CH) (hCC : 0 ≤ CC) : EulerMeanFormGevrey.baseAmplitude (EulerTerminalTimePrimitive.primitiveTimeLp T hT) (EulerTerminalTimePrimitive.initialTrace T hT) CH CC ≤ 1 + T ^ 2 / 2 * CH + T * CC

The sharp terminal time bounds control the norm factors in the actual physical form.

theorem EulerMeanFixedCoefficientGevrey.solenoidalFrame_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (F : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF : ContDiff ℝ (↑⊤) F) (r C : ℝ) (hr : 0 ≤ r) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F x‖ ≤ C * EulerGevrey.majorant r d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (p : P) => EulerMeanVariationalInverse.solenoidalFrame T (F p)) x‖ ≤ C * EulerGevrey.majorant r d n

Restriction to the actual solenoidal space does not enlarge any factorial bound.

theorem EulerMeanFixedCoefficientGevrey.fixedMeanDerivative_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (F F₁ : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF : ContDiff ℝ (↑⊤) F) (hF₁ : ContDiff ℝ (↑⊤) F₁) (r CF CF₁ : ℝ) (hr : 0 ≤ r) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (d : ℕ) (hFb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F x‖ ≤ CF * EulerGevrey.majorant r d n) (hF₁b : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F₁ x‖ ≤ CF₁ * EulerGevrey.majorant r d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (p : P) => EulerMeanFixedSpaceInverse.fixedMeanDerivative T hT (F p) (F₁ p)) x‖ ≤ (T * CF₁ + CF) * EulerGevrey.majorant r d n

The genuine fixed derivative map has only polynomial time cost.

theorem EulerMeanFixedCoefficientGevrey.fixedMeanOperator_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (F F₁ H : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : P → ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (hF : ContDiff ℝ (↑⊤) F) (hF₁ : ContDiff ℝ (↑⊤) F₁) (hH : ContDiff ℝ (↑⊤) H) (hM0 : ContDiff ℝ (↑⊤) M0) (hA : ContDiff ℝ (↑⊤) A) (r CF CF₁ CH CM CA : ℝ) (hr : 0 ≤ r) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCH : 0 ≤ CH) (hCM : 0 ≤ CM) (hCA : 0 ≤ CA) (hFb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F x‖ ≤ CF * EulerGevrey.majorant r 0 n) (hF₁b : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F₁ x‖ ≤ CF₁ * EulerGevrey.majorant r 0 n) (hHb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant r 0 n) (hMb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n M0 x‖ ≤ CM * EulerGevrey.majorant r 0 n) (hAb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ CA * EulerGevrey.majorant r 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (p : P) => EulerMeanFixedSpaceInverse.fixedMeanOperator T hT (F p) (F₁ p) (H p) (M0 p) (A p) L) x‖ ≤ 9 * (T * CF₁ + CF) ^ 2 * (1 + T ^ 2 / 2 * CH + T * (CM + |L| * CA)) * EulerGevrey.majorant r 0 n

A fully explicit polynomial amplitude for actual derivatives of the entire fixed mean operator.

theorem EulerMeanFixedCoefficientGevrey.fixedMeanForcing_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (F F₁ : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (f : P → ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hF : ContDiff ℝ (↑⊤) F) (hF₁ : ContDiff ℝ (↑⊤) F₁) (hf : ContDiff ℝ (↑⊤) f) (r CF CF₁ Cf : ℝ) (hr : 0 ≤ r) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCf : 0 ≤ Cf) (d : ℕ) (hFb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F x‖ ≤ CF * EulerGevrey.majorant r 0 n) (hF₁b : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F₁ x‖ ≤ CF₁ * EulerGevrey.majorant r 0 n) (hfb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ Cf * EulerGevrey.majorant r d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (p : P) => -(ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT (F p) (F₁ p))) (f p)) x‖ ≤ 3 * (T * (T * CF₁ + CF)) * Cf * EulerGevrey.majorant r d n

The actual force pullback preserves the forcing shift and has explicit polynomial amplitude.