Lacunary power series on the unit disc

DefinitionA lacunary power series#✓fully proved

For \(z \in \mathbb{C}\), let \(f(z) = \sum_{j=0}^{\infty} 2^{-j} z^{2^j}\), where \(f(z)\) is taken to be \(0\) when the series is not summable.

noncomputable def f (z : ℂ) : ℂ :=
  ∑' j : ℕ, ((1 / (2 : ℂ)) ^ j) * z ^ (2 ^ j)

Used by 1

Used byRegularity of a lacunary series on the unit disc

TheoremRegularity of a lacunary series on the unit disc#●ready to prove

Let \(f\) be the lacunary series \(f(z) = \sum_{j=0}^{\infty} 2^{-j} z^{2^j}\). Then \(f\) is holomorphic on the open unit disc \(\{z \in \mathbb{C} : |z| < 1\}\) and continuous on its closure, the closed unit disc \(\{z \in \mathbb{C} : |z| \le 1\}\).

public theorem_wanted differentiableOn_ball_continuousOn_closedBall_lacunary :
    DifferentiableOn ℂ f (Metric.ball 0 1) ∧
      ContinuousOn f (closure (Metric.ball 0 1))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; Series expansions of functions of one complex variable), problem ma_proofbench_l1_09.

Uses 1

Statement usesA lacunary power series

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.