Weight on the compact cutoff support

The half-space Carleman weight is continuous on the compact support of the short-time cutoff, so it is bounded there for each fixed parameter.

noncomputable def ESS.buShortCarlemanWeight (a : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The half-space Carleman density at exponent three quarters.

Equations

• ESS.buShortCarlemanWeight a z = z.2 ^ 2 * Real.exp (2 * ESS.halfSpacePhase a (3 / 4) z)

theorem ESS.buShortCarlemanWeight_continuousOn_support (scale R ε a : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) : ContinuousOn (buShortCarlemanWeight a) (buCutSupportSet (buShortFullCutoff scale R hR ε))

The Carleman density is continuous on the compact support of the short-time scalar cutoff.