internlm/Lean-Github huggingface dataset:
Theorem: LogDerivZetaBnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C),
          ∀ (σ t : ℝ),
            3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 9
Tactic:
obtain ⟨A', hA', C', hC', h'⟩ := ZetaDerivUpperBnd
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C),
          ∀ (σ t : ℝ),
            3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C),
          ∀ (σ t : ℝ),
            3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 9
Tactic:
use min A A', ⟨lt_min hA.1 hA'.1, min_le_of_right_le hA'.2⟩, C * C', mul_pos hC hC'
Proof state after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ∀ (σ t : ℝ),
    3 < |t| → σ ∈ Ico (1 - min A A' / |t|.log ^ 9) 1 → ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ∀ (σ t : ℝ),
    3 < |t| → σ ∈ Ico (1 - min A A' / |t|.log ^ 9) 1 → ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
intro σ t t_gt ⟨σ_ge, σ_lt⟩
Proof state after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
have logt_gt : (1 : ℝ) < Real.log |t| := by
  refine (Real.lt_log_iff_exp_lt (by linarith)).mpr (lt_trans ?_ t_gt)
  exact lt_trans Real.exp_one_lt_d9 (by norm_num)
Proof state after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
have σ_ge' : 1 - A / Real.log |t| ^ 9 ≤ σ := by
  apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
  apply div_le_div hA.1.le (min_le_left A A') ?_ (by rfl)
  exact pow_pos (lt_trans (by norm_num) logt_gt) 9
Proof state after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
have σ_ge'' : 1 - A' / Real.log |t| ≤ σ := by
  apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
  apply div_le_div hA'.1.le (min_le_right A A') (lt_trans (by norm_num) logt_gt) ?_
  exact le_self_pow logt_gt.le (by norm_num)
Proof state after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
replace h := h σ t t_gt ⟨σ_ge', σ_lt⟩
Proof state after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
replace h' := h' σ t t_gt ⟨σ_ge'', by linarith⟩
Proof state after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
simp only [norm_div, norm_one, norm_mul, norm_inv]
Proof state after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ / ‖ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ / ‖ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
convert mul_le_mul h h' (by simp [apply_nonneg]) ?_ using 1 <;> (norm_cast; ring_nf)
Proof state after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ 0 ≤ C * |t|.log ^ 7
Theorem: LogDerivZetaBnd
Proof state before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ 0 ≤ C * |t|.log ^ 7
Tactic:
positivity
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ 1 < |t|.log
Tactic:
refine (Real.lt_log_iff_exp_lt (by linarith)).mpr (lt_trans ?_ t_gt)
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ Real.exp 1 < 3
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ Real.exp 1 < 3
Tactic:
exact lt_trans Real.exp_one_lt_d9 (by norm_num)
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ 0 < |t|
Tactic:
linarith
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ 2.7182818286 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ 1 - A / |t|.log ^ 9 ≤ σ
Tactic:
apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ min A A' / |t|.log ^ 9 ≤ A / |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ min A A' / |t|.log ^ 9 ≤ A / |t|.log ^ 9
Tactic:
apply div_le_div hA.1.le (min_le_left A A') ?_ (by rfl)
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ 0 < |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ 0 < |t|.log ^ 9
Tactic:
exact pow_pos (lt_trans (by norm_num) logt_gt) 9
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ |t|.log ^ 9 ≤ |t|.log ^ 9
Tactic:
rfl
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ 1 - A' / |t|.log ≤ σ
Tactic:
apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ min A A' / |t|.log ^ 9 ≤ A' / |t|.log
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ min A A' / |t|.log ^ 9 ≤ A' / |t|.log
Tactic:
apply div_le_div hA'.1.le (min_le_right A A') (lt_trans (by norm_num) logt_gt) ?_
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ |t|.log ≤ |t|.log ^ 9
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ |t|.log ≤ |t|.log ^ 9
Tactic:
exact le_self_pow logt_gt.le (by norm_num)
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ 9 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
⊢ σ ≤ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ 0 ≤ ‖deriv ζ (↑σ + ↑t * I)‖
Tactic:
simp [apply_nonneg]
Proof state after:
no goals
Theorem: LogDerivZetaBnd
Proof state before:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ C * C' * |t|.log ^ 9 = C * |t|.log ^ 7 * (C' * |t|.log ^ 2)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: IntegrableAtFilter.sup_iff
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup β
l✝ l'✝ : Filter α
f g : α → β
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ
Tactic:
use fun h => ⟨h.filter_mono le_sup_left, h.filter_mono le_sup_right⟩
Proof state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup β
l✝ l'✝ : Filter α
f g : α → β
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ
Theorem: IntegrableAtFilter.sup_iff
Proof state before:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup β
l✝ l'✝ : Filter α
f g : α → β
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ
Tactic:
exact fun ⟨⟨s, hsl, hs⟩, ⟨t, htl, ht⟩⟩ ↦ ⟨s ∪ t, union_mem_sup hsl htl, hs.union ht⟩
Proof state after:
no goals
Theorem: Rectangle.symm
Proof state before:
z w : ℂ
c : ℝ
⊢ Rectangle z w = Rectangle w z
Tactic:
simp [Rectangle, uIcc_comm]
Proof state after:
no goals
Theorem: Rectangle.symm_re
Proof state before:
z w : ℂ
c : ℝ
⊢ Rectangle (↑w.re + ↑z.im * I) (↑z.re + ↑w.im * I) = Rectangle z w
Tactic:
simp [Rectangle, uIcc_comm]
Proof state after:
no goals