Actual source forward coefficient and its translated factorial bounds

The input consists of the source frame fields and their genuine uniform jets. The generator itself is constructed by the bounded-field Gram inverse. Its spatial translation family is identified pointwise and estimated in the actual uniform time-space norm.

The constructed inverse Gram field in the uniform space-time norm

Uniform lower bounds for the pointwise frame construct a bounded continuous inverse field. It forms an actual unit of the bounded-field Banach algebra. The resulting time path and its parameter regularity are therefore proved in the uniform spatial norm, not merely at each fixed spatial label.

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse1 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (U →L[ℝ] E)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse1 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse2 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (U →L[ℝ] E)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse2 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse3 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] U)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse3 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse4 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] U)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse4 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse5 {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse5 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse6 {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse6 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse7 {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse7 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse8 {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse8 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse9 {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (U →L[ℝ] U)

Cache the standard NormedRing (U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse9 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse10 {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAlgebra ℝ (U →L[ℝ] U)

Cache the standard NormedAlgebra ℝ (U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse10 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse11 {α : Type u_1} {U : Type u_2} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (BoundedContinuousFunction α (U →L[ℝ] U))

Cache the standard NormedRing (α →ᵇ U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse11 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse12 {α : Type u_1} {U : Type u_2} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAlgebra ℝ (BoundedContinuousFunction α (U →L[ℝ] U))

Cache the standard NormedAlgebra ℝ (α →ᵇ U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse12 = inferInstance

noncomputable def EulerBoundedFieldGramInverse.gramField {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : BoundedContinuousFunction α (U →L[ℝ] E)) : BoundedContinuousFunction α (U →L[ℝ] U)

The literal positive Gram coefficient field.

Equations

• EulerBoundedFieldGramInverse.gramField Q = (EulerBoundedFieldCalculus.compositionMap (EulerBoundedFieldCalculus.adjointMap Q)) Q

@[simp]

theorem EulerBoundedFieldGramInverse.gramField_apply {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : BoundedContinuousFunction α (U →L[ℝ] E)) (x : α) : (gramField Q) x = EulerTransverseGramInverse.gram (Q x)

theorem EulerBoundedFieldGramInverse.inverseField_continuous {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : BoundedContinuousFunction α (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q x) v‖ ^ 2) : Continuous fun (x : α) => EulerTransverseGramInverse.gramInverse (Q x) c hc ⋯

Continuity of the actual pointwise coercive inverse.

noncomputable def EulerBoundedFieldGramInverse.inverseField {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : BoundedContinuousFunction α (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q x) v‖ ^ 2) : BoundedContinuousFunction α (U →L[ℝ] U)

The genuine bounded continuous inverse field, with coercive norm c⁻¹.

Equations

• EulerBoundedFieldGramInverse.inverseField Q c hc hQ = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : α) => EulerTransverseGramInverse.gramInverse (Q x) c hc ⋯) ⋯ c⁻¹ ⋯

@[simp]

theorem EulerBoundedFieldGramInverse.inverseField_apply {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : BoundedContinuousFunction α (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q x) v‖ ^ 2) (x : α) : (inverseField Q c hc hQ) x = EulerTransverseGramInverse.gramInverse (Q x) c hc ⋯

theorem EulerBoundedFieldGramInverse.inverseField_norm {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : BoundedContinuousFunction α (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q x) v‖ ^ 2) : ‖inverseField Q c hc hQ‖ ≤ c⁻¹

noncomputable def EulerBoundedFieldGramInverse.gramFieldUnit {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : BoundedContinuousFunction α (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q x) v‖ ^ 2) : (BoundedContinuousFunction α (U →L[ℝ] U))ˣ

This actual inverse forms a unit in the bounded-field algebra.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerBoundedFieldGramInverse.inverseField_eq_ringInverse {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : BoundedContinuousFunction α (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q x) v‖ ^ 2) : inverseField Q c hc hQ = Ring.inverse (gramField Q)

Actual pointwise inversion equals the Banach-algebra inverse.

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse13 {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse13 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse14 {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse14 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse15 {α : Type u_1} {U : Type u_2} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction α (U →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse15 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramInverse16 {α : Type u_1} {U : Type u_2} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction α (U →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramInverse16 = inferInstance

noncomputable def EulerBoundedFieldGramInverse.gramPath {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] (Qp : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) : C(K, BoundedContinuousFunction α (U →L[ℝ] U))

The Gram field as an actual uniform time path.

Equations

• EulerBoundedFieldGramInverse.gramPath Qp = (EulerBoundedFieldCalculus.pathCompositionMap (EulerBoundedFieldCalculus.pathAdjointMap Qp)) Qp

@[simp]

theorem EulerBoundedFieldGramInverse.gramPath_apply {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] (Qp : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (t : K) : (gramPath Qp) t = gramField (Qp t)

noncomputable def EulerBoundedFieldGramInverse.inversePath {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) {K : Type u_4} [TopologicalSpace K] [CompactSpace K] (Qp : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hLower : ∀ (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Qp t) x) v‖ ^ 2) : C(K, BoundedContinuousFunction α (U →L[ℝ] U))

The constructed inverse is continuous in the spatial uniform norm as time varies.

Equations

• EulerBoundedFieldGramInverse.inversePath c hc Qp hLower = { toFun := fun (t : K) => EulerBoundedFieldGramInverse.inverseField (Qp t) c hc ⋯, continuous_toFun := ⋯ }

@[simp]

theorem EulerBoundedFieldGramInverse.inversePath_apply {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) {K : Type u_4} [TopologicalSpace K] [CompactSpace K] (Qp : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hLower : ∀ (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Qp t) x) v‖ ^ 2) (t : K) (x : α) : ((inversePath c hc Qp hLower) t) x = EulerTransverseGramInverse.gramInverse ((Qp t) x) c hc ⋯

theorem EulerBoundedFieldGramInverse.inversePath_norm {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) {K : Type u_4} [TopologicalSpace K] [CompactSpace K] (Qp : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hLower : ∀ (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Qp t) x) v‖ ^ 2) : ‖inversePath c hc Qp hLower‖ ≤ c⁻¹

The uniform time-space inverse bound is the same coercive bound.

noncomputable def EulerBoundedFieldGramInverse.gramPathUnit {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) {K : Type u_4} [TopologicalSpace K] [CompactSpace K] (Qp : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hLower : ∀ (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Qp t) x) v‖ ^ 2) : C(K, BoundedContinuousFunction α (U →L[ℝ] U))ˣ

The pathwise Gram field is an actual unit of the full time-space Banach algebra.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerBoundedFieldGramInverse.inversePath_eq_ringInverse {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) {K : Type u_4} [TopologicalSpace K] [CompactSpace K] (Qp : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hLower : ∀ (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Qp t) x) v‖ ^ 2) : inversePath c hc Qp hLower = Ring.inverse (gramPath Qp)

The actual inverse path is the algebra inverse in the uniform time-space norm.

theorem EulerBoundedFieldGramInverse.gramPath_contDiff {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] {P : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) {n : WithTop ℕ∞} (hA : ContDiff ℝ n A) : ContDiff ℝ n fun (a : P) => gramPath (A a)

Smoothness of the actual uniform Gram coefficient path.

theorem EulerBoundedFieldGramInverse.inversePath_contDiff {α : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) {K : Type u_4} [TopologicalSpace K] [CompactSpace K] {P : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hLower : ∀ (a : P) (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(((A a) t) x) v‖ ^ 2) {n : WithTop ℕ∞} (hA : ContDiff ℝ n A) : ContDiff ℝ n fun (a : P) => inversePath c hc (A a) ⋯

Smoothness of the constructed inverse in the uniform time-space norm.

Actual factorial estimates for the uniformly bounded space-time Gram inverse.

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey1 {U : Type u_4} {E : Type u_5} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (U →L[ℝ] E)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey2 {U : Type u_4} {E : Type u_5} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (U →L[ℝ] E)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey3 {U : Type u_4} {E : Type u_5} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] U)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey3 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey4 {U : Type u_4} {E : Type u_5} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] U)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey4 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey5 {U : Type u_4} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (U →L[ℝ] U)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey5 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey6 {U : Type u_4} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (U →L[ℝ] U)

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey6 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey7 {α : Type u_1} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey7 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey8 {α : Type u_1} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey8 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey9 {α : Type u_1} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey9 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey10 {α : Type u_1} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey10 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey11 {α : Type u_1} {U : Type u_4} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (BoundedContinuousFunction α (U →L[ℝ] U))

Cache the standard NormedAddCommGroup (α →ᵇ U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey11 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey12 {α : Type u_1} {U : Type u_4} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (BoundedContinuousFunction α (U →L[ℝ] U))

Cache the standard NormedSpace ℝ (α →ᵇ U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey12 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey13 {α : Type u_1} {K : Type u_2} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(K, BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey13 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey14 {α : Type u_1} {K : Type u_2} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(K, BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey14 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey15 {α : Type u_1} {K : Type u_2} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(K, BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey15 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey16 {α : Type u_1} {K : Type u_2} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(K, BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey16 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey17 {α : Type u_1} {K : Type u_2} {U : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup C(K, BoundedContinuousFunction α (U →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey17 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey18 {α : Type u_1} {K : Type u_2} {U : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ C(K, BoundedContinuousFunction α (U →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey18 = inferInstance

theorem EulerBoundedFieldGramInverse.gramPath_bound {α : Type u_1} {K : Type u_2} {P : Type u_3} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hQ : ContDiff ℝ (↑⊤) Q) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => gramPath (Q y)) x‖ ≤ 3 * C ^ 2 * EulerGevrey.majorant R 0 n

The actual Gram field has the sharp fixed factorial product bound.

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey19 {α : Type u_1} {K : Type u_2} {U : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup C(K, BoundedContinuousFunction α (U →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey19 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey20 {α : Type u_1} {K : Type u_2} {U : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ C(K, BoundedContinuousFunction α (U →L[ℝ] U))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey20 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey21 {α : Type u_1} {K : Type u_2} {U : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (C(K, BoundedContinuousFunction α (U →L[ℝ] U)) →L[ℝ] C(K, BoundedContinuousFunction α (U →L[ℝ] U)))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey21 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey22 {α : Type u_1} {K : Type u_2} {U : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (C(K, BoundedContinuousFunction α (U →L[ℝ] U)) →L[ℝ] C(K, BoundedContinuousFunction α (U →L[ℝ] U)))

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

Equations

• EulerBoundedFieldGramInverse.instBoundedFieldGramGevrey22 = inferInstance

theorem EulerBoundedFieldGramInverse.inversePath_gevrey {α : Type u_1} {K : Type u_2} {P : Type u_3} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (c : ℝ) (hc : 0 < c) (hLower : ∀ (y : P) (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(((Q y) t) x) v‖ ^ 2) (hQ : ContDiff ℝ (↑⊤) Q) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (R : ℝ) (hR : 2 * EulerTimeLpGramGevrey.gramCost c C 1 * (Rc + 1) ≤ R) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => inversePath c hc (Q y) ⋯) x‖ ≤ EulerGevrey.majorant R 1 n

The genuinely constructed inverse has one factorial shift in the uniform time-space norm.

theorem EulerBoundedFieldGramInverse.inversePath_coefficient_bound {α : Type u_1} {K : Type u_2} {P : Type u_3} {U : Type u_4} {E : Type u_5} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (c : ℝ) (hc : 0 < c) (hLower : ∀ (y : P) (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(((Q y) t) x) v‖ ^ 2) (hQ : ContDiff ℝ (↑⊤) Q) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (R : ℝ) (hR0 : 0 ≤ R) (hR : 2 * EulerTimeLpGramGevrey.gramCost c C 1 * (Rc + 1) ≤ R) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => inversePath c hc (Q y) ⋯) x‖ ≤ R * EulerGevrey.majorant (4 * R) 0 n

A fixed coefficient radius absorbs the one inverse shift once, before recursive solves.

The actual source forward generator in uniform space-time coefficient norm

The Gram inverse is constructed in the bounded-field Banach algebra. This produces the literal source coefficient -2(QQ)⁻¹QQ₁ and the projected-forcing coefficient (QQ)⁻¹Q. Spatial translation covariance and coefficient estimates are proved for these actual fields.

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator1 {U : Type u_3} {E : Type u_4} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (U →L[ℝ] E)

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator1 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator2 {U : Type u_3} {E : Type u_4} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (U →L[ℝ] E)

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator2 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator3 {U : Type u_3} {E : Type u_4} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] U)

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator3 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator4 {U : Type u_3} {E : Type u_4} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] U)

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator4 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator5 {U : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (U →L[ℝ] U)

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator5 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator6 {U : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (U →L[ℝ] U)

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator6 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator7 {α : Type u_1} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator7 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator8 {α : Type u_1} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator8 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator9 {α : Type u_1} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator9 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator10 {α : Type u_1} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator10 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator11 {α : Type u_1} {U : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (BoundedContinuousFunction α (U →L[ℝ] U))

Cache the standard NormedAddCommGroup (α →ᵇ U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator11 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator12 {α : Type u_1} {U : Type u_3} [TopologicalSpace α] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (BoundedContinuousFunction α (U →L[ℝ] U))

Cache the standard NormedSpace ℝ (α →ᵇ U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator12 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator13 {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(K, BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator13 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator14 {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(K, BoundedContinuousFunction α (U →L[ℝ] E))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator14 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator15 {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(K, BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator15 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator16 {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(K, BoundedContinuousFunction α (E →L[ℝ] U))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator16 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator17 {α : Type u_1} {K : Type u_2} {U : Type u_3} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup C(K, BoundedContinuousFunction α (U →L[ℝ] U))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator17 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator18 {α : Type u_1} {K : Type u_2} {U : Type u_3} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ C(K, BoundedContinuousFunction α (U →L[ℝ] U))

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

Equations

• EulerBoundedFieldForwardGenerator.instBoundedFieldForwardGenerator18 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldForwardGenerator.instForwardPathDistribSMul {α : Type u_1} {K : Type u_2} {U : Type u_3} [TopologicalSpace α] [TopologicalSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : DistribSMul ℝ C(K, BoundedContinuousFunction α (U →L[ℝ] U))

Cache the pointwise distributive scalar action on bounded operator paths.

Equations

• EulerBoundedFieldForwardGenerator.instForwardPathDistribSMul = inferInstance

noncomputable def EulerBoundedFieldForwardGenerator.leftInversePath {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) (Q : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hQ : ∀ (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q t) x) v‖ ^ 2) : C(K, BoundedContinuousFunction α (E →L[ℝ] U))

The actual projected-forcing coefficient field.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerBoundedFieldForwardGenerator.generatorPath {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) (Q Q₁ : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hQ : ∀ (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q t) x) v‖ ^ 2) : C(K, BoundedContinuousFunction α (U →L[ℝ] U))

The actual ordinary coefficient in source equation (12).

Equations

• EulerBoundedFieldForwardGenerator.generatorPath c hc Q Q₁ hQ = -2 • (EulerBoundedFieldCalculus.pathCompositionMap (EulerBoundedFieldForwardGenerator.leftInversePath c hc Q hQ)) Q₁

@[simp]

theorem EulerBoundedFieldForwardGenerator.leftInversePath_apply {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) (Q : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hQ : ∀ (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q t) x) v‖ ^ 2) (t : K) (x : α) : ((leftInversePath c hc Q hQ) t) x = EulerTransverseGramInverse.gramInverse ((Q t) x) c hc ⋯ ∘SL ContinuousLinearMap.adjoint ((Q t) x)

@[simp]

theorem EulerBoundedFieldForwardGenerator.generatorPath_apply {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) (hc : 0 < c) (Q Q₁ : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hQ : ∀ (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q t) x) v‖ ^ 2) (t : K) (x : α) : ((generatorPath c hc Q Q₁ hQ) t) x = -2 • EulerTransverseGramInverse.gramInverse ((Q t) x) c hc ⋯ ∘SL ContinuousLinearMap.adjoint ((Q t) x) ∘SL (Q₁ t) x

theorem EulerBoundedFieldForwardGenerator.leftInversePath_contDiff {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] (c : ℝ) (hc : 0 < c) (Q : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hQ : ∀ (y : P) (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(((Q y) t) x) v‖ ^ 2) {n : WithTop ℕ∞} (hQr : ContDiff ℝ n Q) : ContDiff ℝ n fun (y : P) => leftInversePath c hc (Q y) ⋯

Genuine parameter regularity of the actual projected-forcing coefficient.

theorem EulerBoundedFieldForwardGenerator.generatorPath_contDiff {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] (c : ℝ) (hc : 0 < c) (Q Q₁ : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hQ : ∀ (y : P) (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(((Q y) t) x) v‖ ^ 2) {n : WithTop ℕ∞} (hQr : ContDiff ℝ n Q) (hQ₁r : ContDiff ℝ n Q₁) : ContDiff ℝ n fun (y : P) => generatorPath c hc (Q y) (Q₁ y) ⋯

Genuine parameter regularity of the actual source generator.

theorem EulerBoundedFieldForwardGenerator.leftInversePath_bound {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] (Q : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (c : ℝ) (hc : 0 < c) (hQ : ∀ (y : P) (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(((Q y) t) x) v‖ ^ 2) (hQr : ContDiff ℝ (↑⊤) Q) (Rc C₀ Ri : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => leftInversePath c hc (Q y) ⋯) x‖ ≤ 3 * Ri * C₀ * EulerGevrey.majorant (4 * Ri) 0 n

The projected-forcing coefficient has a polynomial shift-zero amplitude.

theorem EulerBoundedFieldForwardGenerator.generatorPath_bound {α : Type u_1} {K : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace α] [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] (Q Q₁ : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (c : ℝ) (hc : 0 < c) (hQ : ∀ (y : P) (t : K) (x : α) (v : U), c * ‖v‖ ^ 2 ≤ ‖(((Q y) t) x) v‖ ^ 2) (hQr : ContDiff ℝ (↑⊤) Q) (hQ₁r : ContDiff ℝ (↑⊤) Q₁) (Rc C₀ C₁ Ri : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => generatorPath c hc (Q y) (Q₁ y) ⋯) x‖ ≤ 18 * Ri * C₀ * C₁ * EulerGevrey.majorant (4 * Ri) 0 n

The literal generator in (12) satisfies the source's polynomial coefficient bound.

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient1 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (U →L[ℝ] E)

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient1 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient2 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (U →L[ℝ] E)

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient2 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient3 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] U)

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient3 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient4 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] U)

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient4 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient5 {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (U →L[ℝ] U)

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient5 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient6 {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (U →L[ℝ] U)

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient6 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient7 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] E))

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient7 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient8 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] E))

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient8 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient9 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] U))

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient9 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient10 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] U))

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient10 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient11 {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient11 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient12 {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient12 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient13 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient14 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient15 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient16 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient17 {K : Type u_1} {U : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient17 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceForwardCoefficient.instSourceForwardCoefficient18 {K : Type u_1} {U : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

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

Equations

• EulerSourceForwardCoefficient.instSourceForwardCoefficient18 = inferInstance

noncomputable def EulerSourceForwardCoefficient.sourceGenerator {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

The actual bounded continuous source generator.

Equations

• EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ = EulerBoundedFieldForwardGenerator.generatorPath c hc Q.field Q₁.field hQ

noncomputable def EulerSourceForwardCoefficient.sourceForcing {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] U))

The actual bounded continuous projected-forcing coefficient.

Equations

• EulerSourceForwardCoefficient.sourceForcing Q c hc hQ = EulerBoundedFieldForwardGenerator.leftInversePath c hc Q.field hQ

theorem EulerSourceForwardCoefficient.translated_lower {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (a : EulerSmoothLimit.Space) (t : K) (x : EulerSmoothLimit.Space) (v : U) : c * ‖v‖ ^ 2 ≤ ‖(((EulerMeanCoefficients.translateCoefficientPath Q.field a) t) x) v‖ ^ 2

Source lower bounds hold at every translated label.

theorem EulerSourceForwardCoefficient.sourceGenerator_translated {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (a : EulerSmoothLimit.Space) : EulerBoundedFieldForwardGenerator.generatorPath c hc (EulerMeanCoefficients.translateCoefficientPath Q.field a) (EulerMeanCoefficients.translateCoefficientPath Q₁.field a) ⋯ = EulerMeanCoefficients.translateCoefficientPath (sourceGenerator Q Q₁ c hc hQ) a

This is an equality of actual fields, not a chosen translated inverse.

theorem EulerSourceForwardCoefficient.sourceForcing_translated {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (a : EulerSmoothLimit.Space) : EulerBoundedFieldForwardGenerator.leftInversePath c hc (EulerMeanCoefficients.translateCoefficientPath Q.field a) ⋯ = EulerMeanCoefficients.translateCoefficientPath (sourceForcing Q c hc hQ) a

theorem EulerSourceForwardCoefficient.sourceGenerator_translation_contDiff {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath (sourceGenerator Q Q₁ c hc hQ))

The actual generator's translated family is genuinely smooth in the uniform time-space norm.

theorem EulerSourceForwardCoefficient.sourceForcing_translation_contDiff {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath (sourceForcing Q c hc hQ))

theorem EulerSourceForwardCoefficient.sourceGenerator_translation_bound {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (Rc C₀ C₁ Ri : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (sourceGenerator Q Q₁ c hc hQ)) a‖ ≤ 18 * Ri * C₀ * C₁ * EulerGevrey.majorant (4 * Ri) 0 n

The constructed source generator has a polynomial shift-zero coefficient bound.

theorem EulerSourceForwardCoefficient.sourceForcing_translation_bound {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (Rc C₀ Ri : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (sourceForcing Q c hc hQ)) a‖ ≤ 3 * Ri * C₀ * EulerGevrey.majorant (4 * Ri) 0 n

The actual projected-forcing coefficient has the corresponding polynomial bound.