The original MicroPython allows for a soft PWM with a maximum frequency of 1 kHz. Simulation with LTspice and the provided net list shows that there is a significant ripple on the HV output on this frequency. With a PWM frequency of 10 kHz this ripple is almost not present.

To allow a 10 kHz PWM signal from the ESP8266 the following small changes to esp8266/esppwm.c are necessary:

diff --git a/esp8266/esppwm.c b/esp8266/esppwm.c
index f1d7060..e8c787b 100644
--- a/esp8266/esppwm.c
+++ b/esp8266/esppwm.c
@@ -25,8 +25,8 @@
 #define ICACHE_RAM_ATTR // __attribute__((section(".text")))
 
 #define PWM_CHANNEL 8
-#define PWM_DEPTH 1023
-#define PWM_FREQ_MAX 1000
+#define PWM_DEPTH 100
+#define PWM_FREQ_MAX 10000
 #define PWM_1S 1000000
 
 struct pwm_single_param {

You could choose any values you'd like, as long as the product of PWM_DEPTH and PWM_FREQ_MAX does not exceed PWM_1S. I've tested it with a logic analyzer and it seems to work fine.