An explicit viscous shear flow

The velocity has one component, depending only on the transverse coordinate and time. Its spatial gradient has only the entry in row zero, column one.

noncomputable def CKN.shearFlow (z : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Vec3

A decaying sinusoidal shear velocity.

Equations

• CKN.shearFlow z i = if i = 0 then Real.exp (-z.2) * Real.sin (z.1 1) else 0

noncomputable def CKN.shearFlowGrad (z : Foundation.Parabolic.ParabolicPoint) : Fin 3 → Foundation.Parabolic.Vec3

The explicit spatial gradient of the shear velocity.

Equations

• CKN.shearFlowGrad z i j = if i = 0 ∧ j = 1 then Real.exp (-z.2) * Real.cos (z.1 1) else 0

noncomputable def CKN.shearAmplitude (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The scalar amplitude of the velocity.

Equations

• CKN.shearAmplitude z = Real.exp (-z.2) * Real.sin (z.1 1)

noncomputable def CKN.shearSlope (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The transverse derivative of the amplitude.

Equations

• CKN.shearSlope z = Real.exp (-z.2) * Real.cos (z.1 1)

theorem CKN.shearAmplitude_smooth : ContDiff ℝ (↑⊤) shearAmplitude

The scalar amplitude is smooth on the ordinary product space.

theorem CKN.shearSlope_smooth : ContDiff ℝ (↑⊤) shearSlope

The transverse slope is smooth on the ordinary product space.

theorem CKN.shearFlow_smooth : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => shearFlow z

The vector velocity is smooth.

theorem CKN.shearFlowGrad_smooth : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => shearFlowGrad z

The explicit gradient is smooth.

theorem CKN.shearFlow_ne_zero : ∃ z ∈ spaceTimeSet Set.univ (Set.Ioo 0 1), shearFlow z ≠ 0

The shear is nonzero at a point strictly inside its time interval.

theorem CKN.shearAmplitude_spatial (z : Foundation.Parabolic.Vec3 × ℝ) (j : Fin 3) : spatialPartial shearAmplitude j z = if j = 1 then shearSlope z else 0

Spatial derivatives of the scalar amplitude.

theorem CKN.shearSlope_spatial (z : Foundation.Parabolic.Vec3 × ℝ) (j : Fin 3) : spatialPartial shearSlope j z = if j = 1 then -shearAmplitude z else 0

Spatial derivatives of the transverse slope.

theorem CKN.shearAmplitude_time (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial shearAmplitude z = -shearAmplitude z

The amplitude satisfies exponential time decay.

theorem CKN.shearFlow_weakGradient (U : Set Foundation.Parabolic.Vec3) (s : ℝ) (i : Fin 3) : HasWeakGradientOn U (fun (x : Vec 3) => shearFlow (x, s) i) fun (x : Vec 3) => shearFlowGrad (x, s) i

The supplied matrix is the weak spatial gradient on every open spatial set.