internlm/Lean-Github huggingface dataset:
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
s_eq_neg_one : s = -1
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
simp [f, s_eq_neg_one]
Proof state after:
no goals
Theorem: Perron.f_mul_eq_f
Proof state before:
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
Tactic:
convert Complex.cpow_neg_eq_inv_pow_ofReal_pos xpos s
Proof state after:
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
⊢ ↑x⁻¹ = (↑x)⁻¹
Theorem: Perron.f_mul_eq_f
Proof state before:
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
⊢ ↑x⁻¹ = (↑x)⁻¹
Tactic:
exact ofReal_inv x
Proof state after:
no goals
Theorem: Perron.f_mul_eq_f
Proof state before:
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⁻¹
Tactic:
simp only [ofReal_inv]
Proof state after:
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 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)⁻¹
Tactic:
rfl
Proof state after:
no goals
Theorem: Perron.isHolomorphicOn
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (f x) {0, -1}ᶜ
Tactic:
unfold f
Proof state after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (fun s => ↑x ^ s / (s * (s + 1))) {0, -1}ᶜ
Theorem: Perron.isHolomorphicOn
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (fun s => ↑x ^ s / (s * (s + 1))) {0, -1}ᶜ
Tactic:
simp_rw [Complex.cpow_def_of_ne_zero <| ofReal_ne_zero.mpr <| ne_of_gt xpos]
Proof state after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (fun s => cexp ((↑x).log * s) / (s * (s + 1))) {0, -1}ᶜ
Theorem: Perron.isHolomorphicOn
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ HolomorphicOn (fun s => cexp ((↑x).log * s) / (s * (s + 1))) {0, -1}ᶜ
Tactic:
apply DifferentiableOn.div <| DifferentiableOn.cexp <| DifferentiableOn.const_mul differentiableOn_id _
Proof state after:
case hd
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ DifferentiableOn ℂ (fun x => x * (x + 1)) {0, -1}ᶜ

case hx
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ ∀ x ∈ {0, -1}ᶜ, x * (x + 1) ≠ 0
Theorem: Perron.isHolomorphicOn
Proof state before:
case hd
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ DifferentiableOn ℂ (fun x => x * (x + 1)) {0, -1}ᶜ
Tactic:
exact DifferentiableOn.mul differentiableOn_id <| DifferentiableOn.add_const differentiableOn_id 1
Proof state after:
no goals
Theorem: Perron.isHolomorphicOn
Proof state before:
case hx
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ ∀ x ∈ {0, -1}ᶜ, x * (x + 1) ≠ 0
Tactic:
intro x hx
Proof state after:
case hx
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
x : ℂ
hx : x ∈ {0, -1}ᶜ
⊢ x * (x + 1) ≠ 0
Theorem: Perron.isHolomorphicOn
Proof state before:
case hx
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
x : ℂ
hx : x ∈ {0, -1}ᶜ
⊢ x * (x + 1) ≠ 0
Tactic:
obtain ⟨h0, h1⟩ := not_or.mp hx
Proof state after:
case hx.intro
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
x : ℂ
hx : x ∈ {0, -1}ᶜ
h0 : ¬x = 0
h1 : x ∉ {-1}
⊢ x * (x + 1) ≠ 0
Theorem: Perron.isHolomorphicOn
Proof state before:
case hx.intro
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
x : ℂ
hx : x ∈ {0, -1}ᶜ
h0 : ¬x = 0
h1 : x ∉ {-1}
⊢ x * (x + 1) ≠ 0
Tactic:
exact mul_ne_zero h0 <| add_ne_add_left 1 |>.mpr h1 |>.trans_eq (add_left_neg 1)
Proof state after:
no goals
Theorem: Perron.integral_one_div_const_add_sq_pos
Proof state before:
x σ σ' σ'' T c : ℝ
hc : 0 < c
⊢ 0 < ∫ (t : ℝ), 1 / (c + t ^ 2)
Tactic:
have hfun_eq (t : ℝ) : 1 / (c + t ^ 2) = c⁻¹ * (1 + (c.sqrt⁻¹ * t) ^ 2)⁻¹ := by
  field_simp [hc.ne.symm]
Proof state after:
x σ σ' σ'' T c : ℝ
hc : 0 < c
hfun_eq : ∀ (t : ℝ), 1 / (c + t ^ 2) = c⁻¹ * (1 + ((√c)⁻¹ * t) ^ 2)⁻¹
⊢ 0 < ∫ (t : ℝ), 1 / (c + t ^ 2)
Theorem: Perron.integral_one_div_const_add_sq_pos
Proof state before:
x σ σ' σ'' T c : ℝ
hc : 0 < c
hfun_eq : ∀ (t : ℝ), 1 / (c + t ^ 2) = c⁻¹ * (1 + ((√c)⁻¹ * t) ^ 2)⁻¹
⊢ 0 < ∫ (t : ℝ), 1 / (c + t ^ 2)
Tactic:
simp_rw [hfun_eq, MeasureTheory.integral_mul_left,
  Measure.integral_comp_mul_left (fun t ↦ (1 + t ^ 2)⁻¹) (a:=c.sqrt⁻¹)]
Proof state after:
x σ σ' σ'' T c : ℝ
hc : 0 < c
hfun_eq : ∀ (t : ℝ), 1 / (c + t ^ 2) = c⁻¹ * (1 + ((√c)⁻¹ * t) ^ 2)⁻¹
⊢ 0 < c⁻¹ * |(√c)⁻¹⁻¹| • ∫ (y : ℝ), (1 + y ^ 2)⁻¹
Theorem: Perron.integral_one_div_const_add_sq_pos
Proof state before:
x σ σ' σ'' T c : ℝ
hc : 0 < c
hfun_eq : ∀ (t : ℝ), 1 / (c + t ^ 2) = c⁻¹ * (1 + ((√c)⁻¹ * t) ^ 2)⁻¹
⊢ 0 < c⁻¹ * |(√c)⁻¹⁻¹| • ∫ (y : ℝ), (1 + y ^ 2)⁻¹
Tactic:
simp [abs_eq_self.mpr <| Real.sqrt_nonneg c,
  mul_pos (inv_pos.mpr hc) <| mul_pos (sqrt_pos.mpr hc) Real.pi_pos]
Proof state after:
no goals
Theorem: Perron.integral_one_div_const_add_sq_pos
Proof state before:
x σ σ' σ'' T c : ℝ
hc : 0 < c
t : ℝ
⊢ 1 / (c + t ^ 2) = c⁻¹ * (1 + ((√c)⁻¹ * t) ^ 2)⁻¹
Tactic:
field_simp [hc.ne.symm]
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
have c₂_pos : 0 < c₂ := by linarith
Proof state after:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
have hlower (t : ℝ) : 1 / (c₂ + t ^ 2) ≤ 1 / ((c₁ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt) := by
  gcongr
  calc
    _ ≤ (c₂ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt := by gcongr
    _ ≤ c₂ + t ^ 2 := by rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity
Proof state after:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
have hupper (t : ℝ) : 1 / ((c₁ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt) ≤ 1 / (c₁ + t ^ 2)  := by
    gcongr
    calc
      _ ≥ (c₁ + t ^ 2).sqrt * (c₁ + t ^ 2).sqrt := by gcongr
      _ ≥ c₁ + t ^ 2 := by rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity
Proof state after:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
calc 0 < ∫ t, 1 / (c₂ + t^2) := integral_one_div_const_add_sq_pos c₂ c₂_pos
     _ ≤ ∫ t, 1 / (Real.sqrt (c₁ + t^2) * Real.sqrt (c₂ + t^2)) := ?_
Proof state after:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ ∫ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ ∫ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
refine integral_mono (Integrable.one_div_const_add_sq c₂ c₂_pos) ?_ hlower
Proof state after:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ Integrable (fun t => 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))) volume
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ Integrable (fun t => 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))) volume
Tactic:
apply MeasureTheory.Integrable.mono (g := fun t:ℝ ↦ 1/(c₁ + t^2)) <| Integrable.one_div_const_add_sq c₁ c₁_pos
Proof state after:
case hf
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ AEStronglyMeasurable (fun t => 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))) volume

case h
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ ∀ᵐ (a : ℝ), ‖1 / (√(c₁ + a ^ 2) * √(c₂ + a ^ 2))‖ ≤ ‖1 / (c₁ + a ^ 2)‖
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
⊢ 0 < c₂
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
t : ℝ
⊢ 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
gcongr
Proof state after:
case h
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
t : ℝ
⊢ √(c₁ + t ^ 2) * √(c₂ + t ^ 2) ≤ c₂ + t ^ 2
Theorem: Perron.integralPosAux'_of_le
Proof state before:
case h
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
t : ℝ
⊢ √(c₁ + t ^ 2) * √(c₂ + t ^ 2) ≤ c₂ + t ^ 2
Tactic:
calc
  _ ≤ (c₂ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt := by gcongr
  _ ≤ c₂ + t ^ 2 := by rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
t : ℝ
⊢ √(c₁ + t ^ 2) * √(c₂ + t ^ 2) ≤ √(c₂ + t ^ 2) * √(c₂ + t ^ 2)
Tactic:
gcongr
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
t : ℝ
⊢ √(c₂ + t ^ 2) * √(c₂ + t ^ 2) ≤ c₂ + t ^ 2
Tactic:
rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
t : ℝ
⊢ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
Tactic:
gcongr
Proof state after:
case h
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
t : ℝ
⊢ c₁ + t ^ 2 ≤ √(c₁ + t ^ 2) * √(c₂ + t ^ 2)
Theorem: Perron.integralPosAux'_of_le
Proof state before:
case h
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
t : ℝ
⊢ c₁ + t ^ 2 ≤ √(c₁ + t ^ 2) * √(c₂ + t ^ 2)
Tactic:
calc
  _ ≥ (c₁ + t ^ 2).sqrt * (c₁ + t ^ 2).sqrt := by gcongr
  _ ≥ c₁ + t ^ 2 := by rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
t : ℝ
⊢ √(c₁ + t ^ 2) * √(c₂ + t ^ 2) ≥ √(c₁ + t ^ 2) * √(c₁ + t ^ 2)
Tactic:
gcongr
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
t : ℝ
⊢ √(c₁ + t ^ 2) * √(c₁ + t ^ 2) ≥ c₁ + t ^ 2
Tactic:
rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
case hf
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ AEStronglyMeasurable (fun t => 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))) volume
Tactic:
refine (measurable_const.div <| Measurable.mul ?_ ?_).aestronglyMeasurable <;>
  exact (measurable_const.add <| measurable_id'.pow_const 2).sqrt
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
case h
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ ∀ᵐ (a : ℝ), ‖1 / (√(c₁ + a ^ 2) * √(c₂ + a ^ 2))‖ ≤ ‖1 / (c₁ + a ^ 2)‖
Tactic:
refine ae_of_all _ (fun x ↦ ?_)
Proof state after:
case h
x✝ σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
x : ℝ
⊢ ‖1 / (√(c₁ + x ^ 2) * √(c₂ + x ^ 2))‖ ≤ ‖1 / (c₁ + x ^ 2)‖
Theorem: Perron.integralPosAux'_of_le
Proof state before:
case h
x✝ σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
x : ℝ
⊢ ‖1 / (√(c₁ + x ^ 2) * √(c₂ + x ^ 2))‖ ≤ ‖1 / (c₁ + x ^ 2)‖
Tactic:
repeat rewrite [norm_of_nonneg (by positivity)]
Proof state after:
case h
x✝ σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
x : ℝ
⊢ 1 / (√(c₁ + x ^ 2) * √(c₂ + x ^ 2)) ≤ 1 / (c₁ + x ^ 2)
Theorem: Perron.integralPosAux'_of_le
Proof state before:
case h
x✝ σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
x : ℝ
⊢ 1 / (√(c₁ + x ^ 2) * √(c₂ + x ^ 2)) ≤ 1 / (c₁ + x ^ 2)
Tactic:
exact hupper x
Proof state after:
no goals
Theorem: Perron.integralPosAux'_of_le
Proof state before:
case h
x✝ σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
x : ℝ
⊢ 1 / (√(c₁ + x ^ 2) * √(c₂ + x ^ 2)) ≤ ‖1 / (c₁ + x ^ 2)‖
Tactic:
rewrite [norm_of_nonneg (by positivity)]
Proof state after:
case h
x✝ σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
x : ℝ
⊢ 1 / (√(c₁ + x ^ 2) * √(c₂ + x ^ 2)) ≤ 1 / (c₁ + x ^ 2)
Theorem: Perron.integralPosAux'_of_le
Proof state before:
x✝ σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
x : ℝ
⊢ 0 ≤ 1 / (c₁ + x ^ 2)
Tactic:
positivity
Proof state after:
no goals
Theorem: Perron.integralPosAux'
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
by_cases hc : c₁ ≤ c₂
Proof state after:
case pos
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))

case neg
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Theorem: Perron.integralPosAux'
Proof state before:
case pos
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
exact integralPosAux'_of_le c₁ c₂ c₁_pos hc
Proof state after:
no goals
Theorem: Perron.integralPosAux'
Proof state before:
case neg
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
convert integralPosAux'_of_le c₂ c₁ c₂_pos (by linarith) using 4
Proof state after:
case h.e'_4.h.e'_7.h.h.e'_6
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
x✝ : ℝ
⊢ √(c₁ + x✝ ^ 2) * √(c₂ + x✝ ^ 2) = √(c₂ + x✝ ^ 2) * √(c₁ + x✝ ^ 2)
Theorem: Perron.integralPosAux'
Proof state before:
case h.e'_4.h.e'_7.h.h.e'_6
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
x✝ : ℝ
⊢ √(c₁ + x✝ ^ 2) * √(c₂ + x✝ ^ 2) = √(c₂ + x✝ ^ 2) * √(c₁ + x✝ ^ 2)
Tactic:
rw [mul_comm]
Proof state after:
no goals
Theorem: Perron.integralPosAux'
Proof state before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
⊢ c₂ ≤ c₁
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.integralPosAux
Proof state before:
x σ σ' σ'' T : ℝ
⊢ 0 < ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
apply integralPosAux' <;> norm_num
Proof state after:
no goals
Theorem: Perron.vertIntBound
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ‖VerticalIntegral (f x) σ‖ ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
calc
  _ = ‖∫ (t : ℝ), x ^ (σ + t * I) / ((σ + t * I) * (σ + t * I + 1))‖ := ?_
  _ ≤ ∫ (t : ℝ), ‖x ^ (σ + t * I) / ((σ + t * I) * (σ + t * I + 1))‖ :=
      norm_integral_le_integral_norm _
  _ = ∫ (t : ℝ), x ^ σ / ‖((σ + t * I) * (σ + t * I + 1))‖ := ?_
  _ = x ^ σ * ∫ (t : ℝ), 1 / (‖σ + t * I‖ * ‖σ + t * I + 1‖) := ?_
  _ ≤ x ^ σ * ∫ (t : ℝ), 1 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt) :=
      mul_le_mul_of_nonneg_left ?_ (rpow_nonneg xpos.le _)
Proof state after:
case calc_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ‖VerticalIntegral (f x) σ‖ = ‖∫ (t : ℝ), ↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖

case calc_2
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (t : ℝ), ‖↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖ =
    ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖

case calc_3
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖ = x ^ σ * ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖)

case calc_4
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Theorem: Perron.vertIntBound
Proof state before:
case calc_4
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
by_cases hint : Integrable fun (a : ℝ) ↦ 1 / (‖σ + a * I‖ * ‖σ + a * I + 1‖)
Proof state after:
case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Theorem: Perron.vertIntBound
Proof state before:
case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
swap
Proof state after:
case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Theorem: Perron.vertIntBound
Proof state before:
case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
rw [integral_undef hint]
Proof state after:
case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ 0 ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Theorem: Perron.vertIntBound
Proof state before:
case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ 0 ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
exact integral_nonneg <| fun t ↦ by positivity
Proof state after:
case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))