internlm/Lean-Github huggingface dataset:
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Tactic:
have := ((hbot'.sub htop).add (hvert σ' hright)).sub (hvert σ hleft)
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x_1 : ℝ) in σ..σ', f (↑x_1 - ↑x * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +
          I * ∫ (y : ℝ) in -x..-T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in -x..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((0 - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x_1 : ℝ) in σ..σ', f (↑x_1 - ↑x * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +
          I * ∫ (y : ℝ) in -x..-T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in -x..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((0 - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Tactic:
rw [zero_sub] at this
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x_1 : ℝ) in σ..σ', f (↑x_1 - ↑x * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +
          I * ∫ (y : ℝ) in -x..-T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in -x..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x_1 : ℝ) in σ..σ', f (↑x_1 - ↑x * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +
          I * ∫ (y : ℝ) in -x..-T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in -x..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 (-LowerUIntegral f σ σ' T))
Tactic:
simp_rw [RectangleIntegral, LowerUIntegral, HIntegral, VIntegral, h_re, h_im, ofReal_neg, neg_mul, neg_add_rev, neg_sub]
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x_1 : ℝ) in σ..σ', f (↑x_1 - ↑x * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +
          I * ∫ (y : ℝ) in -x..-T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in -x..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)))
⊢ Tendsto
    (fun U =>
      (((∫ (x : ℝ) in σ..σ', f (↑x + -(↑U * I))) - ∫ (x : ℝ) in σ..σ', f (↑x + -(↑T * I))) +
          I • ∫ (y : ℝ) in -U..-T, f (↑σ' + ↑y * I)) -
        I • ∫ (y : ℝ) in -U..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (-(I • ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) +
        ((I • ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) - ∫ (x : ℝ) in σ..σ', f (↑x + -(↑T * I)))))
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x_1 : ℝ) in σ..σ', f (↑x_1 - ↑x * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +
          I * ∫ (y : ℝ) in -x..-T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in -x..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)))
final :
  ((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
      I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I) =
    -(I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) +
      ((I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I))
⊢ Tendsto
    (fun U =>
      (((∫ (x : ℝ) in σ..σ', f (↑x + -(↑U * I))) - ∫ (x : ℝ) in σ..σ', f (↑x + -(↑T * I))) +
          I • ∫ (y : ℝ) in -U..-T, f (↑σ' + ↑y * I)) -
        I • ∫ (y : ℝ) in -U..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (-(I • ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) +
        ((I • ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) - ∫ (x : ℝ) in σ..σ', f (↑x + -(↑T * I)))))
Tactic:
exact final ▸ this
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
s t : ℝ
⊢ (↑s - I * ↑t).re = s
Tactic:
simp
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
s t : ℝ
⊢ (↑s - I * ↑t).im = -t
Tactic:
simp
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
⊢ Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
Tactic:
convert (hbot.comp tendsto_neg_atTop_atBot) using 1
Proof state after:
case h.e'_3
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
⊢ (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) = (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) ∘ Neg.neg
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
case h.e'_3
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
⊢ (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) = (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) ∘ Neg.neg
Tactic:
ext
Proof state after:
case h.e'_3.h
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
x✝ : ℝ
⊢ ∫ (x : ℝ) in σ..σ', f (↑x - ↑x✝ * I) = ((fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) ∘ Neg.neg) x✝
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
case h.e'_3.h
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
x✝ : ℝ
⊢ ∫ (x : ℝ) in σ..σ', f (↑x - ↑x✝ * I) = ((fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) ∘ Neg.neg) x✝
Tactic:
simp only [Function.comp_apply, ofReal_neg, neg_mul]
Proof state after:
case h.e'_3.h
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
x✝ : ℝ
⊢ ∫ (x : ℝ) in σ..σ', f (↑x - ↑x✝ * I) = ∫ (x : ℝ) in σ..σ', f (↑x + -(↑x✝ * I))
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
case h.e'_3.h
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
x✝ : ℝ
⊢ ∫ (x : ℝ) in σ..σ', f (↑x - ↑x✝ * I) = ∫ (x : ℝ) in σ..σ', f (↑x + -(↑x✝ * I))
Tactic:
rfl
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
s : ℝ
int : Integrable (fun y => f (↑s + ↑y * I)) volume
⊢ Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
Tactic:
have := (intervalIntegral_tendsto_integral_Iic (-T) int.restrict tendsto_id).const_smul I
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
s : ℝ
int : Integrable (fun y => f (↑s + ↑y * I)) volume
this :
  Tendsto (fun x => I • ∫ (x : ℝ) in id x..-T, f (↑s + ↑x * I)) atBot
    (𝓝 (I • ∫ (x : ℝ) in Iic (-T), f (↑s + ↑x * I) ∂volume))
⊢ Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
s : ℝ
int : Integrable (fun y => f (↑s + ↑y * I)) volume
this :
  Tendsto (fun x => I • ∫ (x : ℝ) in id x..-T, f (↑s + ↑x * I)) atBot
    (𝓝 (I • ∫ (x : ℝ) in Iic (-T), f (↑s + ↑x * I) ∂volume))
⊢ Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
Tactic:
convert (this.comp tendsto_neg_atTop_atBot) using 1
Proof state after:
no goals
Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x_1 : ℝ) in σ..σ', f (↑x_1 - ↑x * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +
          I * ∫ (y : ℝ) in -x..-T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in -x..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)))
⊢ ((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
      I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I) =
    -(I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) +
      ((I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: limitOfConstant
Proof state before:
a : ℝ → ℂ
σ : ℝ
σpos : 0 < σ
ha : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → a σ' = a σ''
ha' : Tendsto a atTop (𝓝 0)
⊢ a σ = 0
Tactic:
have := eventuallyEq_of_mem (mem_atTop σ) fun σ' h ↦ ha σ' σ (σpos.trans_le h) σpos
Proof state after:
a : ℝ → ℂ
σ : ℝ
σpos : 0 < σ
ha : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → a σ' = a σ''
ha' : Tendsto a atTop (𝓝 0)
this : (fun σ' => a σ') =ᶠ[atTop] fun σ' => a σ
⊢ a σ = 0
Theorem: limitOfConstant
Proof state before:
a : ℝ → ℂ
σ : ℝ
σpos : 0 < σ
ha : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → a σ' = a σ''
ha' : Tendsto a atTop (𝓝 0)
this : (fun σ' => a σ') =ᶠ[atTop] fun σ' => a σ
⊢ a σ = 0
Tactic:
exact tendsto_const_nhds_iff.mp (ha'.congr' this)
Proof state after:
no goals
Theorem: limitOfConstantLeft
Proof state before:
a : ℝ → ℂ
σ : ℝ
σlt : σ ≤ -3 / 2
ha : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → a σ' = a σ''
ha' : Tendsto a atBot (𝓝 0)
⊢ a σ = 0
Tactic:
have := eventuallyEq_of_mem (mem_atBot (-3/2)) fun σ' h ↦ ha σ' σ h σlt
Proof state after:
a : ℝ → ℂ
σ : ℝ
σlt : σ ≤ -3 / 2
ha : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → a σ' = a σ''
ha' : Tendsto a atBot (𝓝 0)
this : (fun σ' => a σ') =ᶠ[atBot] fun σ' => a σ
⊢ a σ = 0
Theorem: limitOfConstantLeft
Proof state before:
a : ℝ → ℂ
σ : ℝ
σlt : σ ≤ -3 / 2
ha : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → a σ' = a σ''
ha' : Tendsto a atBot (𝓝 0)
this : (fun σ' => a σ') =ᶠ[atBot] fun σ' => a σ
⊢ a σ = 0
Tactic:
exact tendsto_const_nhds_iff.mp (ha'.congr' this)
Proof state after:
no goals
Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_lt_one
Proof state before:
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
⊢ Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
Tactic:
have := Tendsto.mul_const C (tendsto_rpow_atTop_of_base_lt_one x (by linarith) x_lt_one)
Proof state after:
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
this : Tendsto (fun k => x ^ k * C) atTop (𝓝 (0 * C))
⊢ Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_lt_one
Proof state before:
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
this : Tendsto (fun k => x ^ k * C) atTop (𝓝 (0 * C))
⊢ Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
Tactic:
simpa only [rpow_eq_pow, zero_mul] using this
Proof state after:
no goals
Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_lt_one
Proof state before:
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
⊢ -1 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_gt_one
Proof state before:
x : ℝ
x_gt_one : 1 < x
C : ℝ
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
Tactic:
have := (zero_lt_one.trans x_gt_one)
Proof state after:
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_gt_one
Proof state before:
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
Tactic:
have h := tendsto_rpow_atTop_nhds_zero_of_norm_lt_one (inv_pos.mpr this) (inv_lt_one x_gt_one) C
Proof state after:
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_gt_one
Proof state before:
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
Tactic:
convert (h.comp tendsto_neg_atBot_atTop) using 1
Proof state after:
case h.e'_3
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
⊢ (fun σ => x ^ σ * C) = (fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg
Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_gt_one
Proof state before:
case h.e'_3
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
⊢ (fun σ => x ^ σ * C) = (fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg
Tactic:
ext
Proof state after:
case h.e'_3.h
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
x✝ : ℝ
⊢ x ^ x✝ * C = ((fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg) x✝
Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_gt_one
Proof state before:
case h.e'_3.h
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
x✝ : ℝ
⊢ x ^ x✝ * C = ((fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg) x✝
Tactic:
simp only [this.le, inv_rpow, Function.comp_apply, rpow_neg, inv_inv]
Proof state after:
no goals
Theorem: Complex.cpow_inv_ofReal_pos
Proof state before:
a : ℝ
ha : 0 ≤ a
r : ℂ
⊢ (↑a ^ r)⁻¹ = (↑a)⁻¹ ^ r
Tactic:
sorry
Proof state after:
no goals
Theorem: Complex.cpow_eq_exp_log_ofReal
Proof state before:
x : ℝ
hx : 0 < x
y : ℂ
⊢ ↑x ^ y = cexp (↑x.log * y)
Tactic:
simp [← Complex.cpow_eq_pow, Complex.cpow, hx.ne.symm, ← Complex.ofReal_log hx.le]
Proof state after:
no goals
Theorem: Complex.cpow_neg_eq_inv_pow_ofReal_pos
Proof state before:
a : ℝ
ha : 0 < a
r : ℂ
⊢ ↑a ^ (-r) = (↑a)⁻¹ ^ r
Tactic:
rw [cpow_neg, ← Complex.inv_cpow]
Proof state after:
case hx
a : ℝ
ha : 0 < a
r : ℂ
⊢ (↑a).arg ≠ π
Theorem: Complex.cpow_neg_eq_inv_pow_ofReal_pos
Proof state before:
case hx
a : ℝ
ha : 0 < a
r : ℂ
⊢ (↑a).arg ≠ π
Tactic:
exact slitPlane_arg_ne_pi (Or.inl ha)
Proof state after:
no goals
Theorem: Perron.f_mul_eq_f
Proof state before:
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
by_cases s_eq_zero : s = 0
Proof state after:
case pos
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : s = 0
⊢ f t s * ↑x ^ (-s) = f (t / x) s

case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Theorem: Perron.f_mul_eq_f
Proof state before:
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
by_cases s_eq_neg_one : s = -1
Proof state after:
case pos
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : s = -1
⊢ f t s * ↑x ^ (-s) = f (t / x) s

case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Theorem: Perron.f_mul_eq_f
Proof state before:
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
field_simp [f, mul_ne_zero s_eq_zero (fun hs ↦ add_eq_zero_iff_eq_neg.mp hs |> s_eq_neg_one)]
Proof state after:
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t ^ s * ↑x ^ (-s) = (↑t / ↑x) ^ s
Theorem: Perron.f_mul_eq_f
Proof state before:
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t ^ s * ↑x ^ (-s) = (↑t / ↑x) ^ s
Tactic:
convert (Complex.mul_cpow_ofReal_nonneg tpos.le (inv_pos.mpr xpos).le s).symm using 2
Proof state after:
case h.e'_2.h.e'_6
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑x ^ (-s) = ↑x⁻¹ ^ s

case h.e'_3.h.e'_5
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t / ↑x = ↑t * ↑x⁻¹
Theorem: Perron.f_mul_eq_f
Proof state before:
case pos
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : s = 0
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
simp [f, s_eq_zero]
Proof state after:
no goals