@[reducible, inline]

noncomputable abbrev divRemovable_zero (f : ℂ → ℂ) : ℂ → ℂ

Equations

• divRemovable_zero f = Function.update (fun (z : ℂ) => f z / z) 0 (deriv f 0)

theorem divRemovable_zero_of_ne_zero {z : ℂ} (f : ℂ → ℂ) (z_ne_0 : z ≠ 0) : divRemovable_zero f z = f z / z

theorem AnalyticOn.divRemovable_zero {f : ℂ → ℂ} {s : Set ℂ} (sInNhds0 : s ∈ nhds 0) (zero : f 0 = 0) (o : IsOpen s) (analytic : AnalyticOn ℂ f s) : AnalyticOn ℂ (_root_.divRemovable_zero f) s

theorem AnalyticOn_divRemovable_zero_closedBall {f : ℂ → ℂ} {R : ℝ} (Rpos : 0 < R) (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R)) (zero : f 0 = 0) : AnalyticOn ℂ (divRemovable_zero f) (Metric.closedBall 0 R)

@[reducible, inline]

noncomputable abbrev schwartzQuotient (f : ℂ → ℂ) (M : ℝ) : ℂ → ℂ

Equations

• schwartzQuotient f M z = divRemovable_zero f z / (2 * ↑M - f z)

theorem AnalyticOn.schwartzQuotient {f : ℂ → ℂ} {R : ℝ} (M : ℝ) (Rpos : 0 < R) (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R)) (nonzero : ∀ z ∈ Metric.closedBall 0 R, 2 * ↑M - f z ≠ 0) (zero : f 0 = 0) : AnalyticOn ℂ (_root_.schwartzQuotient f M) (Metric.closedBall 0 R)

theorem Complex.norm_le_norm_two_mul_sub_of_re_le {M : ℝ} {x : ℂ} (Mpos : 0 < M) (hyp_re_x : x.re ≤ M) : ‖x‖ ≤ ‖2 * ↑M - x‖

theorem AnalyticOn.norm_le_of_norm_le_on_sphere {f : ℂ → ℂ} {C R r : ℝ} (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R)) (hyp_r : r ≤ R) (cond : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ C) (w : ℂ) (wInS : w ∈ Metric.closedBall 0 r) : ‖f w‖ ≤ C

theorem borelCaratheodory_closedBall {M R r : ℝ} {z : ℂ} {f : ℂ → ℂ} (Rpos : 0 < R) (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R)) (zeroAtZero : f 0 = 0) (Mpos : 0 < M) (realPartBounded : ∀ z ∈ Metric.closedBall 0 R, (f z).re ≤ M) (hyp_r : r < R) (hyp_z : z ∈ Metric.closedBall 0 r) : ‖f z‖ ≤ 2 * M * r / (R - r)