Documentation

LeanPool.CaffarelliKohnNirenberg.Setting.Examples.ShearFlowEnergyDensity

Pointwise energy calculus for the viscous shear #

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

The kinetic-energy density of the shear.

Equations
Instances For
    source
    noncomputable def CKN.shearTransport (z : Foundation.Parabolic.Vec3 × ℝ) :
    ℝ

    The cubic scalar transport factor.

    Equations
    Instances For
      source
      theorem CKN.shearEnergy_smooth :
      ContDiff ℝ (↑⊤) shearEnergy

      Smoothness of the energy density.

      source
      theorem CKN.shearTransport_smooth :
      ContDiff ℝ (↑⊤) shearTransport

      Smoothness of the cubic transport factor.

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

      The energy has no derivative along the flow direction.

      source
      theorem CKN.shearEnergy_time (z : Foundation.Parabolic.Vec3 × ℝ) :
      timePartial shearEnergy z = -2 * shearEnergy z

      Time derivative of the energy density.

      source
      theorem CKN.shearTransport_spatial_zero (z : Foundation.Parabolic.Vec3 × ℝ) :
      spatialPartial shearTransport 0 z = 0

      The cubic transport also has zero flow-direction derivative.

      source
      theorem CKN.shearEnergy_second (z : Foundation.Parabolic.Vec3 × ℝ) (j : Fin 3) :
      spatialPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial shearEnergy j w) j z = if j = 1 then 2 * (shearSlope z * shearSlope z - shearEnergy z) else 0

      Second spatial derivatives of the energy density.

      source
      theorem CKN.shearFlow_energy (z : Foundation.Parabolic.ParabolicPoint) :
      Foundation.Parabolic.vec3EuclideanNorm (shearFlow z) ^ 2 = shearEnergy z

      The squared Euclidean speed is the scalar energy.

      source
      theorem CKN.shearFlow_gradientSq (z : Foundation.Parabolic.ParabolicPoint) :
      spatialGradientSq shearFlow shearFlowGrad z = shearSlope z * shearSlope z

      The squared gradient density is the squared transverse slope.