Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.kadiri_rectangle_subset_full_laplace_strip

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Foundations · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Foundations.lean:501 to 523

Mathematical statement

Exact Lean statement

theorem kadiri_rectangle_subset_full_laplace_strip {a b T : ℝ}
    (ha : 0 < a) (hab : a < b) (hT : 0 ≤ T) :
    Rectangle (((-a : ℝ) : ℂ) + ((-T : ℝ) : ℂ) * I)
        (((1 + a : ℝ) : ℂ) + (T : ℂ) * I) ⊆
      {s : ℂ | -b < s.re ∧ s.re < 1 + b}

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem kadiri_rectangle_subset_full_laplace_strip {a b T : ℝ}    (ha : 0 < a) (hab : a < b) (hT : 0 ≤ T) :    Rectangle (((-a : ℝ) : ℂ) + ((-T : ℝ) : ℂ) * I)        (((1 + a : ℝ) : ℂ) + (T : ℂ) * I) ⊆      {s : ℂ | -b < s.re ∧ s.re < 1 + b} := by  intro s hs  have hre :      (((-a : ℝ) : ℂ) + ((-T : ℝ) : ℂ) * I).re ≤        (((1 + a : ℝ) : ℂ) + (T : ℂ) * I).re := by    simp    linarith  have him :      (((-a : ℝ) : ℂ) + ((-T : ℝ) : ℂ) * I).im ≤        (((1 + a : ℝ) : ℂ) + (T : ℂ) * I).im := by    simp    linarith  rcases (mem_Rect hre him s).1 hs with ⟨hsre_lo, hsre_hi, _hsim_lo, _hsim_hi⟩  constructor  · have hleft : -b < -a := by linarith    exact hleft.trans_le (by simpa using hsre_lo)  · have hright : (1 + a : ℝ) < 1 + b := by linarith    have hsre_hi' : s.re ≤ (1 + a : ℝ) := by simpa using hsre_hi    exact hsre_hi'.trans_lt hright