Theorem: Perron.integral_one_div_const_add_sq_pos (PrimeNumberTheoremAnd/PerronFormula.lean)

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]
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)

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⁻¹)]
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)⁻¹

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]
State after:
no goals

State before:
x σ σ' σ'' T c : ℝ
hc : 0 < c
t : ℝ
⊢ 1 / (c + t ^ 2) = c⁻¹ * (1 + ((√c)⁻¹ * t) ^ 2)⁻¹
Tactic:
field_simp [hc.ne.symm]
State after:
no goals