Quadratic densities in the short-time rescaling

These densities abbreviate the source field energy and its two fixed Gaussian weights in the short-time half-space argument.

noncomputable def ESS.buShortQuadraticEnergy (scale : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Quadratic velocity and spatial-gradient energy of the rescaled source field.

Equations

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

noncomputable def ESS.buShortTangentialDensity (scale : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Tangential Gaussian density with the normal polynomial needed for the negative-phase error.

Equations

• ESS.buShortTangentialDensity scale w Dw z = Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * (1 + z.1 2) ^ 4 * ESS.buShortQuadraticEnergy scale w Dw z

noncomputable def ESS.buShortWeightedPolynomialDensity (scale a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Fixed-parameter shifted Carleman density with the polynomial height factor needed for the shell estimates.

Equations

• ESS.buShortWeightedPolynomialDensity scale a w Dw z = ESS.buShortShiftedWeight scale a z * (1 + z.1 2) ^ 4 * ESS.buShortQuadraticEnergy scale w Dw z

noncomputable def ESS.buShortWeightedDensity (scale a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Fixed-parameter shifted Carleman quadratic density.

Equations

• ESS.buShortWeightedDensity scale a w Dw z = ESS.buShortShiftedWeight scale a z * ESS.buShortQuadraticEnergy scale w Dw z