Derivatives of the phase transition factor

The smooth transition in the shifted normal phase is differentiated as a one-dimensional composition with the extended phase.

noncomputable def ESS.buShortPhaseArgument (scale y s : ℝ) : ℝ

The argument of the canonical transition profile in the normal phase factor.

Equations

• ESS.buShortPhaseArgument scale y s = 12 * ((ESS.buShortFExt y s - ESS.buShortB scale) / ESS.buShortB scale) + 9

noncomputable def ESS.buShortPhaseFactor (scale y s : ℝ) : ℝ

The smooth phase transition as a function of height and time.

Equations

• ESS.buShortPhaseFactor scale y s = CKN.smoothTransitionProfile (ESS.buShortPhaseArgument scale y s)

theorem ESS.buShortFExt_height_deriv_differentiable {y s : ℝ} (hy : 2 < y) (hs : 1 / 2 ≤ s) : DifferentiableAt ℝ (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortFExt q s) r) y

The first height derivative of the smooth phase is differentiable above the active height threshold.

theorem ESS.buShortPhaseArgument_deriv_height (scale y s : ℝ) : deriv (fun (r : ℝ) => buShortPhaseArgument scale r s) y = 12 / buShortB scale * deriv (fun (r : ℝ) => buShortFExt r s) y

The height derivative of the phase argument.

theorem ESS.buShortPhaseArgument_deriv_time (scale y s : ℝ) : deriv (fun (t : ℝ) => buShortPhaseArgument scale y t) s = 12 / buShortB scale * deriv (fun (t : ℝ) => buShortFExt y t) s

The time derivative of the phase argument.

theorem ESS.buShortPhaseFactor_deriv_height (scale y s : ℝ) : deriv (fun (r : ℝ) => buShortPhaseFactor scale r s) y = deriv CKN.smoothTransitionProfile (buShortPhaseArgument scale y s) * (12 / buShortB scale * deriv (fun (r : ℝ) => buShortFExt r s) y)

The height derivative of the phase transition factor.

theorem ESS.buShortPhaseFactor_deriv_time (scale y s : ℝ) : deriv (fun (t : ℝ) => buShortPhaseFactor scale y t) s = deriv CKN.smoothTransitionProfile (buShortPhaseArgument scale y s) * (12 / buShortB scale * deriv (fun (t : ℝ) => buShortFExt y t) s)

The time derivative of the phase transition factor.

theorem ESS.buShortPhaseFactor_deriv_height_twice {scale y s : ℝ} (hy : 2 < y) (hs : 1 / 2 ≤ s) : deriv (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortPhaseFactor scale q s) r) y = deriv (deriv CKN.smoothTransitionProfile) (buShortPhaseArgument scale y s) * (12 / buShortB scale * deriv (fun (r : ℝ) => buShortFExt r s) y) ^ 2 + deriv CKN.smoothTransitionProfile (buShortPhaseArgument scale y s) * (12 / buShortB scale * deriv (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortFExt q s) r) y)

The second height derivative of the phase transition factor on the active half-space strip.