Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.norm_le_of_mem_ball_of_forall_sphere_norm_le

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/AbsMax.lean:20 to 34

Source documentation

If f is holomorphic on the disk ‖·‖ < r and bounded by C on the circle ‖·‖ = r, then ‖f z‖ ≤ C for every z in the disk.

Exact Lean statement

theorem norm_le_of_mem_ball_of_forall_sphere_norm_le {f : ℂ → F} {r C : ℝ} {z : ℂ}
    (hd : Differentiable ℂ f) (hrpos : 0 < r)
    (hz : z ∈ Metric.ball (0 : ℂ) r) (hsphere : ∀ u : ℂ, ‖u‖ = r → ‖f u‖ ≤ C) :
    ‖f z‖ ≤ C

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_le_of_mem_ball_of_forall_sphere_norm_le {f : ℂ → F} {r C : ℝ} {z : ℂ}    (hd : Differentiable ℂ f) (hrpos : 0 < r)    (hz : z ∈ Metric.ball (0 : ℂ) r) (hsphere : ∀ u : ℂ, ‖u‖ = r → ‖f u‖ ≤ C) :    ‖f z‖ ≤ C := by  let U : Set ℂ := Metric.ball (0 : ℂ) r  have hfront : ∀ u ∈ frontier U, ‖f u‖ ≤ C := by    intro u hu    have hur : ‖u‖ = r := by      have hfront' : frontier (Metric.ball (0 : ℂ) r) = Metric.sphere (0 : ℂ) r := by        simpa using (frontier_ball (x := (0 : ℂ)) (r := r) (ne_of_gt hrpos))      have : u ∈ Metric.sphere (0 : ℂ) r := by simpa [U, hfront'] using hu      simpa [Metric.mem_sphere, dist_zero_right] using this    exact hsphere u hur  exact norm_le_of_forall_mem_frontier_norm_le (f := f) (U := U) Metric.isBounded_ball    hd.diffContOnCl hfront (subset_closure hz)