Spatial C³ regularity of a smooth periodic flow.

@[reducible, inline]

abbrev AVenhance.Infra.Flow.SpatialC3.FlowCML2 (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Type u_2

Continuous bilinear maps with values in the flow state space.

Equations

• AVenhance.Infra.Flow.SpatialC3.FlowCML2 𝕜 E = (E [×2]→L[𝕜] E)

@[reducible, inline]

abbrev AVenhance.Infra.Flow.SpatialC3.FlowCML3 (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Type u_2

Continuous trilinear maps with values in the flow state space.

Equations

• AVenhance.Infra.Flow.SpatialC3.FlowCML3 𝕜 E = (E [×3]→L[𝕜] E)

@[reducible, inline]

abbrev AVenhance.Infra.Flow.SpatialC3.FlowNestedBilinear (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Type u_2

Bilinear maps represented as nested continuous linear maps.

Equations

• AVenhance.Infra.Flow.SpatialC3.FlowNestedBilinear 𝕜 E = (E →L[𝕜] E →L[𝕜] E)

noncomputable def AVenhance.Infra.Flow.SpatialC3.flowCML2NestedEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : FlowCML2 𝕜 E ≃L[𝕜] FlowNestedBilinear 𝕜 E

The normed bilinear-map space, written as nested continuous linear maps in the second-variation API.

Equations

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

theorem AVenhance.Infra.Flow.SpatialC3.flowCML2NestedEquiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (A : FlowCML2 𝕜 E) (h k : E) : (((flowCML2NestedEquiv E) A) h) k = A ![h, k]

theorem AVenhance.Infra.Flow.flow_spatial_contDiff_three_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) (hst : s ≤ t) : ContDiff ℝ 3 fun (x : Homogenization.Vec 2) => X t x s

On a forward interval, the selected third variation is the derivative of the second spatial derivative, and the fixed-time flow is spatially C³.

theorem AVenhance.Infra.Flow.flow_spatial_contDiff_three {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) : ContDiff ℝ 3 fun (x : Homogenization.Vec 2) => X t x s

Every fixed-time map of a smooth flow is spatially C³.