Source indexedlemma · leanprover/lean4:v4.32.0

Complex.exists_norm_bound_on_closedBall

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Basic.lean:29 to 35

Source documentation

A continuous complex-valued function is bounded on a closed ball.

Exact Lean statement

lemma exists_norm_bound_on_closedBall {f : ℂ → ℂ} {R : ℝ}
    (hcont : ContinuousOn f (Metric.closedBall (0 : ℂ) R)) :
    ∃ M : ℝ, 0 ≤ M ∧ ∀ z : ℂ, ‖z‖ ≤ R → ‖f z‖ ≤ M

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma exists_norm_bound_on_closedBall {f : ℂ → ℂ} {R : ℝ}    (hcont : ContinuousOn f (Metric.closedBall (0 : ℂ) R)) :    ∃ M : ℝ, 0 ≤ M ∧ ∀ z : ℂ, ‖z‖ ≤ R → ‖f z‖ ≤ M := by  have hcomp : IsCompact (Metric.closedBall (0 : ℂ) R) := isCompact_closedBall 0 R  obtain ⟨M, hM⟩ := hcomp.exists_bound_of_continuousOn hcont  refine ⟨max M 0, le_max_right _ _, fun z hz => ?_⟩  exact (hM z (Metric.mem_closedBall.mpr (by simpa using hz))).trans (le_max_left _ _)