A (very weak!) upper bound on the area of the Mandelbrot set

Stream: maths

[Geoffrey Irving]

My power series code is far enough along that I can get the following (super weak) upper bound on the area of the Mandelbrot set from the first 256 terms of the Böttcher series:

/-- An (very weak!) upper bound on the area of the Mandelbrot set -/
lemma area_mandelbrot_le : volume.real mandelbrot ≤ 0.63006 * π := by
  refine le_trans (area_mandelbrot_le_supper (n := 256) (by norm_num)) ?_
  simp only [mul_comm π, mul_le_mul_iff_of_pos_right Real.pi_pos,
    (by norm_num : (0.63006 : ℝ) = (0.63006 : ℚ)), Rat.cast_le]
  native_decide

0.63006 * π is about 1.9794, and by contrast going out to 2 ^ 27 terms using CUDA rather than 256 gives the intermediate strength upper bound of 1.651587035834859. The much stronger method is ruling out small disks via the Koebe quarter theorem which gets to 1.50296686 < μ(M) < 1.57012937 (Fisher and Hill 1993); I'll start in on a verified version of that method once the next version of Lean rolls out.

[Geoffrey Irving]

@Kim Morrison More use of dyadic rationals: all of the inner loops are over docs#Dyadic. :)