Spaces of analytic functions
Hardy, Bergman, Dirichlet and Fock spaces and their reproducing kernels, H^∞, boundary behaviour (Fatou, F. and M. Riesz), cyclicity and polynomial density.
- Bergman space
- Dirichlet space
- Finitely generated ideals of H^∞
- Fock space
- Hardy space
- Lacunary power series on the unit disc
TheoremF. and M. Riesz theorem#●ready to prove
Let \(\mu\) be a complex Borel measure on the circle \(\mathbb{T} = \mathbb{R}/\mathbb{Z}\). If \(\int_{\mathbb{T}} e^{2\pi i n z} \, d\mu(z) = 0\) for every integer \(n \ge 1\), then \(\mu\) is absolutely continuous with respect to the Haar probability measure on \(\mathbb{T}\).
public theorem_wanted riesz_brothers_theorem (μ : ComplexMeasure UnitAddCircle)
(hμ : ∀ n : ℕ, 1 ≤ n → ∫ᵛ z, fourier n z ∂[ContinuousLinearMap.mul ℝ ℂ; μ] = 0) :
μ ≪ᵥ AddCircle.haarAddCircle.toENNRealVectorMeasureSources
- W. Rudin, Real and Complex Analysis; N. K. Nikolski, Operators, Functions, and Systems: An Easy Reading, Volume I: Hardy, Hankel, and Toeplitz. Problem
riesz_brothers_theoremof the lean-eval benchmark.
TheoremFatou's theorem on radial limits#✓fully proved
Let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic and bounded on the open unit disc \(|z| < 1\). Then for Lebesgue-almost every \(\theta \in [0, 2\pi]\) the radial limit \(\lim_{r \to 1^-} f(r e^{i\theta})\) exists in \(\mathbb{C}\).
theorem fatou_radial_limit
(f : ℂ → ℂ)
(hf_diff : DifferentiableOn ℂ f (Metric.ball (0 : ℂ) 1))
(hf_bdd : ∃ M : ℝ, ∀ z ∈ Metric.ball (0 : ℂ) 1, ‖f z‖ ≤ M) :
∀ᵐ θ : ℝ ∂(volume.restrict (Icc (0 : ℝ) (2 * Real.pi))),
∃ L : ℂ,
Filter.Tendsto (fun r : ℝ =>
f ((r : ℂ) * Complex.exp ((θ : ℂ) * Complex.I))) (𝓝[<] (1 : ℝ)) (𝓝 L)Sources
- Fatou radial limit theorem for H∞, P. Fatou, Acta Math. 30 (1906); see Rudin, Real and Complex Analysis, Bounded Analytic Functions; Lean is bounded holomorphic on ball 0 1 with a.e. radial limit via volume.restrict Icc 0 (2π) and 𝓝[<] 1.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.