internlm/Lean-Github huggingface dataset:
Theorem: differentiable_iff_analytic2
Proof state before:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : z1 ∈ ball z1✝ r
⊢ (fun z1 => (z0, z1)) z1 ∈ ball (z0, z1✝) r
Tactic:
simp at z1s ⊢
Proof state after:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : dist z1 z1✝ < r
⊢ dist z1 z1✝ < r
Theorem: differentiable_iff_analytic2
Proof state before:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : dist z1 z1✝ < r
⊢ dist z1 z1✝ < r
Tactic:
assumption
Proof state after:
no goals
Theorem: differentiable_iff_analytic2
Proof state before:
case mpr
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ AnalyticOn ℂ f s → DifferentiableOn ℂ f s
Tactic:
exact fun a ↦ a.differentiableOn
Proof state after:
no goals
Theorem: contDiffAt_iff_analytic_at2
Proof state before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ ContDiffAt ℂ n f x ↔ AnalyticAt ℂ f x
Tactic:
constructor
Proof state after:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ ContDiffAt ℂ n f x → AnalyticAt ℂ f x

case mpr
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ AnalyticAt ℂ f x → ContDiffAt ℂ n f x
Theorem: contDiffAt_iff_analytic_at2
Proof state before:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ ContDiffAt ℂ n f x → AnalyticAt ℂ f x
Tactic:
intro d
Proof state after:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d : ContDiffAt ℂ n f x
⊢ AnalyticAt ℂ f x
Theorem: contDiffAt_iff_analytic_at2
Proof state before:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d : ContDiffAt ℂ n f x
⊢ AnalyticAt ℂ f x
Tactic:
rcases d.contDiffOn n1 with ⟨u, un, d⟩
Proof state after:
case mp.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
⊢ AnalyticAt ℂ f x
Theorem: contDiffAt_iff_analytic_at2
Proof state before:
case mp.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
⊢ AnalyticAt ℂ f x
Tactic:
rcases mem_nhds_iff.mp un with ⟨v, uv, vo, vx⟩
Proof state after:
case mp.intro.intro.intro.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ AnalyticAt ℂ f x
Theorem: contDiffAt_iff_analytic_at2
Proof state before:
case mp.intro.intro.intro.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ AnalyticAt ℂ f x
Tactic:
refine (differentiable_iff_analytic2 vo).mp ?_ _ vx
Proof state after:
case mp.intro.intro.intro.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ DifferentiableOn ℂ f v
Theorem: contDiffAt_iff_analytic_at2
Proof state before:
case mp.intro.intro.intro.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ DifferentiableOn ℂ f v
Tactic:
exact (d.mono uv).differentiableOn (by norm_num)
Proof state after:
no goals
Theorem: contDiffAt_iff_analytic_at2
Proof state before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
d✝ : ContDiffAt ℂ n f x
u : Set (ℂ × ℂ)
un : u ∈ 𝓝 x
d : ContDiffOn ℂ (↑One.one) f u
v : Set (ℂ × ℂ)
uv : v ⊆ u
vo : IsOpen v
vx : x ∈ v
⊢ 1 ≤ ↑One.one
Tactic:
norm_num
Proof state after:
no goals
Theorem: contDiffAt_iff_analytic_at2
Proof state before:
case mpr
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
⊢ AnalyticAt ℂ f x → ContDiffAt ℂ n f x
Tactic:
intro a
Proof state after:
case mpr
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
a : AnalyticAt ℂ f x
⊢ ContDiffAt ℂ n f x
Theorem: contDiffAt_iff_analytic_at2
Proof state before:
case mpr
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
x : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℕ∞
n1 : 1 ≤ n
a : AnalyticAt ℂ f x
⊢ ContDiffAt ℂ n f x
Tactic:
exact a.contDiffAt.of_le le_top
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have m1 : ∀ t : ℝ, t ≤ 1 → t * abs z < 1 :=
  fun _ m ↦ Right.mul_lt_one_of_le_of_lt_of_nonneg m z1 (Complex.abs.nonneg _)
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have dr : ∀ t : ℝ, t ∈ uIcc 0 1 →
    HasDerivAt (fun t : ℝ ↦ -Real.log (1 - t * abs z)) (- (-abs z / (1 - t * abs z))) t := by
  intro t m
  simp only [ge_iff_le, zero_le_one, uIcc_of_le, mem_Icc] at m
  exact (((hasDerivAt_mul_const _).const_sub _).log ((sub_pos.mpr (m1 _ m.2)).ne')).neg
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have ic : IntervalIntegrable (fun t ↦ z / (1 + t*z)) MeasureTheory.volume 0 1 := by
  apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
  apply continuousOn_const.div (Continuous.continuousOn (by continuity))
  intro t ⟨t0,t1⟩
  rw [←Complex.abs.ne_zero_iff]
  apply ne_of_gt
  calc abs (1 + t*z)
    _ ≥ Complex.abs 1 - abs (t*z) := Complex.abs.le_add _ _
    _ = 1 - |t| * abs z := by simp only [map_one, map_mul, Complex.abs_ofReal]
    _ > 0 := by refine sub_pos.mpr (m1 _ (abs_le.mpr ⟨by linarith, t1⟩))
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
simp only [neg_div, neg_neg] at dr
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have ir : IntervalIntegrable (fun t ↦ abs z / (1 - t * abs z)) MeasureTheory.volume 0 1 := by
  apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
  apply continuousOn_const.div (Continuous.continuousOn (by continuity))
  intro t ⟨_,t1⟩; exact ne_of_gt (sub_pos.mpr (m1 _ t1))
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have fc := intervalIntegral.integral_eq_sub_of_hasDerivAt dc ic
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + ↑1 * z).log - (1 + ↑0 * z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + ↑1 * z).log - (1 + ↑0 * z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have fr := intervalIntegral.integral_eq_sub_of_hasDerivAt dr ir
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + ↑1 * z).log - (1 + ↑0 * z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - 1 * abs z).log - -(1 - 0 * abs z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + ↑1 * z).log - (1 + ↑0 * z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - 1 * abs z).log - -(1 - 0 * abs z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
simp only [Complex.ofReal_one, one_mul, Complex.ofReal_zero, zero_mul, add_zero, Complex.log_one,
  sub_zero, Real.log_one, neg_zero] at fc fr
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - abs z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - abs z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
rw [←fc, ←fr, ←Complex.norm_eq_abs]
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - abs z).log
⊢ ‖∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - abs z).log
⊢ ‖∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)
Tactic:
clear dc dr fc fr
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ‖∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ‖∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)
Tactic:
apply le_trans (intervalIntegral.norm_integral_le_integral_norm zero_le_one) ?_
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ∫ (x : ℝ) in 0 ..1, ‖z / (1 + ↑x * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ∫ (x : ℝ) in 0 ..1, ‖z / (1 + ↑x * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)
Tactic:
apply intervalIntegral.integral_mono_on zero_le_one ic.norm ir
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ∀ x ∈ Icc 0 1, ‖z / (1 + ↑x * z)‖ ≤ abs z / (1 - x * abs z)
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ∀ x ∈ Icc 0 1, ‖z / (1 + ↑x * z)‖ ≤ abs z / (1 - x * abs z)
Tactic:
intro t ⟨t0,t1⟩
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ ‖z / (1 + ↑t * z)‖ ≤ abs z / (1 - t * abs z)
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ ‖z / (1 + ↑t * z)‖ ≤ abs z / (1 - t * abs z)
Tactic:
simp only [norm_div, Complex.norm_eq_abs]
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ abs z / abs (1 + ↑t * z) ≤ abs z / (1 - t * abs z)
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ abs z / abs (1 + ↑t * z) ≤ abs z / (1 - t * abs z)
Tactic:
apply div_le_div_of_nonneg_left (Complex.abs.nonneg _) (sub_pos.mpr (m1 _ t1)) ?_
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ 1 - t * abs z ≤ abs (1 + ↑t * z)
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ 1 - t * abs z ≤ abs (1 + ↑t * z)
Tactic:
calc abs (1 + t * z)
  _ ≥ Complex.abs 1 - abs (t * z) := Complex.abs.le_add _ _
  _ = 1 - t * abs z := by
    simp only [map_one, map_mul, Complex.abs_ofReal, _root_.abs_of_nonneg t0]
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
⊢ ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
Tactic:
intro t m
Proof state after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t