-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integrableOn_Ioi_rpow_iff {s t : ℝ} (ht : 0 < t) :
    IntegrableOn (fun x ↦ x ^ s) (Ioi t) ↔ s < -1

Proof state:
case h
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
x : ℝ
hx : x ∈ Ioi (1 ⊔ t)
x_one : 1 ≤ x
⊢ x⁻¹ ≤ x ^ s

Tactic:
rw [← Real.rpow_neg_one x]

Result:
case h
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
x : ℝ
hx : x ∈ Ioi (1 ⊔ t)
x_one : 1 ≤ x
⊢ x ^ (-1) ≤ x ^ s

Proof state:
s t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => x ^ s) (Ioi t) volume
⊢ s < -1

Tactic:
contrapose! h

Result:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
⊢ ¬IntegrableOn (fun x => x ^ s) (Ioi t) volume

Proof state:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
⊢ IntegrableOn (fun x => x⁻¹) (Ioi (1 ⊔ t)) volume

Tactic:
apply H'.mono' measurable_inv.aestronglyMeasurable

Result:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi (1 ⊔ t)), ‖a⁻¹‖ ≤ a ^ s

Proof state:
s t : ℝ
ht : 0 < t
⊢ IntegrableOn (fun x => x ^ s) (Ioi t) volume ↔ s < -1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_rpow_of_lt h ht⟩

Result:
s t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => x ^ s) (Ioi t) volume
⊢ s < -1

Proof state:
case h
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
x : ℝ
hx : x ∈ Ioi (1 ⊔ t)
⊢ ‖x⁻¹‖ ≤ x ^ s

Tactic:
have x_one : 1 ≤ x := ((le_max_left _ _).trans_lt (mem_Ioi.1 hx)).le

Result:
case h
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
x : ℝ
hx : x ∈ Ioi (1 ⊔ t)
x_one : 1 ≤ x
⊢ ‖x⁻¹‖ ≤ x ^ s

Proof state:
case h
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
x : ℝ
hx : x ∈ Ioi (1 ⊔ t)
x_one : 1 ≤ x
⊢ x ^ (-1) ≤ x ^ s

Tactic:
exact Real.rpow_le_rpow_of_exponent_le x_one h

Result:
no goals

Proof state:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
⊢ False

Tactic:
have H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) :=
  H.mono (Set.Ioi_subset_Ioi (le_max_right _ _)) le_rfl

Result:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
⊢ False

Proof state:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
⊢ ¬IntegrableOn (fun x => x ^ s) (Ioi t) volume

Tactic:
intro H

Result:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
⊢ False

Proof state:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
this : IntegrableOn (fun x => x⁻¹) (Ioi (1 ⊔ t)) volume
⊢ False

Tactic:
exact not_IntegrableOn_Ioi_inv this

Result:
no goals

Proof state:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
⊢ False

Tactic:
have : IntegrableOn (fun x ↦ x⁻¹) (Ioi (max 1 t)) := by
  apply H'.mono' measurable_inv.aestronglyMeasurable
  filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
  have x_one : 1 ≤ x := ((le_max_left _ _).trans_lt (mem_Ioi.1 hx)).le
  simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans x_one)]
  rw [← Real.rpow_neg_one x]
  exact Real.rpow_le_rpow_of_exponent_le x_one h

Result:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
this : IntegrableOn (fun x => x⁻¹) (Ioi (1 ⊔ t)) volume
⊢ False

Proof state:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi (1 ⊔ t)), ‖a⁻¹‖ ≤ a ^ s

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx

Result:
case h
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
x : ℝ
hx : x ∈ Ioi (1 ⊔ t)
⊢ ‖x⁻¹‖ ≤ x ^ s

Proof state:
case h
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
x : ℝ
hx : x ∈ Ioi (1 ⊔ t)
x_one : 1 ≤ x
⊢ ‖x⁻¹‖ ≤ x ^ s

Tactic:
simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans x_one)]

Result:
case h
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x => x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x => x ^ s) (Ioi (1 ⊔ t)) volume
x : ℝ
hx : x ∈ Ioi (1 ⊔ t)
x_one : 1 ≤ x
⊢ x⁻¹ ≤ x ^ s