internlm/Lean-Github huggingface dataset:
Theorem: pow_small
Proof state before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs ((1 + z1) ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w
Tactic:
refine pow1p_small ?_ ws
Proof state after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs z1 ≤ 1 / 2
Theorem: pow_small
Proof state before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs z1 ≤ 1 / 2
Tactic:
rw [← zw]
Proof state after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z - 1) ≤ 1 / 2
Theorem: pow_small
Proof state before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z - 1) ≤ 1 / 2
Tactic:
assumption
Proof state after:
no goals
Theorem: pow_small
Proof state before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ z = 1 + z1
Tactic:
rw [← zw]
Proof state after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ z = 1 + (z - 1)
Theorem: pow_small
Proof state before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ z = 1 + (z - 1)
Tactic:
ring
Proof state after:
no goals
Theorem: add_ne_zero_of_abs_lt
Proof state before:
a b : ℂ
h : Complex.abs b < Complex.abs a
⊢ a + b ≠ 0
Tactic:
have e : a + b = a - -b := by abel
Proof state after:
a b : ℂ
h : Complex.abs b < Complex.abs a
e : a + b = a - -b
⊢ a + b ≠ 0
Theorem: add_ne_zero_of_abs_lt
Proof state before:
a b : ℂ
h : Complex.abs b < Complex.abs a
e : a + b = a - -b
⊢ a + b ≠ 0
Tactic:
rw [e, sub_ne_zero]
Proof state after:
a b : ℂ
h : Complex.abs b < Complex.abs a
e : a + b = a - -b
⊢ a ≠ -b
Theorem: add_ne_zero_of_abs_lt
Proof state before:
a b : ℂ
h : Complex.abs b < Complex.abs a
e : a + b = a - -b
⊢ a ≠ -b
Tactic:
contrapose h
Proof state after:
a b : ℂ
e : a + b = a - -b
h : ¬a ≠ -b
⊢ ¬Complex.abs b < Complex.abs a
Theorem: add_ne_zero_of_abs_lt
Proof state before:
a b : ℂ
e : a + b = a - -b
h : ¬a ≠ -b
⊢ ¬Complex.abs b < Complex.abs a
Tactic:
simp only [not_not] at h
Proof state after:
a b : ℂ
e : a + b = a - -b
h : a = -b
⊢ ¬Complex.abs b < Complex.abs a
Theorem: add_ne_zero_of_abs_lt
Proof state before:
a b : ℂ
e : a + b = a - -b
h : a = -b
⊢ ¬Complex.abs b < Complex.abs a
Tactic:
simp only [h, not_lt, AbsoluteValue.map_neg, le_refl]
Proof state after:
no goals
Theorem: add_ne_zero_of_abs_lt
Proof state before:
a b : ℂ
h : Complex.abs b < Complex.abs a
⊢ a + b = a - -b
Tactic:
abel
Proof state after:
no goals
Theorem: Real.exp_one_lt_3
Proof state before:
⊢ 2.7182818286 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: log_add
Proof state before:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
⊢ (a + b).log = a.log + (1 + b / a).log
Tactic:
have d0 : 0 < 1 + b/a := by field_simp [a0.ne']; bound
Proof state after:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
d0 : 0 < 1 + b / a
⊢ (a + b).log = a.log + (1 + b / a).log
Theorem: log_add
Proof state before:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
d0 : 0 < 1 + b / a
⊢ (a + b).log = a.log + (1 + b / a).log
Tactic:
rw [←Real.log_mul a0.ne' d0.ne', left_distrib, mul_one, mul_div_cancel₀ _ a0.ne']
Proof state after:
no goals
Theorem: log_add
Proof state before:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
⊢ 0 < 1 + b / a
Tactic:
field_simp [a0.ne']
Proof state after:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
⊢ 0 < a
Theorem: log_add
Proof state before:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
⊢ 0 < a
Tactic:
bound
Proof state after:
no goals
Theorem: log_abs_add
Proof state before:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Tactic:
have d0 : 1 + b/a ≠ 0 := by field_simp [a0, ab0]
Proof state after:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Theorem: log_abs_add
Proof state before:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Tactic:
have a0' : abs a ≠ 0 := Complex.abs.ne_zero a0
Proof state after:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
a0' : Complex.abs a ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Theorem: log_abs_add
Proof state before:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
a0' : Complex.abs a ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Tactic:
have d0' : abs (1 + b / a) ≠ 0 := Complex.abs.ne_zero d0
Proof state after:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
a0' : Complex.abs a ≠ 0
d0' : Complex.abs (1 + b / a) ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Theorem: log_abs_add
Proof state before:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
a0' : Complex.abs a ≠ 0
d0' : Complex.abs (1 + b / a) ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Tactic:
rw [←Real.log_mul a0' d0', ←Complex.abs.map_mul, left_distrib, mul_one, mul_div_cancel₀ _ a0]
Proof state after:
no goals
Theorem: log_abs_add
Proof state before:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
⊢ 1 + b / a ≠ 0
Tactic:
field_simp [a0, ab0]
Proof state after:
no goals
Theorem: Real.exp_forth_lt_four_thirds
Proof state before:
⊢ (1 / 4).exp < 4 / 3
Tactic:
rw [←Real.exp_one_rpow, one_div, ←@Real.pow_rpow_inv_natCast (4/3) 4 (by norm_num) (by norm_num)]
Proof state after:
⊢ rexp 1 ^ 4⁻¹ < ((4 / 3) ^ 4) ^ (↑4)⁻¹
Theorem: Real.exp_forth_lt_four_thirds
Proof state before:
⊢ rexp 1 ^ 4⁻¹ < ((4 / 3) ^ 4) ^ (↑4)⁻¹
Tactic:
refine Real.rpow_lt_rpow (Real.exp_pos _).le ?_ (by norm_num)
Proof state after:
⊢ rexp 1 < (4 / 3) ^ 4
Theorem: Real.exp_forth_lt_four_thirds
Proof state before:
⊢ rexp 1 < (4 / 3) ^ 4
Tactic:
exact _root_.trans Real.exp_one_lt_d9 (by norm_num)
Proof state after:
no goals
Theorem: Real.exp_forth_lt_four_thirds
Proof state before:
⊢ 0 ≤ 4 / 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: Real.exp_forth_lt_four_thirds
Proof state before:
⊢ 4 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Real.exp_forth_lt_four_thirds
Proof state before:
⊢ 0 < 4⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: Real.exp_forth_lt_four_thirds
Proof state before:
⊢ 2.7182818286 < (4 / 3) ^ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Tactic:
set g := fun n ↦ Complex.log (f n)
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Tactic:
have b : ∀ n, n ∈ s → abs (f n - 1) ≤ c := by
  intro n m; refine _root_.trans ?_ le
  exact Finset.single_le_sum (f := fun n ↦ abs (f n - 1)) (fun _ _ ↦ Complex.abs.nonneg _) m
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Tactic:
have f0 : ∀ n, n ∈ s → f n ≠ 0 := by
  intro n m; specialize b n m; contrapose b; simp only [not_not] at b
  simp only [b, not_le]; norm_num; linarith
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Tactic:
have sg : abs (s.sum g) ≤ 2 * c := by
  refine _root_.trans (Complex.abs.sum_le _ _) ?_
  refine _root_.trans (Finset.sum_le_sum (fun n m ↦ log_small (_root_.trans (b n m) c1))) ?_
  rw [← Finset.mul_sum]; bound
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Tactic:
have e : s.prod f = Complex.exp (s.sum g) := by
  rw [Complex.exp_sum]; apply Finset.prod_congr rfl
  intro n m; rw [Complex.exp_log (f0 n m)]
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
e : s.prod f = (s.sum g).exp
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
e : s.prod f = (s.sum g).exp
⊢ Complex.abs (s.prod f - 1) ≤ 4 * c
Tactic:
rw [e]
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
e : s.prod f = (s.sum g).exp
⊢ Complex.abs ((s.sum g).exp - 1) ≤ 4 * c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
e : s.prod f = (s.sum g).exp
⊢ Complex.abs ((s.sum g).exp - 1) ≤ 4 * c
Tactic:
exact _root_.trans (exp_small (by linarith)) (by linarith)
Proof state after:
no goals
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
⊢ ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
Tactic:
intro n m
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
⊢ Complex.abs (f n - 1) ≤ c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
⊢ Complex.abs (f n - 1) ≤ c
Tactic:
refine _root_.trans ?_ le
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
⊢ Complex.abs (f n - 1) ≤ s.sum fun n => Complex.abs (f n - 1)
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
⊢ Complex.abs (f n - 1) ≤ s.sum fun n => Complex.abs (f n - 1)
Tactic:
exact Finset.single_le_sum (f := fun n ↦ abs (f n - 1)) (fun _ _ ↦ Complex.abs.nonneg _) m
Proof state after:
no goals
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
⊢ ∀ n ∈ s, f n ≠ 0
Tactic:
intro n m
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
n : ℕ
m : n ∈ s
⊢ f n ≠ 0
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
n : ℕ
m : n ∈ s
⊢ f n ≠ 0
Tactic:
specialize b n m
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : Complex.abs (f n - 1) ≤ c
⊢ f n ≠ 0
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : Complex.abs (f n - 1) ≤ c
⊢ f n ≠ 0
Tactic:
contrapose b
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : ¬f n ≠ 0
⊢ ¬Complex.abs (f n - 1) ≤ c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : ¬f n ≠ 0
⊢ ¬Complex.abs (f n - 1) ≤ c
Tactic:
simp only [not_not] at b
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : f n = 0
⊢ ¬Complex.abs (f n - 1) ≤ c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : f n = 0
⊢ ¬Complex.abs (f n - 1) ≤ c
Tactic:
simp only [b, not_le]
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : f n = 0
⊢ c < Complex.abs (0 - 1)
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : f n = 0
⊢ c < Complex.abs (0 - 1)
Tactic:
norm_num
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : f n = 0
⊢ c < 1
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
n : ℕ
m : n ∈ s
b : f n = 0
⊢ c < 1
Tactic:
linarith
Proof state after:
no goals
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
⊢ Complex.abs (s.sum g) ≤ 2 * c
Tactic:
refine _root_.trans (Complex.abs.sum_le _ _) ?_
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
⊢ (s.sum fun i => Complex.abs (f i).log) ≤ 2 * c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
⊢ (s.sum fun i => Complex.abs (f i).log) ≤ 2 * c
Tactic:
refine _root_.trans (Finset.sum_le_sum (fun n m ↦ log_small (_root_.trans (b n m) c1))) ?_
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
⊢ (s.sum fun i => 2 * Complex.abs (f i - 1)) ≤ 2 * c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
⊢ (s.sum fun i => 2 * Complex.abs (f i - 1)) ≤ 2 * c
Tactic:
rw [← Finset.mul_sum]
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
⊢ (2 * s.sum fun i => Complex.abs (f i - 1)) ≤ 2 * c
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
⊢ (2 * s.sum fun i => Complex.abs (f i - 1)) ≤ 2 * c
Tactic:
bound
Proof state after:
no goals
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
⊢ s.prod f = (s.sum g).exp
Tactic:
rw [Complex.exp_sum]
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
⊢ s.prod f = s.prod fun x => (f x).log.exp
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
⊢ s.prod f = s.prod fun x => (f x).log.exp
Tactic:
apply Finset.prod_congr rfl
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
⊢ ∀ x ∈ s, f x = (f x).log.exp
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
⊢ ∀ x ∈ s, f x = (f x).log.exp
Tactic:
intro n m
Proof state after:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
n : ℕ
m : n ∈ s
⊢ f n = (f n).log.exp
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
n : ℕ
m : n ∈ s
⊢ f n = (f n).log.exp
Tactic:
rw [Complex.exp_log (f0 n m)]
Proof state after:
no goals
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
e : s.prod f = (s.sum g).exp
⊢ Complex.abs (s.sum g) ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: dist_prod_one_le_abs_sum
Proof state before:
f : ℕ → ℂ
s : Finset ℕ
c : ℝ
le : (s.sum fun n => Complex.abs (f n - 1)) ≤ c
c1 : c ≤ 1 / 2
g : ℕ → ℂ := fun n => (f n).log
b : ∀ n ∈ s, Complex.abs (f n - 1) ≤ c
f0 : ∀ n ∈ s, f n ≠ 0
sg : Complex.abs (s.sum g) ≤ 2 * c
e : s.prod f = (s.sum g).exp
⊢ 2 * Complex.abs (s.sum g) ≤ 4 * c
Tactic:
linarith
Proof state after:
no goals
Theorem: ChartedSpace.t1Space
Proof state before:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
⊢ ∀ (x : M), IsClosed {x}
Tactic:
intro x
Proof state after:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsClosed {x}
Theorem: ChartedSpace.t1Space
Proof state before:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsClosed {x}
Tactic:
rw [←compl_compl ({x} : Set M)]
Proof state after:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsClosed {x}ᶜᶜ
Theorem: ChartedSpace.t1Space
Proof state before:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsClosed {x}ᶜᶜ
Tactic:
apply IsOpen.isClosed_compl
Proof state after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsOpen {x}ᶜ
Theorem: ChartedSpace.t1Space
Proof state before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsOpen {x}ᶜ
Tactic:
rw [isOpen_iff_mem_nhds]
Proof state after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ ∀ x_1 ∈ {x}ᶜ, {x}ᶜ ∈ 𝓝 x_1
Theorem: ChartedSpace.t1Space
Proof state before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ ∀ x_1 ∈ {x}ᶜ, {x}ᶜ ∈ 𝓝 x_1
Tactic:
intro y m
Proof state after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ∈ {x}ᶜ
⊢ {x}ᶜ ∈ 𝓝 y
Theorem: ChartedSpace.t1Space
Proof state before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ∈ {x}ᶜ
⊢ {x}ᶜ ∈ 𝓝 y
Tactic:
simp only [mem_compl_singleton_iff] at m
Proof state after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
⊢ {x}ᶜ ∈ 𝓝 y
Theorem: ChartedSpace.t1Space
Proof state before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
⊢ {x}ᶜ ∈ 𝓝 y
Tactic:
simp only [mem_nhds_iff, subset_compl_singleton_iff]
Proof state after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Theorem: ChartedSpace.t1Space
Proof state before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
by_cases xm : x ∈ (chartAt A y).source
Proof state after:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t

case neg
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∉ (_root_.chartAt A y).source
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Theorem: ChartedSpace.t1Space
Proof state before:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
set t := (chartAt A y).source \ {x}
Proof state after:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t