awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20)
have h : |rexp 1 -
      expNear 21 1
        ((((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                                  7 -
                                                                1) *
                                                              8 -
                                                            1) *
                                                          9 -
                                                        1) *
                                                      10 -
                                                    1) *
                                                  11 -
                                                1) *
                                              12 -
                                            1) *
                                          13 -
                                        1) *
                                      14 -
                                    1) *
                                  15 -
                                1) *
                              16 -
                            1) *
                          17 -
                        1) *
                      18 -
                    1) *
                  19 -
                1) *
              20 -
            1) *
          21)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 21 / (↑(Nat.factorial 21) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 *
            18 *
          19 *
        20 *
      21)
Tactic: iterate 21 refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑22 : ℝ) 22
have norm_cast : Eq (α := ℝ) 22 22
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ round (rexp 1) = 3
have refine : (↑3 : ℝ) ≤ rexp 1 + 1 / 2
Tactic: refine round_eq _ |>.trans <| Int.floor_eq_iff.mpr ⟨?_, by grind [exp_one_lt_three]⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ (↑3 : ℝ) ≤ rexp 1 + 1 / 2
have grw : (↑3 : ℝ) ≤ 2.7182818283 + 1 / 2
Tactic: grw [← exp_one_gt_d9]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ 0.36787944116 < rexp (-1)
have rw : rexp 1 < 0.36787944116⁻¹
Tactic: rw [exp_neg, lt_inv_comm₀ _ (exp_pos _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
rw : rexp 1 < 0.36787944116⁻¹
⊢ 0.36787944116 < rexp (-1)
have rw₁ : LT.lt (α := ℝ) 0 0.36787944116
Tactic: rw [exp_neg, lt_inv_comm₀ _ (exp_pos _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ rexp 1 < 0.36787944116⁻¹
have refine : 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 + 2244083 / 825552 < 0.36787944116⁻¹
Tactic: refine lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ rexp (-1) < 0.3678794412
have rw : 0.3678794412⁻¹ < rexp 1
Tactic: rw [exp_neg, inv_lt_comm₀ (exp_pos _) (by norm_num)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
this :
  |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
⊢ |log 2 - 287209 / 414355| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10
have norm_num1 : ∀ (this : |log 2 - 287209 / 414355| ≤ 1 / 10000000000), |log 2 - 287209 / 414355| ≤ 1 / 10000000000
Tactic: norm_num1 at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |log 2 - 287209 / 414355| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10
have suffices : |log 2 - 287209 / 414355| ≤
  1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
Tactic: suffices |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34) by
    norm_num1 at *
    assumption
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) |2⁻¹| 2⁻¹
have rw : LT.lt (α := ℝ) 0 2⁻¹
Tactic: rw [abs_of_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
⊢ |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
have t : Eq (α := ℝ) |2⁻¹| 2⁻¹
Tactic: have t : |(2⁻¹ : ℝ)| = 2⁻¹ := by rw [abs_of_pos]; norm_num
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ LT.lt (α := ℝ) |2⁻¹| 1
have rw : LT.lt (α := ℝ) 2⁻¹ 1
Tactic: rw [t]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
have z : |∑ i ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (HSub.hSub (α := ℝ) 1 2⁻¹)| ≤
  HPow.hPow (α := ℝ) |2⁻¹| (HAdd.hAdd (α := ℕ) 34 1) / HSub.hSub (α := ℝ) 1 |2⁻¹|
Tactic: have z := Real.abs_log_sub_add_sum_range_le (show |(2⁻¹ : ℝ)| < 1 by rw [t]; norm_num) 34
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
z :
  |∑ i ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (HSub.hSub (α := ℝ) 1 2⁻¹)| ≤
    HPow.hPow (α := ℝ) |2⁻¹| (HAdd.hAdd (α := ℕ) 34 1) / HSub.hSub (α := ℝ) 1 |2⁻¹|
⊢ |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
have z₁ : |∑ i ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (HSub.hSub (α := ℝ) 1 2⁻¹)| ≤
  HPow.hPow (α := ℝ) 2⁻¹ (HAdd.hAdd (α := ℕ) 34 1) / HSub.hSub (α := ℝ) 1 2⁻¹
Tactic: rw [t] at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
z :
  |∑ i ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (HSub.hSub (α := ℝ) 1 2⁻¹)| ≤
    HPow.hPow (α := ℝ) 2⁻¹ (HAdd.hAdd (α := ℕ) 34 1) / HSub.hSub (α := ℝ) 1 2⁻¹
⊢ |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
have z₁ : |∑ x ∈ range 34, (1 / 2) ^ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + log (1 / 2)| ≤ 1 / 17179869184
Tactic: norm_num1 at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
z : |∑ x ∈ range 34, (1 / 2) ^ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + log (1 / 2)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
have z₁ : |log 2 - ∑ x ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1| ≤ 1 / 17179869184
Tactic: rw [one_div (2 : ℝ), log_inv, ← sub_eq_add_neg, _root_.abs_sub_comm] at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
z : |log 2 - ∑ x ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
have apply : |∑ x ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 - 287209 / 414355| ≤
  1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34
Tactic: apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
this :
  |log 3 - 109861228867 / 100000000000| ≤
    HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹)
⊢ |log 3 - 109861228867 / 100000000000| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10
have norm_num1 : ∀ (this : |log 3 - 109861228867 / 100000000000| ≤ 1 / 10000000000),
  |log 3 - 109861228867 / 100000000000| ≤ 1 / 10000000000
Tactic: norm_num1 at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |log 3 - 109861228867 / 100000000000| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10
have suffices : |log 3 - 109861228867 / 100000000000| ≤
  HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹)
Tactic: suffices |log 3 - 109861228867 / 100000000000| ≤
      (2 / 3) ^ 71 / 3⁻¹ + (1 / 10 ^ 10 - (2 / 3) ^ 71 / 3⁻¹) by
    norm_num1 at *
    assumption
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
⊢ |log 3 - 109861228867 / 100000000000| ≤
    HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹)
have t : |2 / 3| = 2 / 3
Tactic: have t : |2 / 3| = (2 : ℝ) / 3 := by norm_num
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
t : |2 / 3| = 2 / 3
⊢ |log 3 - 109861228867 / 100000000000| ≤
    HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹)
have z : |∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 2 / 3)| ≤
  |2 / 3| ^ HAdd.hAdd (α := ℕ) 70 1 / (1 - |2 / 3|)
Tactic: have z := abs_log_sub_add_sum_range_le (x := 2 / 3) (by norm_num) 70
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
t : |2 / 3| = 2 / 3
z :
  |∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 2 / 3)| ≤
    |2 / 3| ^ HAdd.hAdd (α := ℕ) 70 1 / (1 - |2 / 3|)
⊢ |log 3 - 109861228867 / 100000000000| ≤
    HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹)
have z₁ : |log 3 - ∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤ (2 / 3) ^ HAdd.hAdd (α := ℕ) 70 1 / 3⁻¹
Tactic: rw [t, show (1 - (2 : ℝ) / 3) = (1 / 3 : ℝ) by norm_num, one_div (3 : ℝ), log_inv,
    ← sub_eq_add_neg, _root_.abs_sub_comm] at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
t : |2 / 3| = 2 / 3
z :
  |log 3 - ∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤ (2 / 3) ^ HAdd.hAdd (α := ℕ) 70 1 / 3⁻¹
⊢ |log 3 - 109861228867 / 100000000000| ≤
    HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹)
have apply : |∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 - 109861228867 / 100000000000| ≤
  1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹
Tactic: apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
this :
  |log 5 - 160943791243 / 100000000000| ≤
    HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹ +
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹)
⊢ |log 5 - 160943791243 / 100000000000| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10
have norm_num1 : ∀ (this : |log 5 - 160943791243 / 100000000000| ≤ 1 / 10000000000),
  |log 5 - 160943791243 / 100000000000| ≤ 1 / 10000000000
Tactic: norm_num1 at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |log 5 - 160943791243 / 100000000000| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10
have suffices : |log 5 - 160943791243 / 100000000000| ≤
  HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹)
Tactic: suffices |log 5 - 160943791243 / 100000000000| ≤
      (4 / 5) ^ 131 / 5⁻¹ + (1 / 10 ^ 10 - (4 / 5) ^ 131 / 5⁻¹) by
    norm_num1 at *
    assumption
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
⊢ |log 5 - 160943791243 / 100000000000| ≤
    HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹ +
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹)
have t : |4 / 5| = 4 / 5
Tactic: have t : |4 / 5| = (4 : ℝ) / 5 := by norm_num
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
t : |4 / 5| = 4 / 5
⊢ |log 5 - 160943791243 / 100000000000| ≤
    HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹ +
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹)
have z : |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 4 / 5)| ≤
  |4 / 5| ^ HAdd.hAdd (α := ℕ) 130 1 / (1 - |4 / 5|)
Tactic: have z := abs_log_sub_add_sum_range_le (x := 4 / 5) (by norm_num) 130
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (hypothesis)
Goal:
t : |4 / 5| = 4 / 5
z :
  |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 4 / 5)| ≤
    |4 / 5| ^ HAdd.hAdd (α := ℕ) 130 1 / (1 - |4 / 5|)
⊢ |log 5 - 160943791243 / 100000000000| ≤
    HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹ +
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹)
have z₁ : |log 5 - ∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤ (4 / 5) ^ HAdd.hAdd (α := ℕ) 130 1 / 5⁻¹
Tactic: rw [t, show (1 - (4 : ℝ) / 5) = (1 / 5 : ℝ) by norm_num, one_div (5 : ℝ), log_inv,
    ← sub_eq_add_neg, _root_.abs_sub_comm] at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
t : |4 / 5| = 4 / 5
z :
  |log 5 - ∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤
    (4 / 5) ^ HAdd.hAdd (α := ℕ) 130 1 / 5⁻¹
⊢ |log 5 - 160943791243 / 100000000000| ≤
    HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹ +
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹)
have apply : |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 - 160943791243 / 100000000000| ≤
  1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹
Tactic: apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
x : ℝ
⊢ 0 ≤ sSupNormIm f x
have hs : ∀ x_1 ∈ norm ∘ f '' re ⁻¹' {x}, 0 ≤ x_1
Tactic: apply Real.sSup_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
x : ℝ
⊢ 0 < ε + sSupNormIm f x
have linarith : ε + sSupNormIm f x ≤ 0 → 0 - ε + (ε + sSupNormIm f x - 0) + (0 - sSupNormIm f x) = 0
Tactic: linarith [sSupNormIm_nonneg f x]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖invInterpStrip f z ε‖ = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
have simp : ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
  (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
Tactic: simp only [invInterpStrip, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
have rw : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
  (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
Tactic: rw [← ofReal_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
have rw : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
  (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
Tactic: rw [← ofReal_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
have repeat : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
  (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
Tactic: repeat rw [← ofReal_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
have rw : (ε + sSupNormIm f 0) ^ (z - 1).re * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
  (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
Tactic: rw [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ (ε + sSupNormIm f 0) ^ (z - 1).re * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
have rw : (ε + sSupNormIm f 0) ^ (z - 1).re * (ε + sSupNormIm f 1) ^ (-z).re =
  (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
Tactic: rw [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
have repeat : (ε + sSupNormIm f 0) ^ (z - 1).re * (ε + sSupNormIm f 1) ^ (-z).re =
  (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
Tactic: repeat rw [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ invInterpStrip f z ε) (verticalStrip 0 1)
have h : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ invInterpStrip f z ε
Tactic: apply Differentiable.diffContOnCl
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ invInterpStrip f z ε
have h : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ ((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)
Tactic: apply Differentiable.mul
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
h : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ ((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ invInterpStrip f z ε
have h₁ : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)
Tactic: apply Differentiable.mul
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ ((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)
have apply : (↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ) ≠ 0 ∨ ∀ (x : ℂ), id x - 1 ≠ 0
Tactic: apply Differentiable.const_cpow (Differentiable.sub_const differentiable_id 1) _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ (↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ) ≠ 0 ∨ ∀ (x : ℂ), id x - 1 ≠ 0
have h : (↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ) ≠ 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ (↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ) ≠ 0
have h : ε + sSupNormIm f 0 ≠ 0
Tactic: rw [← ofReal_add, ofReal_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)
have h : (↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ) ≠ 0 ∨ ∀ (x : ℂ), Ne (α := ℂ) ((-id) x : ℂ) (0 : ℂ)
Tactic: apply Differentiable.const_cpow (Differentiable.neg differentiable_id)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ (↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ) ≠ 0 ∨ ∀ (x : ℂ), Ne (α := ℂ) ((-id) x : ℂ) (0 : ℂ)
have h : (↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ) ≠ 0
Tactic: apply Or.inl
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ (↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ) ≠ 0
have h : ε + sSupNormIm f 1 ≠ 0
Tactic: rw [← ofReal_add, ofReal_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ≤ sSupNormIm f z.re
have refine_1 : BddAbove (norm ∘ f '' re ⁻¹' {z.re})
Tactic: refine le_csSup ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
refine_1 : BddAbove (norm ∘ f '' re ⁻¹' {z.re})
⊢ ‖f z‖ ≤ sSupNormIm f z.re
have refine_2 : ‖f z‖ ∈ norm ∘ f '' re ⁻¹' {z.re}
Tactic: refine le_csSup ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ BddAbove (norm ∘ f '' re ⁻¹' {z.re})
have refine_1 : ∀ (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), BddAbove (norm ∘ f '' re ⁻¹' {z.re})
Tactic: revert hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
⊢ ∀ (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), BddAbove (norm ∘ f '' re ⁻¹' {z.re})
have refine_1 : re ⁻¹' {z.re} ⊆ verticalClosedStrip 0 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ∈ norm ∘ f '' re ⁻¹' {z.re}
have refine_2 : z ∈ re ⁻¹' {z.re}
Tactic: apply mem_image_of_mem (norm ∘ f)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ BddAbove (norm ∘ F f ε '' verticalClosedStrip 0 1)
have simp : BddAbove (α := ℝ)
  ((fun (a : ℂ) ↦
      ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
    verticalClosedStrip 0 1)
Tactic: simp only [F, comp_apply, invInterpStrip]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ BddAbove (α := ℝ)
    ((fun (a : ℂ) ↦
        ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
      verticalClosedStrip 0 1)
have hB₁ : ∃ (x : ℝ), ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ x
Tactic: rw [bddAbove_def] at *
Cleared hypotheses: hB