Theorem: dist_prod_one_le_abs_sum (Ray/Misc/Bounds.lean)

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)
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

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
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

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
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

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
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

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)]
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

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]
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

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)
State after:
no goals

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
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

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
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)

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
State after:
no goals

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
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

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
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

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
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

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
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

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]
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)

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
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

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
State after:
no goals

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 _ _) ?_
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

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))) ?_
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

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]
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

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
State after:
no goals

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]
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

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
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

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
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

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)]
State after:
no goals

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
State after:
no goals

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
State after:
no goals