internlm/Lean-Github huggingface dataset:
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < max 16 (Complex.abs c / 2) ^ d

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)
Tactic:
bound
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)
Tactic:
rw [mul_one_div]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d / 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d / 8
Tactic:
rw [le_div_iff, mul_comm]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < 8
Tactic:
swap
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < 8

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < 8

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d
Tactic:
norm_num
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d
Tactic:
refine le_trans ?_ (pow_le_pow_right (le_max_of_le_left (by norm_num)) (two_le_d d))
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Tactic:
by_cases cb : abs c / 2 ≤ 16
Proof state after:
case pos
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2

case neg
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Theorem: superNearF
Proof state before:
case pos
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2

case neg
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Tactic:
rw [max_eq_left cb, pow_two]
Proof state after:
case pos
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ 16 * 16

case neg
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Theorem: superNearF
Proof state before:
case pos
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ 16 * 16

case neg
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Tactic:
linarith
Proof state after:
case neg
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Theorem: superNearF
Proof state before:
case neg
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ 2
Tactic:
rw [max_eq_right (not_le.mp cb).le, pow_two]
Proof state after:
case neg
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ Complex.abs c / 2 * (Complex.abs c / 2)
Theorem: superNearF
Proof state before:
case neg
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
cb : ¬Complex.abs c / 2 ≤ 16
⊢ 8 * Complex.abs c ≤ Complex.abs c / 2 * (Complex.abs c / 2)
Tactic:
nlinarith
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 1 ≤ 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
⊢ ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
Tactic:
intro z m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
Tactic:
calc abs (1 + c * z ^ d)
  _ ≥ Complex.abs 1 - abs (c * z ^ d) := by bound
  _ ≥ Complex.abs 1 - 1 / 8 := by linarith [cz m]
  _ = 7 / 8 := by norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ Complex.abs (1 + c * z ^ d) ≥ Complex.abs 1 - Complex.abs (c * z ^ d)
Tactic:
bound
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ Complex.abs 1 - Complex.abs (c * z ^ d) ≥ Complex.abs 1 - 1 / 8
Tactic:
linarith [cz m]
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ Complex.abs 1 - 1 / 8 = 7 / 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
⊢ ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
Tactic:
intro z m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ t
⊢ Complex.abs z ≤ 1 / 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ t
⊢ Complex.abs z ≤ 1 / 8
Tactic:
rw [← ht] at m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ Complex.abs z ≤ 1 / 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ Complex.abs z ≤ 1 / 8
Tactic:
refine le_trans (le_of_lt m) ?_
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ (max 16 (Complex.abs c / 2))⁻¹ ≤ 1 / 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ (max 16 (Complex.abs c / 2))⁻¹ ≤ 1 / 8
Tactic:
rw [one_div]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ (max 16 (Complex.abs c / 2))⁻¹ ≤ 8⁻¹
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ (max 16 (Complex.abs c / 2))⁻¹ ≤ 8⁻¹
Tactic:
exact inv_le_inv_of_le (by norm_num) (le_trans (by norm_num) (le_max_left _ _))
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ 0 < 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
z : ℂ
m : z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ 8 ≤ 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ IsOpen t
Tactic:
rw [← ht]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ IsOpen {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ IsOpen {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
exact isOpen_lt Complex.continuous_abs continuous_const
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ 0 ∈ t
Tactic:
simp only [← ht, mem_setOf, Complex.abs.map_zero]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ 0 < (max 16 (Complex.abs c / 2))⁻¹
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ 0 < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ 1 / 8 ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ AnalyticOn ℂ (fl (f d) ∞ c) t
Tactic:
intro z m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ AnalyticAt ℂ (fl (f d) ∞ c) z
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ AnalyticAt ℂ (fl (f d) ∞ c) z
Tactic:
rw [fl_f]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ AnalyticAt ℂ ((fun c z => z ^ d / (1 + c * z ^ d)) c) z
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ AnalyticAt ℂ ((fun c z => z ^ d / (1 + c * z ^ d)) c) z
Tactic:
refine ((analyticAt_id _ _).pow _).div (analyticAt_const.add
  (analyticAt_const.mul ((analyticAt_id _ _).pow _))) ?_
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ 1 + c * z ^ d ≠ 0
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ 1 + c * z ^ d ≠ 0
Tactic:
rw [← Complex.abs.ne_zero_iff]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ Complex.abs (1 + c * z ^ d) ≠ 0
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
z : ℂ
m : z ∈ t
⊢ Complex.abs (1 + c * z ^ d) ≠ 0
Tactic:
exact (lt_of_lt_of_le (by norm_num) (cz1 m)).ne'
Proof state after:
no goals