theorem lem_2logOlog : (fun (t : ℝ) => 2 * Real.log t) =O[Filter.atTop] fun (t : ℝ) => Real.log t

theorem lem_logt22logt (t : ℝ) (_ht : t ≥ 2) : Real.log (t ^ 2) = 2 * Real.log t

theorem lem_log2tlogt2 (t : ℝ) (ht : t ≥ 2) : Real.log (2 * t) ≤ Real.log (t ^ 2)

theorem lem_log22log (t : ℝ) (ht : t ≥ 2) : Real.log (2 * t) ≤ 2 * Real.log t

theorem lem_exprule (n : ℕ) (hn : n ≥ 1) (α β : ℂ) : ↑n ^ (α + β) = ↑n ^ α * ↑n ^ β

theorem lem_realbw (b : ℝ) (w : ℂ) : (↑b * w).re = b * w.re

theorem lem_sumReal {f : ℕ+ → ℂ} (hf : Summable f) : (∑' (n : ℕ+), f n).re = ∑' (n : ℕ+), (f n).re

theorem lem_Euler (a : ℝ) : Complex.exp (↑a * Complex.I) = ↑(Real.cos a) + ↑(Real.sin a) * Complex.I

theorem lem_Reecos (a : ℝ) : (Complex.exp (↑a * Complex.I)).re = Real.cos a

theorem lem_explog (n : ℕ) (hn : n ≥ 1) : ↑n = Real.exp (Real.log ↑n)

theorem lem_coseven (a : ℝ) : Real.cos (-a) = Real.cos a

theorem lem_coseveny (n : ℕ) (_hn : n ≥ 1) (y : ℝ) : Real.cos (-y * Real.log ↑n) = Real.cos (y * Real.log ↑n)

theorem lem_niyelog (n : ℕ) (hn : n ≥ 1) (y : ℝ) : ↑n ^ (-↑y * Complex.I) = Complex.exp (-↑y * Complex.I * ↑(Real.log ↑n))

theorem lem_eacosalog (n : ℕ) (_hn : n ≥ 1) (y : ℝ) : (Complex.exp (-↑y * Complex.I * ↑(Real.log ↑n))).re = Real.cos (-y * Real.log ↑n)

theorem lem_eacosalog2 (n : ℕ) (hn : n ≥ 1) (y : ℝ) : (↑n ^ (-↑y * Complex.I)).re = Real.cos (-y * Real.log ↑n)

theorem lem_eacosalog3 (n : ℕ) (hn : n ≥ 1) (y : ℝ) : (↑n ^ (-↑y * Complex.I)).re = Real.cos (y * Real.log ↑n)

theorem lem_cos2t (θ : ℝ) : Real.cos (2 * θ) = 2 * Real.cos θ ^ 2 - 1

theorem lem_cos2t2 (θ : ℝ) : 2 * Real.cos θ ^ 2 = 1 + Real.cos (2 * θ)

theorem lem_cosSquare (θ : ℝ) : 2 * (1 + Real.cos θ) ^ 2 = 2 + 4 * Real.cos θ + 2 * Real.cos θ ^ 2

theorem lem_cos2cos341 (θ : ℝ) : 2 * (1 + Real.cos θ) ^ 2 = 3 + 4 * Real.cos θ + Real.cos (2 * θ)

theorem lem_SquarePos (y : ℝ) : 0 ≤ y ^ 2

theorem lem_SquarePos2 (y : ℝ) : 0 ≤ 2 * y ^ 2

theorem lem_SquarePoscos (θ : ℝ) : 0 ≤ 2 * (1 + Real.cos θ) ^ 2

theorem lem_postrig (θ : ℝ) : 0 ≤ 3 + 4 * Real.cos θ + Real.cos (2 * θ)

theorem lem_postriglogn (n : ℕ) (_hn : n ≥ 1) (t : ℝ) : 0 ≤ 3 + 4 * Real.cos (t * Real.log ↑n) + Real.cos (2 * t * Real.log ↑n)

theorem lem_seriesPos {r_n : ℕ+ → ℝ} {r : ℝ} (h_hasSum : HasSum r_n r) (h_nonneg : ∀ (n : ℕ+), r_n n ≥ 0) : r ≥ 0

theorem real_part_of_diff (M : ℝ) (w : ℂ) : (2 * ↑M - w).re = 2 * M - w.re

theorem real_part_of_diffz (M : ℝ) (f_z : ℂ) : (2 * ↑M - f_z).re = 2 * M - f_z.re

theorem inequality_reversal (x M : ℝ) (hxM : x ≤ M) : 2 * M - x ≥ M

theorem real_part_lower_bound (w : ℂ) (M : ℝ) (_hM : M > 0) (h : w.re ≤ M) : 2 * M - w.re ≥ M

theorem real_part_lower_bound2 (w : ℂ) (M : ℝ) (hM : M > 0) (h : w.re ≤ M) : (2 * ↑M - w).re ≥ M

theorem real_part_lower_bound3 (w : ℂ) (M : ℝ) (hM : M > 0) (h : w.re ≤ M) : (2 * ↑M - w).re > 0

theorem nonzero_if_real_part_positive (w : ℂ) (hw_re_pos : w.re > 0) : w ≠ 0

theorem lem_real_part_lower_bound4 (w : ℂ) (M : ℝ) (hM : M > 0) (h : w.re ≤ M) : 2 * ↑M - w ≠ 0

theorem lem_abspos (z : ℂ) : z ≠ 0 → ‖z‖ > 0

theorem lem_real_part_lower_bound5 (w : ℂ) (M : ℝ) (hM : M > 0) (h : w.re ≤ M) : ‖2 * ↑M - w‖ > 0

theorem lem_wReIm (w : ℂ) : w = ↑w.re + Complex.I * ↑w.im

theorem lem_modaib (a b : ℝ) : ‖↑a + Complex.I * ↑b‖ ^ 2 = a ^ 2 + b ^ 2

theorem lem_modcaib (a b c : ℝ) : ‖↑c - ↑a - Complex.I * ↑b‖ ^ 2 = (c - a) ^ 2 + b ^ 2

theorem lem_diffmods (a b c : ℝ) : ‖↑c - ↑a - Complex.I * ↑b‖ ^ 2 - ‖↑a + Complex.I * ↑b‖ ^ 2 = (c - a) ^ 2 - a ^ 2

theorem lem_casq (a c : ℝ) : (c - a) ^ 2 = a ^ 2 - 2 * a * c + c ^ 2

theorem lem_casq2 (a c : ℝ) : (c - a) ^ 2 - a ^ 2 = c * (c - 2 * a)

theorem lem_diffmods2 (a b c : ℝ) : ‖↑c - ↑a - Complex.I * ↑b‖ ^ 2 - ‖↑a + Complex.I * ↑b‖ ^ 2 = c * (c - 2 * a)

theorem lem_modulus_sq_ReImw (M : ℝ) (w : ℂ) : ‖2 * ↑M - w‖ ^ 2 - ‖w‖ ^ 2 = 4 * M * (M - w.re)

theorem lem_modulus_sq_identity (M : ℝ) (w : ℂ) : ‖2 * ↑M - w‖ ^ 2 - ‖w‖ ^ 2 = 4 * M * (M - w.re)

theorem lem_nonnegative_product (M x : ℝ) (hM : M > 0) (hxM : x ≤ M) : 4 * M * (M - x) ≥ 0

theorem lem_nonnegative_product2 (M : ℝ) (w : ℂ) (hM : M > 0) (hw_re_le_M : w.re ≤ M) : 4 * M * (M - w.re) ≥ 0

theorem lem_nonnegative_product3 (M : ℝ) (w : ℂ) (hM : M > 0) (hw_re_le_M : w.re ≤ M) : ‖2 * ↑M - w‖ ^ 2 - ‖w‖ ^ 2 ≥ 0

theorem lem_nonnegative_product4 (M : ℝ) (w : ℂ) (hM : M > 0) (hw_re_le_M : w.re ≤ M) : ‖2 * ↑M - w‖ ^ 2 ≥ ‖w‖ ^ 2

theorem lem_nonnegative_product5 (M : ℝ) (w : ℂ) (hM : M > 0) (hw_re_le_M : w.re ≤ M) : ‖2 * ↑M - w‖ ≥ ‖w‖

theorem lem_nonnegative_product6 (M : ℝ) (w : ℂ) (hM : M > 0) (hw_re_le_M : w.re ≤ M) : ‖w‖ ≤ ‖2 * ↑M - w‖

theorem lem_ineqmultr (a b c : ℝ) (hc : c > 0) (ha : 0 ≤ a) (hab : a ≤ b) : a / c ≤ b / c

theorem lem_ineqmultrbb (a b : ℝ) (hb : b > 0) (ha : 0 ≤ a) (hab : a ≤ b) : a / b ≤ 1

theorem lem_nonnegative_product7 (M : ℝ) (w : ℂ) (hM : M > 0) (h_abs_diff_pos : ‖2 * ↑M - w‖ > 0) (h_abs_le_abs_diff : ‖w‖ ≤ ‖2 * ↑M - w‖) : ‖w‖ / ‖2 * ↑M - w‖ ≤ 1

theorem lem_nonnegative_product8 (M : ℝ) (w : ℂ) (hM : M > 0) (hw_re_le_M : w.re ≤ M) (h_abs_le_abs_diff : ‖w‖ ≤ ‖2 * ↑M - w‖) : ‖w‖ / ‖2 * ↑M - w‖ ≤ 1

theorem lem_nonnegative_product9 (M : ℝ) (w : ℂ) (hM : M > 0) (hw_re_le_M : w.re ≤ M) : ‖w‖ / ‖2 * ↑M - w‖ ≤ 1

theorem lem_triangle_ineq (N G : ℂ) : ‖N + G‖ ≤ ‖N‖ + ‖G‖

theorem lem_triangleineqminus (N F : ℂ) : ‖N - F‖ ≤ ‖N‖ + ‖F‖

theorem lem_rtriangle (r : ℝ) (N F : ℂ) (hr : r > 0) : r * ‖N - F‖ ≤ r * (‖N‖ + ‖F‖)

theorem rtriangle2 (r : ℝ) (N F : ℂ) (hr : r > 0) : r * ‖N - F‖ ≤ r * ‖N‖ + r * ‖F‖

theorem lem_rtriangle3 (r R : ℝ) (N F : ℂ) (hr : r > 0) (hR : r < R) (h : R * ‖F‖ ≤ r * ‖N - F‖) : R * ‖F‖ ≤ r * ‖N‖ + r * ‖F‖

theorem lem_rtriangle4 (r R : ℝ) (N F : ℂ) (hr : 0 < r) (hR : r < R) (h_hyp : R * ‖F‖ ≤ r * ‖N - F‖) : (R - r) * ‖F‖ ≤ r * ‖N‖

theorem lem_absposeq (a : ℝ) (ha : a > 0) : |a| = a

theorem lem_a2a (a : ℝ) (ha : a > 0) : 2 * a > 0

theorem lem_absposeq2 (a : ℝ) (ha : a > 0) : |2 * a| = 2 * a

theorem lem_rtriangle5 (r R M : ℝ) (F : ℂ) (hr : 0 < r) (hrR : r < R) (hM : M > 0) (h_hyp : R * ‖F‖ ≤ r * ‖2 * ↑M - F‖) : (R - r) * ‖F‖ ≤ 2 * M * r

theorem lem_RrFpos (r R : ℝ) (F : ℂ) (hr : 0 < r) (hrR : r < R) : (R - r) * ‖F‖ ≥ 0

theorem lem_rtriangle6 (r R M : ℝ) (F : ℂ) (hr : 0 < r) (hrR : r < R) (hM : M > 0) (h_hyp : (R - r) * ‖F‖ ≤ 2 * M * r) : ‖F‖ ≤ 2 * M * r / (R - r)

theorem lem_rtriangle7 (r R M : ℝ) (F : ℂ) (hr : 0 < r) (hrR : r < R) (hM : M > 0) (h_hyp : R * ‖F‖ ≤ r * ‖2 * ↑M - F‖) : ‖F‖ ≤ 2 * M * r / (R - r)

def ballDR (R : ℝ) : Set ℂ

Equations

• ballDR R = Metric.ball 0 R

theorem analyticAt_to_analyticWithinAt {f : ℂ → ℂ} {S : Set ℂ} {z : ℂ} (hf : AnalyticAt ℂ f z) : AnalyticWithinAt ℂ f S z

theorem analyticWithinAt_to_analyticAt_aux {f : ℂ → ℂ} {S : Set ℂ} {z : ℂ} (hS : S ∈ nhds z) (p : FormalMultilinearSeries ℂ ℂ ℂ) (r : ENNReal) (h_conv_on_inter : r ≤ p.radius) (hr_pos : 0 < r) (hasSumt : ∀ {y : ℂ}, z + y ∈ insert z S → y ∈ EMetric.ball 0 r → HasSum (fun (n : ℕ) => (p n) fun (x : Fin n) => y) (f (z + y))) (ε : ℝ) (hε_pos : ε > 0) (h_ball_subset_S : Metric.ball z ε ⊆ S) : let r' := min r (ENNReal.ofReal ε); ∀ {y : ℂ}, y ∈ EMetric.ball 0 r' → HasSum (fun (n : ℕ) => (p n) fun (x : Fin n) => y) (f (z + y))

theorem analyticWithinAt_to_analyticAt {f : ℂ → ℂ} {S : Set ℂ} {z : ℂ} (hS : S ∈ nhds z) (h : AnalyticWithinAt ℂ f S z) : AnalyticAt ℂ f z

theorem lem_not0mono (R : ℝ) (hR_pos : 0 < R) (hR_lt_one : R < 1) : {z : ℂ | ‖z‖ ≤ R ∧ z ≠ 0} ⊆ {z : ℂ | z ≠ 0}

theorem lem_analmono {T S : Set ℂ} {f : ℂ → ℂ} (hS : AnalyticOn ℂ f S) (hT : T ⊆ S) : AnalyticOn ℂ f T

theorem lem_1zanalDR (R : ℝ) (hR_pos : 0 < R) : AnalyticOn ℂ (fun (z : ℂ) => z⁻¹) {z : ℂ | ‖z‖ ≤ R ∧ z ≠ 0}

theorem lem_analprod {T : Set ℂ} {f1 f2 : ℂ → ℂ} (hf1 : AnalyticOn ℂ f1 T) (hf2 : AnalyticOn ℂ f2 T) : AnalyticOn ℂ (f1 * f2) T

theorem lem_analprodST {T S : Set ℂ} {f1 f2 : ℂ → ℂ} (hTS : T ⊆ S) (hf1 : AnalyticOn ℂ f1 T) (hf2 : AnalyticOn ℂ f2 S) : AnalyticOn ℂ (f1 * f2) T

theorem lem_analprodTDR (R : ℝ) (f1 f2 : ℂ → ℂ) : AnalyticOn ℂ f1 {z : ℂ | ‖z‖ ≤ R ∧ z ≠ 0} → AnalyticOn ℂ f2 (Metric.closedBall 0 R) → AnalyticOn ℂ (f1 * f2) {z : ℂ | ‖z‖ ≤ R ∧ z ≠ 0}

theorem lem_fzzTanal {R : ℝ} (hR_pos : 0 < R) (f : ℂ → ℂ) (hf : AnalyticOn ℂ f (Metric.closedBall 0 R)) : AnalyticOn ℂ (fun (z : ℂ) => f z / z) {z : ℂ | ‖z‖ ≤ R ∧ z ≠ 0}

theorem lem_AnalOntoWithin {V : Set ℂ} {h : ℂ → ℂ} (hh : AnalyticOn ℂ h V) (z : ℂ) (hz : z ∈ V) : AnalyticWithinAt ℂ h V z

theorem lem_AnalWithintoOn {R : ℝ} (hR : 0 < R) (h : ℂ → ℂ) : (∀ z ∈ Metric.closedBall 0 R, AnalyticWithinAt ℂ h (Metric.closedBall 0 R) z) → AnalyticOn ℂ h (Metric.closedBall 0 R)

theorem lem_DR0T {R : ℝ} (hR : 0 < R) : Metric.closedBall 0 R = {0} ∪ {z : ℂ | ‖z‖ ≤ R ∧ z ≠ 0}

theorem lem_analWWWithin {R : ℝ} (hR_pos : 0 < R) (h : ℂ → ℂ) : AnalyticWithinAt ℂ h (Metric.closedBall 0 R) 0 → (∀ z ∈ {z : ℂ | ‖z‖ ≤ R ∧ z ≠ 0}, AnalyticWithinAt ℂ h (Metric.closedBall 0 R) z) → ∀ z ∈ Metric.closedBall 0 R, AnalyticWithinAt ℂ h (Metric.closedBall 0 R) z

theorem lem_analWWithinAtOn (R : ℝ) (hR_pos : 0 < R) (h : ℂ → ℂ) (h_at_0 : AnalyticWithinAt ℂ h (Metric.closedBall 0 R) 0) (h_at_T : ∀ z ∈ {z : ℂ | ‖z‖ ≤ R ∧ z ≠ 0}, AnalyticWithinAt ℂ h (Metric.closedBall 0 R) z) : AnalyticOn ℂ h (Metric.closedBall 0 R)

theorem lem_AnalAttoWithin {h : ℂ → ℂ} {s : Set ℂ} (hh : AnalyticAt ℂ h 0) : AnalyticWithinAt ℂ h s 0

theorem analyticWithinAt_punctured_to_closedBall {R : ℝ} (hR : 0 < R) {h : ℂ → ℂ} {z : ℂ} (hz : z ∈ {w : ℂ | ‖w‖ ≤ R ∧ w ≠ 0}) (h_within : AnalyticWithinAt ℂ h {w : ℂ | ‖w‖ ≤ R ∧ w ≠ 0} z) : AnalyticWithinAt ℂ h (Metric.closedBall 0 R) z

theorem lem_analAtOnOn {R : ℝ} (hR_pos : 0 < R) (h : ℂ → ℂ) : AnalyticAt ℂ h 0 → AnalyticOn ℂ h {z : ℂ | ‖z‖ ≤ R ∧ z ≠ 0} → AnalyticOn ℂ h (Metric.closedBall 0 R)

theorem lem_orderne0 (f : ℂ → ℂ) (hf : AnalyticAt ℂ f 0) (hf0 : f 0 = 0) : analyticOrderAt f 0 ≠ 0

theorem lem_ordernetop (f : ℂ → ℂ) (hf : AnalyticAt ℂ f 0) (hf_ne_zero : ¬∀ᶠ (z : ℂ) in nhds 0, f z = 0) : analyticOrderAt f 0 ≠ ⊤

theorem lem_ordernatcast (f : ℂ → ℂ) (hf : AnalyticAt ℂ f 0) (n : ℕ) (hn : analyticOrderAt f 0 = ↑n) : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g 0 ∧ g 0 ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds 0, f z = z ^ n * g z

theorem lem_ordernatcast1 (f : ℂ → ℂ) (hf : AnalyticAt ℂ f 0) (n : ℕ) (hn : analyticOrderAt f 0 = ↑n) (hn_ne_zero : n ≠ 0) : ∃ (h : ℂ → ℂ), AnalyticAt ℂ h 0 ∧ ∀ᶠ (z : ℂ) in nhds 0, f z = z * h z

theorem lem_ordernatcast2_old (f : ℂ → ℂ) (hf : AnalyticAt ℂ f 0) (hf0 : f 0 = 0) (h_not_eventually_zero : ¬∀ᶠ (z : ℂ) in nhds 0, f z = 0) : ∃ (h : ℂ → ℂ), AnalyticAt ℂ h 0 ∧ ∀ᶠ (z : ℂ) in nhds 0, f z = z * h z

theorem lem_ordernatcast2 {R : ℝ} (hR_pos : 0 < R) (f : ℂ → ℂ) (hf0 : f 0 = 0) (hf : AnalyticOn ℂ f (Metric.closedBall 0 R)) : AnalyticAt ℂ (fun (z : ℂ) => if z = 0 then (fderiv ℂ f 0) 1 else f z / z) 0

theorem ex (x : ℂ) {r : ℝ} (hr : r > 0) : closure (Metric.ball x r) = Metric.closedBall x r

theorem lem_ballDR (R : ℝ) (hR : R > 0) : closure (ballDR R) = Metric.closedBall 0 R

theorem lem_inDR (R : ℝ) (hR : R > 0) (w : ℂ) (hw : w ∈ closure (ballDR R)) : ‖w‖ ≤ R

theorem lem_notinDR (R : ℝ) (hR : R > 0) (w : ℂ) (hw : w ∉ ballDR R) : ‖w‖ ≥ R

theorem lem_legeR (R : ℝ) (hR : R > 0) (w : ℂ) (hw1 : ‖w‖ ≤ R) (hw2 : ‖w‖ ≥ R) : ‖w‖ = R

theorem lem_circleDR (R : ℝ) (hR : R > 0) (w : ℂ) (hw1 : w ∈ closure (ballDR R)) (hw2 : w ∉ ballDR R) : ‖w‖ = R

theorem lem_Rself (R : ℝ) (hR : R > 0) : |R| = R

theorem lem_Rself2 (R : ℝ) (hR : R > 0) : |R| ≤ R

theorem lem_Rself3 (R : ℝ) (hR : R > 0) : ↑R ∈ closure (ballDR R)

theorem lem_DRcompact (R : ℝ) (hR : R > 0) : IsCompact (closure (ballDR R))

theorem lem_ExtrValThm {K : Set ℂ} (hK : IsCompact K) (hK_nonempty : K.Nonempty) (g : ↑K → ℂ) (hg : Continuous g) : ∃ (v : ↑K), ∀ (z : ↑K), ‖g z‖ ≤ ‖g v‖

theorem lem_ExtrValThmDR (R : ℝ) (hR : R > 0) (g : ↑(closure (ballDR R)) → ℂ) (hg : Continuous g) : ∃ (v : ↑(closure (ballDR R))), ∀ (z : ↑(closure (ballDR R))), ‖g z‖ ≤ ‖g v‖

theorem lem_AnalCont {R : ℝ} (hR : R > 0) (H : ℂ → ℂ) (h_analytic : AnalyticOn ℂ H (closure (ballDR R))) : Continuous (H ∘ Subtype.val)

theorem lem_ExtrValThmh {R : ℝ} (hR : R > 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) : ∃ (u : ↑(closure (ballDR R))), ∀ (z : ↑(closure (ballDR R))), ‖h ↑u‖ ≥ ‖h ↑z‖

theorem lem_MaxModP (R : ℝ) (hR : R > 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) (w : ℂ) (hw_in_DR : w ∈ ballDR R) (hw_max : ∀ z ∈ ballDR R, ‖h z‖ ≤ ‖h w‖) (z : ℂ) : z ∈ closure (ballDR R) → ‖h z‖ = ‖h w‖

theorem lem_MaxModR (R : ℝ) (hR : R > 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) (w : ℂ) (hw_in_DR : w ∈ ballDR R) (hw_max : ∀ z ∈ ballDR R, ‖h z‖ ≤ ‖h w‖) : ‖h ↑R‖ = ‖h w‖

theorem lem_MaxModRR (R : ℝ) (hR : R > 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) (w : ℂ) (hw_in_DR : w ∈ ballDR R) (hw_max : ∀ z ∈ ballDR R, ‖h z‖ ≤ ‖h w‖) (z : ℂ) : z ∈ closure (ballDR R) → ‖h ↑R‖ ≥ ‖h z‖

theorem lem_MaxModv2 (R : ℝ) (hR : R > 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) : ∃ (v : ↑(closure (ballDR R))), ‖↑v‖ = R ∧ ∀ (z : ↑(closure (ballDR R))), ‖h ↑v‖ ≥ ‖h ↑z‖

theorem lem_MaxModv3 (R : ℝ) (hR : R > 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) : ∃ (v : ℂ), ‖v‖ = R ∧ ∀ z ∈ closure (ballDR R), ‖h v‖ ≥ ‖h z‖

theorem lem_MaxModv4 (R B : ℝ) (hR : R > 0) (hB : B ≥ 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) (h_boundary_bound : ∀ (z : ℂ), ‖z‖ = R → ‖h z‖ ≤ B) : ∃ (v : ℂ), ‖v‖ = R ∧ (∀ w ∈ closure (ballDR R), ‖h v‖ ≥ ‖h w‖) ∧ ‖h v‖ ≤ B

theorem lem_HardMMP (R B : ℝ) (hR : R > 0) (hB : B ≥ 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) (h_boundary_bound : ∀ (z : ℂ), ‖z‖ = R → ‖h z‖ ≤ B) (w : ℂ) : w ∈ closure (ballDR R) → ‖h w‖ ≤ B

theorem lem_EasyMMP (R B : ℝ) (hR : R > 0) (hB : B ≥ 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) (h_closure_bound : ∀ w ∈ closure (ballDR R), ‖h w‖ ≤ B) (z : ℂ) : ‖z‖ = R → ‖h z‖ ≤ B

theorem lem_MMP (R B : ℝ) (hR : R > 0) (hB : B ≥ 0) (h : ℂ → ℂ) (h_analytic : AnalyticOn ℂ h (closure (ballDR R))) : (∀ z ∈ closure (ballDR R), ‖h z‖ ≤ B) ↔ ∀ (z : ℂ), ‖z‖ = R → ‖h z‖ ≤ B

theorem lem_denominator_nonzero (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (z : ℂ) : z ∈ closure (ballDR R) → 2 * ↑M - f z ≠ 0

theorem lem_f_vs_2M_minus_f (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (z : ℂ) : z ∈ closure (ballDR R) → ‖f z‖ / ‖2 * ↑M - f z‖ ≤ 1

theorem fderiv_factorization_at_zero (R : ℝ) (hR : R > 0) (f h : ℂ → ℂ) (h_analytic_f : AnalyticOn ℂ f (closure (ballDR R))) (h_analytic_h : AnalyticOn ℂ h (closure (ballDR R))) (h_zero : f 0 = 0) (h_factor : ∀ z ∈ closure (ballDR R), f z = z * h z) : (fderiv ℂ f 0) 1 = h 0

theorem lem_removable_singularity (R : ℝ) (hR : R > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) : AnalyticOn ℂ (fun (z : ℂ) => if z = 0 then (fderiv ℂ f 0) 1 else f z / z) (closure (ballDR R))

theorem lem_quotient_analytic {R : ℝ} (hR : R > 0) (h1 h2 : ℂ → ℂ) (h_analytic1 : AnalyticOn ℂ h1 (closure (ballDR R))) (h_analytic2 : AnalyticOn ℂ h2 (closure (ballDR R))) (h_nonzero : ∀ z ∈ closure (ballDR R), h2 z ≠ 0) : AnalyticOn ℂ (fun (z : ℂ) => h1 z / h2 z) (closure (ballDR R))

noncomputable def f_M (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) : ℂ → ℂ

Equations

• f_M R M hR hM f h_analytic h_zero h_re_bound z = (if z = 0 then (fderiv ℂ f 0) 1 else f z / z) / (2 * ↑M - f z)

theorem lem_g_analytic (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) : AnalyticOn ℂ (f_M R M hR hM f h_analytic h_zero h_re_bound) (closure (ballDR R))

theorem lem_absab (a b : ℂ) (hb : b ≠ 0) : ‖a / b‖ = ‖a‖ / ‖b‖

theorem lem_g_on_boundaryz (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (z : ℂ) (hz_in_closure : z ∈ closure (ballDR R)) (hz_nonzero : z ≠ 0) : ‖f_M R M hR hM f h_analytic h_zero h_re_bound z‖ = ‖f z / z‖ / ‖2 * ↑M - f z‖

theorem lem_fzzR (R : ℝ) (hR : R > 0) (z w : ℂ) (hz : ‖z‖ = R) : ‖w / z‖ = ‖w‖ / R

theorem lem_g_on_boundary (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (z : ℂ) (hz_on_boundary : ‖z‖ = R) : ‖f_M R M hR hM f h_analytic h_zero h_re_bound z‖ = ‖f z‖ / R / ‖2 * ↑M - f z‖

theorem lem_f_vs_2M_minus_fR (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (z : ℂ) (hz_in_closure : z ∈ closure (ballDR R)) : ‖f z‖ / R / ‖2 * ↑M - f z‖ ≤ 1 / R

theorem lem_g_boundary_bound0 (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (z : ℂ) (hz_on_boundary : ‖z‖ = R) : ‖f_M R M hR hM f h_analytic h_zero h_re_bound z‖ ≤ 1 / R

theorem lem_g_interior_bound (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (z : ℂ) : z ∈ closure (ballDR R) → ‖f_M R M hR hM f h_analytic h_zero h_re_bound z‖ ≤ 1 / R

theorem lem_g_at_r (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (r : ℝ) (hr_pos : r > 0) (hr_lt_R : r < R) (z : ℂ) (hz_on_boundary : ‖z‖ = r) : ‖f_M R M hR hM f h_analytic h_zero h_re_bound z‖ = ‖f z‖ / r / ‖2 * ↑M - f z‖

theorem lem_g_at_rR (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (r : ℝ) (hr_pos : r > 0) (hr_lt_R : r < R) (z : ℂ) (hz_on_boundary : ‖z‖ = r) : ‖f z‖ / r / ‖2 * ↑M - f z‖ ≤ 1 / R

theorem lem_fracs (a b r R : ℝ) (ha : a > 0) (hb : b > 0) (hr : r > 0) (hR : R > 0) (h_le : a / r / b ≤ 1 / R) : R * a ≤ r * b

theorem lem_nonneg_product_with_real_abs (r M : ℝ) (hr : r > 0) (hM : M > 0) : 0 ≤ r * (2 * |M|)

theorem lem_f_bound_rearranged (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (r : ℝ) (hr_pos : r > 0) (hr_lt_R : r < R) (z : ℂ) (hz_on_boundary : ‖z‖ = r) : R * ‖f z‖ ≤ r * ‖2 * ↑M - f z‖

theorem lem_final_bound_on_circle0 (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (r : ℝ) (hr_pos : r > 0) (hr_lt_R : r < R) (z : ℂ) (hz_on_boundary : ‖z‖ = r) : ‖f z‖ ≤ 2 * r / (R - r) * M

theorem lem_final_bound_on_circle (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (r : ℝ) (hr_pos : r > 0) (hr_lt_R : r < R) (z : ℂ) (hz_on_boundary : ‖z‖ = r) : ‖f z‖ ≤ 2 * r / (R - r) * M

theorem lem_BCI (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (r : ℝ) (hr_pos : r > 0) (hr_lt_R : r < R) (z : ℂ) (hz_in_ball : ‖z‖ ≤ r) : ‖f z‖ ≤ 2 * r / (R - r) * M

theorem thm_BorelCaratheodoryI (R M : ℝ) (hR : R > 0) (hM : M > 0) (f : ℂ → ℂ) (h_analytic : AnalyticOn ℂ f (closure (ballDR R))) (h_zero : f 0 = 0) (h_re_bound : ∀ z ∈ closure (ballDR R), (f z).re ≤ M) (r : ℝ) (hr_pos : r > 0) (hr_lt_R : r < R) : sSup (norm ∘ f '' closure (ballDR r)) ≤ 2 * r / (R - r) * M

def I : ℂ

Equations

• I = Complex.I

theorem cauchy_formula_deriv {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : deriv f z = (1 / (2 * ↑Real.pi * I)) • ∮ (w : ℂ) in C(0, r_int), (w - z)⁻¹ ^ 2 • f w

theorem lem_dw_dt {r_int : ℝ} (t : ℝ) : deriv (fun (t' : ℂ) => ↑r_int * Complex.exp (I * t')) ↑t = I * ↑r_int * Complex.exp (I * ↑t)

theorem circleMap_zero_eq_exp (r t : ℝ) : circleMap 0 r t = ↑r * Complex.exp (I * ↑t)

theorem deriv_ofReal_eq_one (t : ℝ) : deriv Complex.ofReal t = 1

theorem differentiableAt_ofReal (t : ℝ) : DifferentiableAt ℝ Complex.ofReal t

theorem lem_dw_dt_real {r_int : ℝ} (t : ℝ) : deriv (fun (t' : ℝ) => ↑r_int * Complex.exp (I * ↑t')) t = I * ↑r_int * Complex.exp (I * ↑t)

theorem deriv_circleMap_zero (r t : ℝ) : deriv (circleMap 0 r) t = I * ↑r * Complex.exp (I * ↑t)

theorem lem_CIF_deriv_param {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : deriv f z = 1 / (2 * ↑Real.pi * I) * ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), I * ↑r_int * Complex.exp (I * ↑t) * (↑r_int * Complex.exp (I * ↑t) - z)⁻¹ ^ 2 * f (↑r_int * Complex.exp (I * ↑t))

theorem mul_comm_div_cancel (a b : ℂ) (ha : a ≠ 0) (hb : b ≠ 0) : a * b / (b * a) = 1

theorem complex_coeff_I_cancel : 1 / (2 * ↑Real.pi * I) * I = 1 / (2 * ↑Real.pi)

theorem factor_I_from_integrand (f : ℂ → ℂ) (r_int : ℝ) (z : ℂ) : ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), I * ↑r_int * Complex.exp (I * ↑t) * (↑r_int * Complex.exp (I * ↑t) - z)⁻¹ ^ 2 * f (↑r_int * Complex.exp (I * ↑t)) = I * ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), ↑r_int * Complex.exp (I * ↑t) * (↑r_int * Complex.exp (I * ↑t) - z)⁻¹ ^ 2 * f (↑r_int * Complex.exp (I * ↑t))

theorem integrand_transform_div (f : ℂ → ℂ) (r_int : ℝ) (z : ℂ) (t : ℝ) : ↑r_int * Complex.exp (I * ↑t) * (↑r_int * Complex.exp (I * ↑t) - z)⁻¹ ^ 2 * f (↑r_int * Complex.exp (I * ↑t)) = ↑r_int * Complex.exp (I * ↑t) * f (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2

theorem lem_CIF_deriv_simplified {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : deriv f z = 1 / (2 * ↑Real.pi) * ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), ↑r_int * Complex.exp (I * ↑t) * f (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2

theorem lem_modulus_of_f_prime0 {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ‖deriv f z‖ = ‖1 / (2 * ↑Real.pi) * ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), ↑r_int * Complex.exp (I * ↑t) * f (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖

theorem one_div_two_pi_pos : 1 / (2 * Real.pi) > 0

theorem abs_integral_le_integral_abs {a b : ℝ} {g : ℝ → ℂ} (hab : a ≤ b) : ‖∫ (t : ℝ) in Set.Icc a b, g t‖ ≤ ∫ (t : ℝ) in Set.Icc a b, ‖g t‖

theorem abs_ofReal_mul_complex (c : ℝ) (z : ℂ) (hc : c ≥ 0) : ‖↑c * z‖ = c * ‖z‖

theorem complex_abs_mul (a b : ℂ) : ‖a * b‖ = ‖a‖ * ‖b‖

theorem complex_abs_ofReal_nonneg (r : ℝ) (hr : r ≥ 0) : ‖↑r‖ = r

theorem abs_one_div_two_pi_complex : ‖1 / (2 * ↑Real.pi)‖ = 1 / (2 * Real.pi)

theorem lem_integral_modulus_inequality {r_int : ℝ} {z : ℂ} {f : ℂ → ℂ} : ‖1 / (2 * ↑Real.pi) * ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), ↑r_int * Complex.exp (I * ↑t) * f (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖ ≤ 1 / (2 * Real.pi) * ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), ‖↑r_int * Complex.exp (I * ↑t) * f (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖

theorem lem_modulus_of_f_prime {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ‖deriv f z‖ ≤ 1 / (2 * Real.pi) * ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), ‖↑r_int * Complex.exp (I * ↑t) * f (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖

theorem lem_modulus_of_integrand_product2 {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (t : ℝ) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) : ‖f (↑r_int * Complex.exp (I * ↑t)) * (↑r_int * Complex.exp (I * ↑t))‖ = ‖f (↑r_int * Complex.exp (I * ↑t))‖ * ‖↑r_int * Complex.exp (I * ↑t)‖

theorem lem_modeit (t : ℝ) : ‖Complex.exp (I * ↑t)‖ = Real.exp (I * ↑t).re

theorem lem_Reit0 (t : ℝ) : (I * ↑t).re = 0

theorem lem_eReite0 (t : ℝ) : Real.exp (I * ↑t).re = Real.exp 0

theorem lem_e01 : Real.exp 0 = 1

theorem lem_eReit1 (t : ℝ) : Real.exp (I * ↑t).re = 1

theorem lem_modulus_of_e_it_is_one (t : ℝ) : ‖Complex.exp (I * ↑t)‖ = 1

theorem lem_modulus_of_ae_it {a t : ℝ} (ha : 0 < a) : ‖↑a * Complex.exp (I * ↑t)‖ = a

theorem lem_modulus_of_integrand_product3 {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (t : ℝ) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) : ‖f (↑r_int * Complex.exp (I * ↑t)) * (↑r_int * Complex.exp (I * ↑t))‖ = r_int * ‖f (↑r_int * Complex.exp (I * ↑t))‖

theorem lem_modulus_of_square (c : ℂ) : ‖c ^ 2‖ = ‖c‖ ^ 2

theorem lem_modulus_wz (w z : ℂ) : ‖(w - z) ^ 2‖ = ‖w - z‖ ^ 2

theorem lem_reverse_triangle (w z : ℂ) : ‖w‖ - ‖z‖ ≤ ‖w - z‖

theorem lem_reverse_triangle2 {R_analytic r_z r_int t : ℝ} {z : ℂ} (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) : ‖↑r_int * Complex.exp (I * ↑t)‖ - ‖z‖ ≤ ‖↑r_int * Complex.exp (I * ↑t) - z‖

theorem lem_reverse_triangle3 {R_analytic r_z r_int t : ℝ} {z : ℂ} (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) : r_int - ‖z‖ ≤ ‖↑r_int * Complex.exp (I * ↑t) - z‖

theorem lem_zrr1 {R_analytic r_z r_int : ℝ} (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : 0 < r_int - ‖z‖

theorem lem_zrr2 {R_analytic r_z r_int t : ℝ} {z : ℂ} (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) (hz : z ∈ Metric.closedBall 0 r_z) : r_int - r_z ≤ ‖↑r_int * Complex.exp (I * ↑t) - z‖

theorem lem_rr11 {r r' : ℝ} (h_r_pos : 0 < r) (h_r_lt_r_prime : r < r') : r' - r > 0

theorem lem_rr12 {r r' : ℝ} (h_r_pos : 0 < r) (h_r_lt_r_prime : r < r') : (r' - r) ^ 2 > 0

theorem lem_zrr3 {R_analytic r_z r_int t : ℝ} {z : ℂ} (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) (hz : z ∈ Metric.closedBall 0 r_z) : (r_int - r_z) ^ 2 ≤ ‖↑r_int * Complex.exp (I * ↑t) - z‖ ^ 2

theorem lem_zrr4 {R_analytic r_z r_int : ℝ} (t : ℝ) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ‖(↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖ = ‖↑r_int * Complex.exp (I * ↑t) - z‖ ^ 2

theorem lem_reverse_triangle4 {R_analytic r_z r_int t : ℝ} {z : ℂ} (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) (hz : z ∈ Metric.closedBall 0 r_z) : 0 < ‖↑r_int * Complex.exp (I * ↑t) - z‖

theorem lem_wposneq0 (w : ℂ) : ‖w‖ > 0 → w ≠ 0

theorem lem_reverse_triangle5 {R_analytic r_z r_int : ℝ} (t : ℝ) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ↑r_int * Complex.exp (I * ↑t) - z ≠ 0

theorem lem_reverse_triangle6 {R_analytic r_z r_int : ℝ} (t : ℝ) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : (↑r_int * Complex.exp (I * ↑t) - z) ^ 2 ≠ 0

theorem lem_absdiv {a b : ℂ} (hb : b ≠ 0) : ‖a / b‖ = ‖a‖ / ‖b‖

theorem lem_modulus_of_integrand_product {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (t : ℝ) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ‖f (↑r_int * Complex.exp (I * ↑t)) * (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖ = ‖f (↑r_int * Complex.exp (I * ↑t)) * (↑r_int * Complex.exp (I * ↑t))‖ / ‖↑r_int * Complex.exp (I * ↑t) - z‖ ^ 2

theorem lem_modulus_of_product {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (t : ℝ) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ‖f (↑r_int * Complex.exp (I * ↑t)) * (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖ = r_int * ‖f (↑r_int * Complex.exp (I * ↑t))‖ / ‖↑r_int * Complex.exp (I * ↑t) - z‖ ^ 2

theorem lem_modulus_of_product2 {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (t : ℝ) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ‖f (↑r_int * Complex.exp (I * ↑t)) * (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖ = r_int * ‖f (↑r_int * Complex.exp (I * ↑t))‖ / ‖↑r_int * Complex.exp (I * ↑t) - z‖ ^ 2

theorem lem_modulus_of_product3 {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (t : ℝ) (hf : DifferentiableOn ℂ f (Metric.closedBall 0 R_analytic)) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : r_int * ‖f (↑r_int * Complex.exp (I * ↑t))‖ / ‖↑r_int * Complex.exp (I * ↑t) - z‖ ^ 2 ≤ r_int * ‖f (↑r_int * Complex.exp (I * ↑t))‖ / (r_int - r_z) ^ 2

theorem lem_modulus_of_product4 {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} (t : ℝ) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ‖f (↑r_int * Complex.exp (I * ↑t)) * (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖ ≤ r_int * ‖f (↑r_int * Complex.exp (I * ↑t))‖ / (r_int - r_z) ^ 2

theorem lem_bound_on_f_at_r_prime {M R_analytic r_int : ℝ} (hM_pos : 0 < M) (hR_analytic_pos : 0 < R_analytic) (hr_int_pos : 0 < r_int) (hr_int_lt_R_analytic : r_int < R_analytic) (f : ℂ → ℂ) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (hf0 : f 0 = 0) (hRe_f_le_M : ∀ z ∈ Metric.closedBall 0 R_analytic, (f z).re ≤ M) (t : ℝ) : ‖f (↑r_int * Complex.exp (I * ↑t))‖ ≤ 2 * r_int * M / (R_analytic - r_int)

theorem lem_bound_on_integrand_modulus {f : ℂ → ℂ} {M R_analytic r_z r_int : ℝ} (hM_pos : 0 < M) (hR_analytic_pos : 0 < R_analytic) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (hf0 : f 0 = 0) (hRe_f_le_M : ∀ w ∈ Metric.closedBall 0 R_analytic, (f w).re ≤ M) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) (t : ℝ) : ‖f (↑r_int * Complex.exp (I * ↑t)) * (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖ ≤ 2 * r_int ^ 2 * M / ((R_analytic - r_int) * (r_int - r_z) ^ 2)

theorem lem_integral_inequality_aux {g : ℝ → ℝ} {C a b : ℝ} (hab : a ≤ b) (h_integrable : IntervalIntegrable g MeasureTheory.volume a b) (h_bound : ∀ t ∈ Set.Icc a b, g t ≤ C) : ∫ (t : ℝ) in a..b, g t ≤ ∫ (t : ℝ) in a..b, C

theorem lem_integral_inequality {g : ℝ → ℝ} {C a b : ℝ} (hab : a ≤ b) (h_integrable : IntervalIntegrable g MeasureTheory.volume a b) (h_bound : ∀ t ∈ Set.Icc a b, g t ≤ C) : ∫ (t : ℝ) in Set.Icc a b, g t ≤ ∫ (t : ℝ) in Set.Icc a b, C

theorem continuous_real_parameterization (r : ℝ) : Continuous fun (t : ℝ) => ↑r * Complex.exp (I * ↑t)

theorem continuous_f_parameterized {f : ℂ → ℂ} {R r : ℝ} (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R ⊆ U ∧ DifferentiableOn ℂ f U) (hr_pos : 0 < r) (hr_lt_R : r < R) : Continuous fun (t : ℝ) => f (↑r * Complex.exp (I * ↑t))

theorem continuous_denominator_parameterized (r : ℝ) (z : ℂ) : Continuous fun (t : ℝ) => (↑r * Complex.exp (I * ↑t) - z) ^ 2

theorem interval_integrable_cauchy_integrand {f : ℂ → ℂ} {R_analytic r_z r_int : ℝ} {z : ℂ} (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) (hz : z ∈ Metric.closedBall 0 r_z) : IntervalIntegrable (fun (t : ℝ) => ‖↑r_int * Complex.exp (I * ↑t) * f (↑r_int * Complex.exp (I * ↑t)) / (↑r_int * Complex.exp (I * ↑t) - z) ^ 2‖) MeasureTheory.volume 0 (2 * Real.pi)

theorem integral_const_over_interval (C : ℝ) : ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), C = 2 * Real.pi * C

theorem lem_f_prime_bound_by_integral_of_constant {f : ℂ → ℂ} {M R_analytic r_z r_int : ℝ} (hM_pos : 0 < M) (hR_analytic_pos : 0 < R_analytic) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (hf0 : f 0 = 0) (hRe_f_le_M : ∀ w ∈ Metric.closedBall 0 R_analytic, (f w).re ≤ M) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ‖deriv f z‖ ≤ 2 * r_int ^ 2 * M / ((R_analytic - r_int) * (r_int - r_z) ^ 2)

theorem lem_integral_of_1 : ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), 1 = 2 * Real.pi

theorem lem_integral_2 : 1 / (2 * Real.pi) * ∫ (t : ℝ) in Set.Icc 0 (2 * Real.pi), 1 = 1

theorem lem_f_prime_bound {f : ℂ → ℂ} {M R_analytic r_z r_int : ℝ} (hM_pos : 0 < M) (hR_analytic_pos : 0 < R_analytic) (h_r_z_pos : 0 < r_z) (h_r_z_lt_r_int : r_z < r_int) (h_r_int_lt_R_analytic : r_int < R_analytic) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R_analytic ⊆ U ∧ DifferentiableOn ℂ f U) (hf0 : f 0 = 0) (hRe_f_le_M : ∀ w ∈ Metric.closedBall 0 R_analytic, (f w).re ≤ M) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r_z) : ‖deriv f z‖ ≤ 2 * r_int ^ 2 * M / ((R_analytic - r_int) * (r_int - r_z) ^ 2)

theorem lem_r_prime_gt_r {r R : ℝ} (h_r_pos : 0 < r) (h_r_lt_R : r < R) : r < (r + R) / 2

theorem lem_r_prime_lt_R {r R : ℝ} (h_r_pos : 0 < r) (h_r_lt_R : r < R) : (r + R) / 2 < R

theorem lem_r_prime_is_intermediate {r R : ℝ} (h_r_pos : 0 < r) (h_r_lt_R : r < R) : r < (r + R) / 2 ∧ (r + R) / 2 < R

theorem lem_calc_R_minus_r_prime {r R : ℝ} (h_r_pos : 0 < r) (h_r_lt_R : r < R) : R - (r + R) / 2 = (R - r) / 2

theorem lem_calc_r_prime_minus_r {r R : ℝ} (h_r_pos : 0 < r) (h_r_lt_R : r < R) : (r + R) / 2 - r = (R - r) / 2

theorem lem_calc_denominator_specific {r R : ℝ} (h_r_pos : 0 < r) (h_r_lt_R : r < R) : (R - (r + R) / 2) * ((r + R) / 2 - r) ^ 2 = (R - r) ^ 3 / 8

theorem lem_calc_numerator_specific {M r R : ℝ} (hM_pos : 0 < M) (hr_pos : 0 < r) (hr_lt_R : r < R) : 2 * ((r + R) / 2) ^ 2 * M = (R + r) ^ 2 * M / 2

theorem lem_frac_simplify {M r R : ℝ} (hM_pos : 0 < M) (hr_pos : 0 < r) (hr_lt_R : r < R) : let r_prime := (r + R) / 2; 2 * r_prime ^ 2 * M / ((R - r_prime) * (r_prime - r) ^ 2) = (R + r) ^ 2 * M / 2 / ((R - r) ^ 3 / 8)

theorem lem_frac_simplify2 {M r R : ℝ} (hM_pos : 0 < M) (hr_pos : 0 < r) (hr_lt_R : r < R) : (R + r) ^ 2 * M / 2 / ((R - r) ^ 3 / 8) = 4 * (R + r) ^ 2 * M / (R - r) ^ 3

theorem lem_frac_simplify3 {M r R : ℝ} (hM_pos : 0 < M) (hr_pos : 0 < r) (hr_lt_R : r < R) : let r_prime := (r + R) / 2; 2 * r_prime ^ 2 * M / ((R - r_prime) * (r_prime - r) ^ 2) = 4 * (R + r) ^ 2 * M / (R - r) ^ 3

theorem lem_ineq_R_plus_r_lt_2R {r R : ℝ} (h_r_lt_R : r < R) : R + r < 2 * R

theorem lem_R_plus_r_is_positive {r R : ℝ} (hr_pos : 0 < r) (hr_lt_R : r < R) : 0 < R + r

theorem lem_2R_is_positive {R : ℝ} (hR_pos : 0 < R) : 0 < 2 * R

theorem lem_square_inequality_strict {a b : ℝ} (h_a_pos : 0 < a) (h_a_lt_b : a < b) : a ^ 2 < b ^ 2

theorem lem_ineq_R_plus_r_sq_lt_2R_sq {r R : ℝ} (hr_pos : 0 < r) (hr_lt_R : r < R) : (R + r) ^ 2 < (2 * R) ^ 2

theorem lem_2R_sq_is_4R_sq {R : ℝ} (hR_pos : 0 < R) : (2 * R) ^ 2 = 4 * R ^ 2

theorem lem_ineq_R_plus_r_sq {r R : ℝ} (hr_pos : 0 < r) (hr_lt_R : r < R) : (R + r) ^ 2 < 4 * R ^ 2

theorem lem_ineq_R_plus_r_sqM {M r R : ℝ} (hM_pos : 0 < M) (hr_pos : 0 < r) (hr_lt_R : r < R) : 4 * (R + r) ^ 2 * M < 16 * R ^ 2 * M

theorem lem_simplify_final_bound {M r R : ℝ} (hM_pos : 0 < M) (hr_pos : 0 < r) (hr_lt_R : r < R) : 4 * (R + r) ^ 2 * M / (R - r) ^ 3 < 16 * R ^ 2 * M / (R - r) ^ 3

theorem lem_bound_after_substitution {M r R : ℝ} (hM_pos : 0 < M) (hr_pos : 0 < r) (hr_lt_R : r < R) : let r_prime := (r + R) / 2; 2 * r_prime ^ 2 * M / ((R - r_prime) * (r_prime - r) ^ 2) ≤ 16 * R ^ 2 * M / (R - r) ^ 3

theorem borel_caratheodory_II {f : ℂ → ℂ} {R M r : ℝ} (hR_pos : 0 < R) (hM_pos : 0 < M) (hr_pos : 0 < r) (hr_lt_R : r < R) (hf_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 R ⊆ U ∧ DifferentiableOn ℂ f U) (hf0 : f 0 = 0) (hRe_f_le_M : ∀ w ∈ Metric.closedBall 0 R, (f w).re ≤ M) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r) : ‖deriv f z‖ ≤ 16 * M * R ^ 2 / (R - r) ^ 3

noncomputable def If_taxicab {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) (f : ℂ → ℂ) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) : ↑(Metric.closedBall 0 r1) → ℂ

Definition 1: I_f defined along the taxicab (axis-aligned) path.

Equations

• If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf z = (∫ (t : ℝ) in 0 ..(↑z).re, f ↑t) + Complex.I * ∫ (τ : ℝ) in 0 ..(↑z).im, f (↑(↑z).re + Complex.I * ↑τ)

theorem def_If_z_plus_h {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) : If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z + h, hzh⟩ = (∫ (t : ℝ) in 0 ..(z + h).re, f ↑t) + Complex.I * ∫ (τ : ℝ) in 0 ..(z + h).im, f (↑(z + h).re + Complex.I * ↑τ)

Lemma: I_f(z+h) expands by definition.

theorem def_If_z {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r1) : If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z, hz⟩ = (∫ (t : ℝ) in 0 ..z.re, f ↑t) + Complex.I * ∫ (τ : ℝ) in 0 ..z.im, f (↑z.re + Complex.I * ↑τ)

Lemma: I_f(z) expands by definition.

theorem def_If_w {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : let w := ↑(z + h).re + Complex.I * ↑z.im; If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨w, hw⟩ = (∫ (t : ℝ) in 0 ..(z + h).re, f ↑t) + Complex.I * ∫ (τ : ℝ) in 0 ..z.im, f (↑(z + h).re + Complex.I * ↑τ)

Lemma: I_f(w) with w := (z+h).re + i*z.im.

theorem continuous_vertical_line (a : ℂ) : Continuous fun (τ : ℝ) => ↑a.re + Complex.I * ↑τ

theorem norm_re_add_I_mul_le_norm (a : ℂ) {τ : ℝ} (hτ : |τ| ≤ |a.im|) : ‖↑a.re + Complex.I * ↑τ‖ ≤ ‖a‖

theorem closedBall_mono_center0 {r1 R : ℝ} (h : r1 ≤ R) : Metric.closedBall 0 r1 ⊆ Metric.closedBall 0 R

theorem abs_le_abs_of_mem_uIcc_zero {b t : ℝ} (ht : t ∈ Set.uIcc 0 b) : |t| ≤ |b|

theorem vertical_intervalIntegrable_of_mem_ball {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {a : ℂ} (ha : a ∈ Metric.closedBall 0 r1) : IntervalIntegrable (fun (τ : ℝ) => f (↑a.re + Complex.I * ↑τ)) MeasureTheory.volume 0 a.im

theorem helper_im_of_w (z h : ℂ) : (↑(z + h).re + Complex.I * ↑z.im).im = z.im

theorem helper_mul_sub_complex (x y : ℂ) : Complex.I * x - Complex.I * y = Complex.I * (x - y)

theorem helper_re_of_w (z h : ℂ) : (↑(z + h).re + Complex.I * ↑z.im).re = (z + h).re

theorem diff_If_zh_w {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : let w := ↑(z + h).re + Complex.I * ↑z.im; If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z + h, hzh⟩ - If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨w, hw⟩ = Complex.I * ∫ (τ : ℝ) in z.im..(z + h).im, f (↑(z + h).re + Complex.I * ↑τ)

Lemma: I_f(z+h) - I_f(w) equals the vertical integral piece.

theorem diff_If_w_z_initial_form_vertical {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : let w := ↑(z + h).re + Complex.I * ↑z.im; If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z + h, hzh⟩ - If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨w, hw⟩ = Complex.I * ∫ (τ : ℝ) in z.im..(z + h).im, f (↑(z + h).re + Complex.I * ↑τ)

theorem diff_If_w_z_initial_form {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : let w := ↑(z + h).re + Complex.I * ↑z.im; If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨w, hw⟩ - If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z, hz⟩ = (∫ (t : ℝ) in z.re..w.re, f ↑t) + Complex.I * ∫ (τ : ℝ) in 0 ..z.im, f (↑w.re + Complex.I * ↑τ) - f (↑z.re + Complex.I * ↑τ)

theorem scalar_mul_integral_sub {a b : ℝ} (c : ℂ) (f g : ℝ → ℂ) (hf : IntervalIntegrable f MeasureTheory.volume a b) (hg : IntervalIntegrable g MeasureTheory.volume a b) : (c * ∫ (x : ℝ) in a..b, f x) - c * ∫ (x : ℝ) in a..b, g x = c * ∫ (x : ℝ) in a..b, f x - g x

theorem algebraic_rearrangement_four_terms (a b c d : ℂ) : a - b + c - d = 0 → c - d = b - a

theorem real_between_as_convex_combination (b₁ b₂ t : ℝ) (h : b₁ ≤ t ∧ t ≤ b₂ ∨ b₂ ≤ t ∧ t ≤ b₁) : ∃ (lam : ℝ), 0 ≤ lam ∧ lam ≤ 1 ∧ t = (1 - lam) * b₁ + lam * b₂

theorem convex_combination_mem_segment {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x y : E) (t : ℝ) (h₀ : 0 ≤ t) (h₁ : t ≤ 1) : (1 - t) • x + t • y ∈ segment ℝ x y

theorem vertical_line_in_segment (a : ℂ) (b₁ b₂ t : ℝ) (h : b₁ ≤ t ∧ t ≤ b₂ ∨ b₂ ≤ t ∧ t ≤ b₁) : a + Complex.I * ↑t ∈ segment ℝ (a + Complex.I * ↑b₁) (a + Complex.I * ↑b₂)

theorem horizontal_line_in_segment (a b₁ b₂ t : ℝ) (h : b₁ ≤ t ∧ t ≤ b₂ ∨ b₂ ≤ t ∧ t ≤ b₁) : ↑t + Complex.I * ↑a ∈ segment ℝ (↑b₁ + Complex.I * ↑a) (↑b₂ + Complex.I * ↑a)

theorem intervalIntegrable_of_continuousOn_range (f : ℂ → ℂ) (g : ℝ → ℂ) (a b : ℝ) (S : Set ℂ) (hf : ContinuousOn f S) (hg : Continuous g) (hrange : ∀ t ∈ Set.uIcc a b, g t ∈ S) : IntervalIntegrable (f ∘ g) MeasureTheory.volume a b

theorem intervalIntegrable_of_analyticOnNhd_of_endpoints_in_smaller_ball {r1 R : ℝ} (hr1_lt_R : r1 < R) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {a : ℂ} {b₁ b₂ : ℝ} (h₁ : ‖a + Complex.I * ↑b₁‖ ≤ r1) (h₂ : ‖a + Complex.I * ↑b₂‖ ≤ r1) : IntervalIntegrable (fun (t : ℝ) => f (a + Complex.I * ↑t)) MeasureTheory.volume b₁ b₂

theorem cauchy_for_rectangles {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z w : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hw : w ∈ Metric.closedBall 0 r1) (hzw : ↑w.re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) (hwz : ↑z.re + Complex.I * ↑w.im ∈ Metric.closedBall 0 r1) : (((∫ (x : ℝ) in z.re..w.re, f (↑x + Complex.I * ↑z.im)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + Complex.I * ↑w.im)) + Complex.I * ∫ (y : ℝ) in z.im..w.im, f (↑w.re + Complex.I * ↑y)) - Complex.I * ∫ (y : ℝ) in z.im..w.im, f (↑z.re + Complex.I * ↑y) = 0

Cauchy–Goursat for rectangles with mixed-corner hypotheses ensuring containment.

theorem cauchy_for_horizontal_strip {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : (((∫ (t : ℝ) in z.re..(z + h).re, f ↑t) - ∫ (t : ℝ) in z.re..(z + h).re, f (↑t + Complex.I * ↑z.im)) + Complex.I * ∫ (τ : ℝ) in 0 ..z.im, f (↑(z + h).re + Complex.I * ↑τ)) - Complex.I * ∫ (τ : ℝ) in 0 ..z.im, f (↑z.re + Complex.I * ↑τ) = 0

Horizontal-strip Cauchy identity specialized to w := (z+h).re + i z.im.

theorem integrability_from_cauchy_horizontal_strip {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : IntervalIntegrable (fun (τ : ℝ) => f (↑(z + h).re + Complex.I * ↑τ)) MeasureTheory.volume 0 z.im ∧ IntervalIntegrable (fun (τ : ℝ) => f (↑z.re + Complex.I * ↑τ)) MeasureTheory.volume 0 z.im

theorem cauchy_rearrangement_step1 {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : Complex.I * ∫ (τ : ℝ) in 0 ..z.im, f (↑(z + h).re + Complex.I * ↑τ) - f (↑z.re + Complex.I * ↑τ) = (∫ (t : ℝ) in z.re..(z + h).re, f (↑t + Complex.I * ↑z.im)) - ∫ (t : ℝ) in z.re..(z + h).re, f ↑t

theorem diff_If_w_z {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : let w := ↑(z + h).re + Complex.I * ↑z.im; If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨w, hw⟩ - If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z, hz⟩ = ∫ (t : ℝ) in z.re..(z + h).re, f (↑t + Complex.I * ↑z.im)

theorem If_difference_is_L_path_integral {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z + h, hzh⟩ - If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z, hz⟩ = (∫ (t : ℝ) in z.re..(z + h).re, f (↑t + Complex.I * ↑z.im)) + Complex.I * ∫ (τ : ℝ) in z.im..(z + h).im, f (↑(z + h).re + Complex.I * ↑τ)

Sum of the two differences gives the L-shaped path integral from z to z+h.

theorem If_diff_add_sub_identity {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z + h, hzh⟩ - If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z, hz⟩ = (∫ (t : ℝ) in z.re..(z + h).re, f (↑t + Complex.I * ↑z.im) - f z + f z) + Complex.I * ∫ (τ : ℝ) in z.im..(z + h).im, f (↑(z + h).re + Complex.I * ↑τ) - f z + f z

Add–subtract f z inside each integrand (pure algebra).

theorem intervalIntegrable_of_analyticOnNhd_of_horizontal_endpoints_in_smaller_ball {r1 R : ℝ} (hr1_lt_R : r1 < R) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {im_part a b : ℝ} (h₁ : ‖↑a + Complex.I * ↑im_part‖ ≤ r1) (h₂ : ‖↑b + Complex.I * ↑im_part‖ ≤ r1) : IntervalIntegrable (fun (t : ℝ) => f (↑t + Complex.I * ↑im_part)) MeasureTheory.volume a b

theorem If_diff_linearity {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z + h, hzh⟩ - If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z, hz⟩ = ((∫ (t : ℝ) in z.re..(z + h).re, f (↑t + Complex.I * ↑z.im) - f z) + ∫ (t : ℝ) in z.re..(z + h).re, f z) + Complex.I * ((∫ (τ : ℝ) in z.im..(z + h).im, f (↑(z + h).re + Complex.I * ↑τ) - f z) + ∫ (τ : ℝ) in z.im..(z + h).im, f z)

Apply linearity of the integral to split the two addends.

theorem integral_of_constant_over_L_path {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) : (∫ (t : ℝ) in z.re..(z + h).re, f z) + Complex.I * ∫ (τ : ℝ) in z.im..(z + h).im, f z = f z * h

Integrating the constant function along the L-path yields f z * h.

noncomputable def Err {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) (f : ℂ → ℂ) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) (z h : ℂ) : ℂ

Final decomposition with an explicit error term.

Equations

• One or more equations did not get rendered due to their size.

theorem CD_eq_fz_h {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) : (∫ (t : ℝ) in z.re..(z + h).re, f z) + Complex.I * ∫ (τ : ℝ) in z.im..(z + h).im, f z = f z * h

theorem If_diff_decomposition_final {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z + h, hzh⟩ - If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z, hz⟩ = f z * h + Err hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf z h

noncomputable def S_horiz (z h : ℂ) (f : ℂ → ℂ) : ℝ

Equations

• S_horiz z h f = sSup {r : ℝ | ∃ t ∈ Set.uIcc z.re (z + h).re, r = ‖f (↑t + Complex.I * ↑z.im) - f z‖}

noncomputable def S_vert (z h : ℂ) (f : ℂ → ℂ) : ℝ

Equations

• S_vert z h f = sSup {r : ℝ | ∃ τ ∈ Set.uIcc z.im (z + h).im, r = ‖f (↑(z + h).re + Complex.I * ↑τ) - f z‖}

noncomputable def S_max (z h : ℂ) (f : ℂ → ℂ) : ℝ

Equations

• S_max z h f = max (S_horiz z h f) (S_vert z h f)

theorem bound_on_Err {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) : ‖Err hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf z h‖ ≤ |h.re| * S_max z h f + |h.im| * S_max z h f

theorem S_horiz_nonneg (z h : ℂ) (f : ℂ → ℂ) : 0 ≤ S_horiz z h f

theorem S_max_nonneg (z h : ℂ) (f : ℂ → ℂ) : 0 ≤ S_max z h f

theorem bound_on_Err_ratio {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hz : z ∈ Metric.closedBall 0 r1) (hzh : z + h ∈ Metric.closedBall 0 r1) (hw : ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 r1) (hh : h ≠ 0) : ‖Err hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf z h / h‖ ≤ 2 * S_max z h f

theorem abs_horizontal_diff_eq_abs_real (z : ℂ) (t : ℝ) : ‖↑t + Complex.I * ↑z.im - z‖ = |t - z.re|

theorem abs_sub_le_of_mem_uIcc (a b t : ℝ) (ht : t ∈ Set.uIcc a b) : |t - a| ≤ |b - a| ∧ |b - t| ≤ |b - a|

theorem sub_ofReal_add_I (a b c d : ℝ) : ↑a + Complex.I * ↑b - (↑c + Complex.I * ↑d) = ↑(a - c) + Complex.I * (↑b - ↑d)

theorem abs_re_im_bound (a b : ℝ) : ‖↑a + Complex.I * ↑b‖ ≤ |a| + |b|

theorem norm_ofReal (x : ℝ) : ‖↑x‖ = |x|

theorem norm_I_mul_ofReal (b : ℝ) : ‖Complex.I * ↑b‖ = |b|

theorem abs_add_Ile (a b : ℝ) : ‖↑a + Complex.I * ↑b‖ ≤ |a| + |b|

theorem abs_vertical_diff_le_core (z h : ℂ) (τ : ℝ) : ‖↑((z + h).re - z.re) + Complex.I * (↑τ - ↑z.im)‖ ≤ |(z + h).re - z.re| + |τ - z.im|

theorem abs_vertical_core (z h : ℂ) (τ : ℝ) : ‖↑h.re + Complex.I * (↑τ - ↑z.im)‖ ≤ |h.re| + |τ - z.im|

theorem S_vert_nonneg (z h : ℂ) (f : ℂ → ℂ) : 0 ≤ S_vert z h f

theorem abs_im_le_norm (z : ℂ) : |z.im| ≤ ‖z‖

theorem mem_closedBall_mono_radius {z : ℂ} {r R : ℝ} (hz : z ∈ Metric.closedBall 0 r) (h : r ≤ R) : z ∈ Metric.closedBall 0 R

theorem tendsto_of_nonneg_local_bound {g : ℂ → ℝ} (h_nonneg : ∀ (h : ℂ), 0 ≤ g h) (h_loc : ∀ ε > 0, ∃ δ > 0, ∀ (h : ℂ), ‖h‖ < δ → g h ≤ ε) : Filter.Tendsto g (nhds 0) (nhds 0)

theorem sum_abs_le_two_mul {x y A : ℝ} (hx : |x| ≤ A) (hy : |y| ≤ A) : |x| + |y| ≤ 2 * A

theorem two_norm_lt_of_norm_lt_half {h : ℂ} {δ : ℝ} (_hpos : 0 < δ) (hbound : ‖h‖ < δ / 2) : 2 * ‖h‖ < δ

theorem limit_of_S_is_zero {r1 R R0 : ℝ} (_hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (_hR_lt_R0 : R < R0) (_hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r1) : Filter.Tendsto (fun (h : ℂ) => S_max z h f) (nhds 0) (nhds 0)

theorem eventually_corner_and_sum_in_closedBall {z : ℂ} {R' : ℝ} (hz : ‖z‖ < R') : ∀ᶠ (h : ℂ) in nhds 0, z + h ∈ Metric.closedBall 0 R' ∧ ↑(z + h).re + Complex.I * ↑z.im ∈ Metric.closedBall 0 R'

theorem limit_of_Err_ratio_is_zero {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r1) : Filter.Tendsto (fun (h : ℂ) => Err hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf z h / h) (nhds 0) (nhds 0)

noncomputable def If_ext {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) (f : ℂ → ℂ) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) : ℂ → ℂ

Extend If_taxicab to a total function on ℂ by zero outside the closed ball.

Equations

• If_ext hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf w = if h : w ∈ Metric.closedBall 0 r1 then If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨w, h⟩ else 0

theorem If_ext_eq_taxicab_of_mem {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) (f : ℂ → ℂ) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {w : ℂ} (hw : w ∈ Metric.closedBall 0 r1) : If_ext hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf w = If_taxicab hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf ⟨w, hw⟩

theorem If_taxicab_param_invariance {r1₁ r1₂ R R0 : ℝ} (hr1₁_pos : 0 < r1₁) (hr1₁_lt_R : r1₁ < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) (hr1₂_pos : 0 < r1₂) (hr1₂_lt_R : r1₂ < R) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {w : ℂ} (hw₁ : w ∈ Metric.closedBall 0 r1₁) (hw₂ : w ∈ Metric.closedBall 0 r1₂) : If_taxicab hr1₁_pos hr1₁_lt_R hR_lt_R0 hR0_lt_one f hf ⟨w, hw₁⟩ = If_taxicab hr1₂_pos hr1₂_lt_R hR_lt_R0 hR0_lt_one f hf ⟨w, hw₂⟩

theorem derivWithin_eq_deriv_of_isOpen_mem {s : Set ℂ} (hs : IsOpen s) {f : ℂ → ℂ} {z : ℂ} (hz : z ∈ s) : derivWithin f s z = deriv f z

theorem eventually_decomposition_for_ext {R' R R0 : ℝ} (hR'_pos : 0 < R') (hR'_lt_R : R' < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) (z : ℂ) (hz : ‖z‖ < R') : ∀ᶠ (h : ℂ) in nhds 0, let g := If_ext hR'_pos hR'_lt_R hR_lt_R0 hR0_lt_one f hf; g (z + h) - g z = f z * h + Err hR'_pos hR'_lt_R hR_lt_R0 hR0_lt_one f hf z h

theorem tendsto_Err_ratio_radius (R' R R0 : ℝ) (hR'_pos : 0 < R') (hR'_lt_R : R' < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z : ℂ} (hz : ‖z‖ < R') : Filter.Tendsto (fun (h : ℂ) => Err hR'_pos hR'_lt_R hR_lt_R0 hR0_lt_one f hf z h / h) (nhds 0) (nhds 0)

theorem If_ext_eq_taxicab_at_sum {R' R R0 : ℝ} (hR'_pos : 0 < R') (hR'_lt_R : R' < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z h : ℂ} (hzh : z + h ∈ Metric.closedBall 0 R') : If_ext hR'_pos hR'_lt_R hR_lt_R0 hR0_lt_one f hf (z + h) = If_taxicab hR'_pos hR'_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z + h, hzh⟩

theorem If_ext_eq_taxicab_at_point {R' R R0 : ℝ} (hR'_pos : 0 < R') (hR'_lt_R : R' < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) {z : ℂ} (hz : z ∈ Metric.closedBall 0 R') : If_ext hR'_pos hR'_lt_R hR_lt_R0 hR0_lt_one f hf z = If_taxicab hR'_pos hR'_lt_R hR_lt_R0 hR0_lt_one f hf ⟨z, hz⟩

theorem hasDerivWithinAt_congr_eqOn {f g : ℂ → ℂ} {s : Set ℂ} {z f' : ℂ} (hEq : Set.EqOn f g s) (hz : z ∈ s) : HasDerivWithinAt g f' s z → HasDerivWithinAt f f' s z

theorem differentiableOn_of_hasDerivWithinAt {f : ℂ → ℂ} {s : Set ℂ} {F : ℂ → ℂ} (h : ∀ z ∈ s, HasDerivWithinAt f (F z) s z) : DifferentiableOn ℂ f s

theorem If_ext_agree_on_smallBall {r1 R' R R0 : ℝ} (hr1_pos : 0 < r1) (hR'_pos : 0 < R') (hr1_lt_R : r1 < R) (hR'_lt_R : R' < R) (hr1_lt_R' : r1 < R') (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) : Set.EqOn (If_ext hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf) (If_ext hR'_pos hR'_lt_R hR_lt_R0 hR0_lt_one f hf) (Metric.closedBall 0 r1)

theorem hasDerivAt_of_local_decomposition' (g : ℂ → ℂ) (z F : ℂ) (Err_func : ℂ → ℂ) (hdecomp : ∀ᶠ (h : ℂ) in nhds 0, g (z + h) - g z = F * h + Err_func h) (hErr : Filter.Tendsto (fun (h : ℂ) => Err_func h / h) (nhds 0) (nhds 0)) : HasDerivAt g F z

theorem uniqueDiffWithinAt_convex_complex {s : Set ℂ} (hconv : Convex ℝ s) (hs : (interior s).Nonempty) {x : ℂ} (hx : x ∈ closure s) : UniqueDiffWithinAt ℂ s x

theorem interior_closedBall_nonempty_of_pos {R : ℝ} (hR_pos : 0 < R) : (interior (Metric.closedBall 0 R)).Nonempty

theorem mem_closure_of_mem_closedBall {R : ℝ} {z : ℂ} (hz : z ∈ Metric.closedBall 0 R) : z ∈ closure (Metric.closedBall 0 R)

theorem uniqueDiffWithinAt_closedBall_complex_of_mem {R : ℝ} {z : ℂ} (hR_pos : 0 < R) (hz : z ∈ Metric.closedBall 0 R) : UniqueDiffWithinAt ℂ (Metric.closedBall 0 R) z

theorem If_is_differentiable_on {r1 R R0 : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R : r1 < R) (hR_lt_R0 : R < R0) (hR0_lt_one : R0 < 1) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) : DifferentiableOn ℂ (If_ext hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf) (Metric.closedBall 0 r1) ∧ ∀ z ∈ Metric.closedBall 0 r1, derivWithin (If_ext hr1_pos hr1_lt_R hR_lt_R0 hR0_lt_one f hf) (Metric.closedBall 0 r1) z = f z

theorem AnalyticOnNhd.mono_closedBall {B : ℂ → ℂ} {R : ℝ} (R' : ℝ) (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hR' : R' < R) : AnalyticOnNhd ℂ B (Metric.closedBall 0 R')

theorem log_deriv_is_analytic {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R')) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 r1, B z ≠ 0) : AnalyticOnNhd ℂ (fun (z : ℂ) => deriv B z / B z) (Metric.closedBall 0 r1)

Lemma: B'/B is analyticOnNhd when B is analyticOnNhd and nonzero.

theorem I_is_antiderivative {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) : ∃ (J : ℂ → ℂ), AnalyticOnNhd ℂ J (Metric.closedBall 0 r1) ∧ J 0 = 0 ∧ ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z

Lemma: There exists J analyticOnNhd with J(0) = 0 and J'(z) = B'(z)/B(z).

noncomputable def H_auxiliary {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) (J : ℂ → ℂ) : ℂ → ℂ

Definition: H(z) := exp(J(z))/B(z) where J is from I_is_antiderivative.

Equations

• H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J z = Complex.exp (J z) / B z

theorem exp_I_at_zero {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) : Complex.exp (J 0) = 1

Lemma: exp(J(0)) = 1 when J(0) = 0.

theorem H_at_zero {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) : H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J 0 = 1 / B 0

Lemma: H(0) = 1/B(0).

theorem log_deriv_id {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → deriv J z * B z = deriv B z

Lemma: J'(z)B(z) = B'(z).

theorem log_deriv_identity {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → deriv J z * B z - deriv B z = 0

Lemma: J'(z)B(z) - B'(z) = 0.

theorem H_derivative_quotient_rule {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → deriv (H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J) z = (deriv (fun (w : ℂ) => Complex.exp (J w)) z * B z - deriv B z * Complex.exp (J z)) / B z ^ 2

Lemma: Derivative of H(z) using quotient rule.

theorem exp_I_derivative_chain_rule {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → deriv (fun (w : ℂ) => Complex.exp (J w)) z = deriv J z * Complex.exp (J z)

theorem H_derivative_calc {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → deriv (H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J) z = (deriv J z * B z - deriv B z) * Complex.exp (J z) / B z ^ 2

theorem H_derivative_is_zero {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → deriv (H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J) z = 0

theorem zero_mem_closedBall_zero_radius {r1 : ℝ} (hr1 : 0 ≤ r1) : 0 ∈ Metric.closedBall 0 r1

theorem H_deriv_zero_on_closedBall {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → deriv (H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J) z = 0

theorem H_auxiliary_differentiableOn_closedBall {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) : DifferentiableOn ℂ (H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J) (Metric.closedBall 0 r1)

theorem hasDerivAt_H_auxiliary_zero_on_closedBall {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → HasDerivAt (H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J) 0 z

theorem fderivWithin_eq_zero_of_derivWithin_eq_zero {s : Set ℂ} {f : ℂ → ℂ} {x : ℂ} (hdiff : DifferentiableWithinAt ℂ f s x) (hderiv : derivWithin f s x = 0) : fderivWithin ℂ f s x = 0

theorem hasDerivWithinAt_of_hasDerivAt {f : ℂ → ℂ} {s : Set ℂ} {x : ℂ} (h : HasDerivAt f 0 x) : HasDerivWithinAt f 0 s x

theorem uniqueDiffWithinAt_closedBall (r1 : ℝ) {x : ℂ} (hr1 : 0 < r1) (hx : x ∈ Metric.closedBall 0 r1) : UniqueDiffWithinAt ℝ (Metric.closedBall 0 r1) x

theorem H_auxiliary_fderivWithin_zero_on_closedBall {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → fderivWithin ℂ (H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J) (Metric.closedBall 0 r1) z = 0

theorem H_is_constant {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J z = H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J 0

Lemma: H is constant on the closed ball.

theorem H_is_one {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → H_auxiliary hr1_pos hr1_lt_R' hR'_lt_R hR_lt_one hB hB_ne_zero J z = 1 / B 0

theorem analytic_log_exists {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → B z = B 0 * Complex.exp (J z)

Lemma: B(z) = B(0) * exp(J(z)).

theorem modulus_of_exp_I {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → ‖Complex.exp (J z)‖ = Real.exp (J z).re

theorem modulus_of_B_product_form {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → ‖B z‖ = ‖B 0‖ * ‖Complex.exp (J z)‖

Lemma: |B(z)| = |B(0)| * |exp(J(z))|.

theorem modulus_of_exp_log {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → ‖B z‖ = ‖B 0‖ * Real.exp (J z).re

Lemma: |B(z)| = |B(0)| * exp(Re(J(z))).

theorem log_modulus_as_sum {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → Real.log ‖B z‖ = Real.log ‖B 0‖ + Real.log (Real.exp (J z).re)

Lemma: log|B(z)| = log|B(0)| + log(exp(Re(J(z)))).

theorem real_log_of_modulus_difference {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) {J : ℂ → ℂ} (hJ : AnalyticOnNhd ℂ J (Metric.closedBall 0 r1)) (hJ_zero : J 0 = 0) (hJ_deriv : ∀ z ∈ Metric.closedBall 0 r1, deriv J z = deriv B z / B z) (z : ℂ) : z ∈ Metric.closedBall 0 r1 → Real.log ‖B z‖ - Real.log ‖B 0‖ = (J z).re

Lemma: log|B(z)| - log|B(0)| = Re(J(z)).

theorem log_of_analytic {r1 R' R : ℝ} (hr1_pos : 0 < r1) (hr1_lt_R' : r1 < R') (hR'_lt_R : R' < R) (hR_lt_one : R < 1) {B : ℂ → ℂ} (hB : AnalyticOnNhd ℂ B (Metric.closedBall 0 R)) (hB_ne_zero : ∀ z ∈ Metric.closedBall 0 R', B z ≠ 0) : ∃ (J_B : ℂ → ℂ), AnalyticOnNhd ℂ J_B (Metric.closedBall 0 r1) ∧ J_B 0 = 0 ∧ (∀ z ∈ Metric.closedBall 0 r1, deriv J_B z = deriv B z / B z) ∧ ∀ z ∈ Metric.closedBall 0 r1, Real.log ‖B z‖ - Real.log ‖B 0‖ = (J_B z).re