Actual bounded-field bilinear and adjoint calculus

Pointwise application/composition are bounded bilinear maps in the genuine uniform field norm, including on a noncompact spatial domain. Lifting these maps to compact time paths preserves their norm bounds. These are the coefficient maps used to construct the actual source forward generator.

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus1 {F : Type u_3} {G : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] : NormedAddCommGroup (F →L[ℝ] G)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus1 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus2 {F : Type u_3} {G : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] : NormedSpace ℝ (F →L[ℝ] G)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus2 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus3 {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] : NormedAddCommGroup (E →L[ℝ] F →L[ℝ] G)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus3 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus4 {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] : NormedSpace ℝ (E →L[ℝ] F →L[ℝ] G)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus4 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus5 {α : Type u_1} [TopologicalSpace α] {E : Type u_2} [NormedAddCommGroup E] : NormedAddCommGroup (BoundedContinuousFunction α E)

Cache the standard NormedAddCommGroup (α →ᵇ E) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus5 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus6 {α : Type u_1} [TopologicalSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ (BoundedContinuousFunction α E)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus6 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus7 {α : Type u_1} [TopologicalSpace α] {F : Type u_3} [NormedAddCommGroup F] : NormedAddCommGroup (BoundedContinuousFunction α F)

Cache the standard NormedAddCommGroup (α →ᵇ F) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus7 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus8 {α : Type u_1} [TopologicalSpace α] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (BoundedContinuousFunction α F)

Cache the standard NormedSpace ℝ (α →ᵇ F) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus8 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus9 {α : Type u_1} [TopologicalSpace α] {G : Type u_4} [NormedAddCommGroup G] : NormedAddCommGroup (BoundedContinuousFunction α G)

Cache the standard NormedAddCommGroup (α →ᵇ G) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus9 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus10 {α : Type u_1} [TopologicalSpace α] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] : NormedSpace ℝ (BoundedContinuousFunction α G)

Cache the standard NormedSpace ℝ (α →ᵇ G) instance to shorten typeclass synthesis.

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus10 = inferInstance

noncomputable def EulerBoundedFieldCalculus.bilinearValue {α : Type u_1} [TopologicalSpace α] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) (f : BoundedContinuousFunction α E) (g : BoundedContinuousFunction α F) : BoundedContinuousFunction α G

The literal pointwise bounded bilinear field.

Equations

• EulerBoundedFieldCalculus.bilinearValue B f g = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : α) => (B (f x)) (g x)) ⋯ (‖B‖ * ‖f‖ * ‖g‖) ⋯

@[simp]

theorem EulerBoundedFieldCalculus.bilinearValue_apply {α : Type u_1} [TopologicalSpace α] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) (f : BoundedContinuousFunction α E) (g : BoundedContinuousFunction α F) (x : α) : (bilinearValue B f g) x = (B (f x)) (g x)

theorem EulerBoundedFieldCalculus.bilinearValue_norm {α : Type u_1} [TopologicalSpace α] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) (f : BoundedContinuousFunction α E) (g : BoundedContinuousFunction α F) : ‖bilinearValue B f g‖ ≤ ‖B‖ * ‖f‖ * ‖g‖

noncomputable def EulerBoundedFieldCalculus.bilinearLinear {α : Type u_1} [TopologicalSpace α] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) : BoundedContinuousFunction α E →ₗ[ℝ] BoundedContinuousFunction α F →ₗ[ℝ] BoundedContinuousFunction α G

Bilinearity is proved on the actual coefficient functions.

Equations

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

noncomputable def EulerBoundedFieldCalculus.bilinearMap {α : Type u_1} [TopologicalSpace α] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) : BoundedContinuousFunction α E →L[ℝ] BoundedContinuousFunction α F →L[ℝ] BoundedContinuousFunction α G

The actual bilinear map on bounded continuous fields.

Equations

• EulerBoundedFieldCalculus.bilinearMap B = (EulerBoundedFieldCalculus.bilinearLinear B).mkContinuous₂ ‖B‖ ⋯

@[simp]

theorem EulerBoundedFieldCalculus.bilinearMap_apply {α : Type u_1} [TopologicalSpace α] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) (f : BoundedContinuousFunction α E) (g : BoundedContinuousFunction α F) (x : α) : (((bilinearMap B) f) g) x = (B (f x)) (g x)

theorem EulerBoundedFieldCalculus.bilinearMap_norm {α : Type u_1} [TopologicalSpace α] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) : ‖bilinearMap B‖ ≤ ‖B‖

theorem EulerBoundedFieldCalculus.postcomposition_norm {α : Type u_1} [TopologicalSpace α] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) : ‖ContinuousLinearMap.compLeftContinuousBounded α L‖ ≤ ‖L‖

Pointwise postcomposition preserves the coefficient map's norm bound.

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus11 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus12 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus13 {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (E →L[ℝ] F)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus13 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus14 {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (E →L[ℝ] F)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus14 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus15 {U : Type u_2} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (U →L[ℝ] F)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus15 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus16 {U : Type u_2} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (U →L[ℝ] F)

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus16 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus17 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus18 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus19 {α : Type u_1} [TopologicalSpace α] {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (BoundedContinuousFunction α (E →L[ℝ] F))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus19 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus20 {α : Type u_1} [TopologicalSpace α] {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (BoundedContinuousFunction α (E →L[ℝ] F))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus20 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus21 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (BoundedContinuousFunction α (U →L[ℝ] F))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus21 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus22 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (BoundedContinuousFunction α (U →L[ℝ] F))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus22 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus23 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (BoundedContinuousFunction α (U →L[ℝ] E) →L[ℝ] BoundedContinuousFunction α (U →L[ℝ] F))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus23 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus24 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (BoundedContinuousFunction α (U →L[ℝ] E) →L[ℝ] BoundedContinuousFunction α (U →L[ℝ] F))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus24 = inferInstance

noncomputable def EulerBoundedFieldCalculus.compositionMap {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : BoundedContinuousFunction α (E →L[ℝ] F) →L[ℝ] BoundedContinuousFunction α (U →L[ℝ] E) →L[ℝ] BoundedContinuousFunction α (U →L[ℝ] F)

The literal composition of two bounded operator fields.

Equations

• EulerBoundedFieldCalculus.compositionMap = EulerBoundedFieldCalculus.bilinearMap (ContinuousLinearMap.compL ℝ U E F)

theorem EulerBoundedFieldCalculus.compositionMap_norm {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ‖compositionMap‖ ≤ 1

@[simp]

theorem EulerBoundedFieldCalculus.compositionMap_apply {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) (B : BoundedContinuousFunction α (U →L[ℝ] E)) (x : α) : ((compositionMap A) B) x = A x ∘SL B x

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus25 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Type u_5} [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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus25 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus26 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Type u_5} [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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus26 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus27 {α : Type u_1} [TopologicalSpace α] {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_5} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction α (E →L[ℝ] F))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus27 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus28 {α : Type u_1} [TopologicalSpace α] {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_5} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction α (E →L[ℝ] F))

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus28 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus29 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus30 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus31 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus32 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus33 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus34 = inferInstance

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

Pointwise spatial composition, uniformly along a compact time path.

Equations

• EulerBoundedFieldCalculus.pathCompositionMap = EulerContinuousPathCalculus.coefficientMap ∘SL ContinuousLinearMap.compLeftContinuous ℝ K EulerBoundedFieldCalculus.compositionMap

@[simp]

theorem EulerBoundedFieldCalculus.pathCompositionMap_apply {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_5} [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction α (E →L[ℝ] F))) (B : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (t : K) (x : α) : (((pathCompositionMap A) B) t) x = (A t) x ∘SL (B t) x

theorem EulerBoundedFieldCalculus.pathCompositionMap_norm {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_5} [TopologicalSpace K] [CompactSpace K] : ‖pathCompositionMap‖ ≤ 1

theorem EulerBoundedFieldCalculus.pathComposition_contDiff {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_5} [TopologicalSpace K] [CompactSpace K] {P : Type u_6} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, BoundedContinuousFunction α (E →L[ℝ] F))) (B : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) {n : WithTop ℕ∞} (hA : ContDiff ℝ n A) (hB : ContDiff ℝ n B) : ContDiff ℝ n fun (y : P) => (pathCompositionMap (A y)) (B y)

Genuine smoothness of pointwise field composition in the uniform time-space norm.

theorem EulerBoundedFieldCalculus.pathComposition_bound {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_5} [TopologicalSpace K] [CompactSpace K] {P : Type u_6} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, BoundedContinuousFunction α (E →L[ℝ] F))) (B : P → C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (c d : ℕ) (hbA : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R c n) (hbB : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n B x‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (pathCompositionMap (A y)) (B y)) x‖ ≤ 3 * C * D * EulerGevrey.majorant R (c + d) n

The actual field product has the same factorial convolution bound.

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus35 {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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus35 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus36 {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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus36 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus37 {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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus37 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus38 {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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus38 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus39 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus39 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus40 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus40 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus41 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus41 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus42 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus42 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus43 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus44 = inferInstance

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

The actual adjoint of every bounded coefficient operator.

Equations

• EulerBoundedFieldCalculus.adjointMap = ContinuousLinearMap.compLeftContinuousBounded α EulerTransverseGramInverse.realAdjoint

@[simp]

theorem EulerBoundedFieldCalculus.adjointMap_apply {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A : BoundedContinuousFunction α (U →L[ℝ] E)) (x : α) : (adjointMap A) x = ContinuousLinearMap.adjoint (A x)

theorem EulerBoundedFieldCalculus.adjointMap_norm {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : ‖adjointMap‖ ≤ 1

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus45 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus45 = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedFieldCalculus.instBoundedFieldCalculus46 {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [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

• EulerBoundedFieldCalculus.instBoundedFieldCalculus46 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus47 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus48 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus49 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerBoundedFieldCalculus.instBoundedFieldCalculus50 = inferInstance

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

The bounded adjoint map on entire coefficient paths.

Equations

• EulerBoundedFieldCalculus.pathAdjointMap = ContinuousLinearMap.compLeftContinuous ℝ K EulerBoundedFieldCalculus.adjointMap

@[simp]

theorem EulerBoundedFieldCalculus.pathAdjointMap_apply {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : Type u_4} [TopologicalSpace K] (A : C(K, BoundedContinuousFunction α (U →L[ℝ] E))) (t : K) (x : α) : ((pathAdjointMap A) t) x = ContinuousLinearMap.adjoint ((A t) x)

theorem EulerBoundedFieldCalculus.pathAdjointMap_norm {α : Type u_1} [TopologicalSpace α] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] : ‖pathAdjointMap‖ ≤ 1