Actual nonlinear products of smooth continuous cylinder paths

The existing complete H6 multiplication constructs the product. Its real mixed translation orbit is smooth because each input has a smooth H6 orbit. The output representative is the literal pointwise product at every point.

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct1 {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

• EulerCylinderPathProduct.instCylinderPathProduct1 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct2 {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

• EulerCylinderPathProduct.instCylinderPathProduct2 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct3 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {E : Type u_2} [NormedAddCommGroup E] : NormedAddCommGroup C(K, E)

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

Equations

• EulerCylinderPathProduct.instCylinderPathProduct3 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct4 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ C(K, E)

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

Equations

• EulerCylinderPathProduct.instCylinderPathProduct4 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct5 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {F : Type u_3} [NormedAddCommGroup F] : NormedAddCommGroup C(K, F)

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

Equations

• EulerCylinderPathProduct.instCylinderPathProduct5 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct6 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ C(K, F)

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

Equations

• EulerCylinderPathProduct.instCylinderPathProduct6 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct7 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {G : Type u_4} [NormedAddCommGroup G] : NormedAddCommGroup C(K, G)

Cache the standard NormedAddCommGroup C(K,G) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPathProduct.instCylinderPathProduct7 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct8 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] : NormedSpace ℝ C(K, G)

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

Equations

• EulerCylinderPathProduct.instCylinderPathProduct8 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct9 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {F : Type u_3} {G : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] : NormedAddCommGroup (C(K, F) →L[ℝ] C(K, G))

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

Equations

• EulerCylinderPathProduct.instCylinderPathProduct9 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathProduct10 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {F : Type u_3} {G : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] : NormedSpace ℝ (C(K, F) →L[ℝ] C(K, G))

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

Equations

• EulerCylinderPathProduct.instCylinderPathProduct10 = inferInstance

noncomputable def EulerCylinderPathProduct.pathBilinear {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {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) : C(K, E) →L[ℝ] C(K, F) →L[ℝ] C(K, G)

A genuine bounded bilinear map acts pointwise on continuous paths.

Equations

• EulerCylinderPathProduct.pathBilinear B = EulerContinuousPathCalculus.coefficientMap ∘SL ContinuousLinearMap.compLeftContinuous ℝ K B

@[simp]

theorem EulerCylinderPathProduct.pathBilinear_apply {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {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) (p : C(K, E)) (q : C(K, F)) (t : K) : (((pathBilinear B) p) q) t = (B (p t)) (q t)

theorem EulerCylinderPathProduct.pathBilinear_norm {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {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) : ‖pathBilinear B‖ ≤ ‖B‖

theorem EulerCylinderPathProduct.contDiff_pathBilinear {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {X : Type u_5} [NormedAddCommGroup X] [NormedSpace ℝ X] (B : E →L[ℝ] F →L[ℝ] G) (f : X → C(K, E)) (g : X → C(K, F)) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ ↑⊤ fun (x : X) => ((pathBilinear B) (f x)) (g x)

noncomputable def EulerCylinderPathProduct.scalarProductPath {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

The actual continuous L² product, constructed in the complete H6 algebra.

Equations

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

theorem EulerCylinderPathProduct.scalarProductPath_apply {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (t : K) : (scalarProductPath P L hL p q hp hq) t = EulerSobolevL2Product.scalarProduct P scalarProductPath_apply._proof_1 L ((EulerCylinderSmoothOrbit.sobolevPath P 6 p hp) t) (q t)

theorem EulerCylinderPathProduct.scalarProductPath_orbit_formula {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (a : EulerLiftedGradientSpace.LiftTangent) : (EulerLpCylinderTranslation.pathTranslate P a) (scalarProductPath P L hL p q hp hq) = (ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderSobolevSpace.valueOperator P 6)) (((pathBilinear (EulerSobolevL2Product.productHqBilinear P scalarProductPath._proof_1 L hL)) (EulerCylinderSmoothOrbit.sobolevOrbit P 6 p hp a)) (EulerCylinderSmoothOrbit.sobolevOrbit P 6 q hq a))

theorem EulerCylinderPathProduct.scalarProductPath_orbit {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (scalarProductPath P L hL p q hp hq)

Smoothness is for the actual output translation orbit, not an auxiliary family.

theorem EulerCylinderPathProduct.scalarProductPath_ae {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (t : K) : ↑↑((scalarProductPath P L hL p q hp hq) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => L (EulerCylinderSmoothOrbit.pointField P p hp t x) • EulerCylinderSmoothOrbit.pointField P q hq t x

theorem EulerCylinderPathProduct.pointField_scalarProductPath {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (t : K) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerCylinderSmoothOrbit.pointField P (scalarProductPath P L hL p q hp hq) ⋯ t x = L (EulerCylinderSmoothOrbit.pointField P p hp t x) • EulerCylinderSmoothOrbit.pointField P q hq t x

The output smooth representative equals the literal nonlinear product everywhere.