Theorem: Perron.integralPosAux'_of_le (PrimeNumberTheoremAnd/PerronFormula.lean)

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

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

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

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)) := ?_
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))

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

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

State before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
⊢ 0 < c₂
Tactic:
linarith
State after:
no goals

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

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

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

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

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

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

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

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

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

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 ↦ ?_)
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)‖

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

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

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

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