-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
/-- The power function `x ↦ x^s` is integrable on `(0, t)` iff `-1 < s`. -/
lemma integrableOn_Ioo_rpow_iff {s t : ℝ} (ht : 0 < t) :
    IntegrableOn (fun x ↦ x ^ s) (Ioo (0 : ℝ) t) ↔ -1 < s

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

Tactic:
simpa [intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
using intervalIntegrable_rpow' h (a := 0) (b := t)

Result:
no goals

Proof state:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
⊢ False

Tactic:
have : IntegrableOn (fun x ↦ x⁻¹) (Ioo 0 (min 1 t)) := by
  apply H'.mono' measurable_inv.aestronglyMeasurable
  filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx
  simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hx.1)]
  rwa [← Real.rpow_neg_one x, Real.rpow_le_rpow_left_iff_of_base_lt_one hx.1]
  exact lt_of_lt_of_le hx.2 (min_le_left _ _)

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

Proof state:
case h
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
x : ℝ
hx : x ∈ Set.Ioo 0 (1 ⊓ t)
⊢ x⁻¹ ≤ x ^ s

Tactic:
rwa [← Real.rpow_neg_one x, Real.rpow_le_rpow_left_iff_of_base_lt_one hx.1]

Result:
case h
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
x : ℝ
hx : x ∈ Set.Ioo 0 (1 ⊓ t)
⊢ x < 1

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

Tactic:
contrapose! h

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

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

Tactic:
have I : 0 < min 1 t := lt_min zero_lt_one ht

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

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

Tactic:
have H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) :=
  H.mono (Set.Ioo_subset_Ioo le_rfl (min_le_right _ _)) le_rfl

Result:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
⊢ False

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

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx

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

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

Tactic:
have : IntervalIntegrable (fun x ↦ x⁻¹) volume 0 (min 1 t) := by
  rwa [intervalIntegrable_iff_integrableOn_Ioo_of_le I.le]

Result:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
this✝ : IntegrableOn (fun x => x⁻¹) (Set.Ioo 0 (1 ⊓ t)) volume
this : IntervalIntegrable (fun x => x⁻¹) volume 0 (1 ⊓ t)
⊢ False

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

Tactic:
simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hx.1)]

Result:
case h
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
x : ℝ
hx : x ∈ Set.Ioo 0 (1 ⊓ t)
⊢ x⁻¹ ≤ x ^ s

Proof state:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
⊢ IntegrableOn (fun x => x⁻¹) (Set.Ioo 0 (1 ⊓ t)) volume

Tactic:
apply H'.mono' measurable_inv.aestronglyMeasurable

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

Proof state:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
this✝ : IntegrableOn (fun x => x⁻¹) (Set.Ioo 0 (1 ⊓ t)) volume
this : IntervalIntegrable (fun x => x⁻¹) volume 0 (1 ⊓ t)
⊢ False

Tactic:
simp [intervalIntegrable_inv_iff, I.ne] at this

Result:
no goals

Proof state:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
this : IntegrableOn (fun x => x⁻¹) (Set.Ioo 0 (1 ⊓ t)) volume
⊢ IntervalIntegrable (fun x => x⁻¹) volume 0 (1 ⊓ t)

Tactic:
rwa [intervalIntegrable_iff_integrableOn_Ioo_of_le I.le]

Result:
no goals

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

Tactic:
intro H

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

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simpa [intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
  using intervalIntegrable_rpow' h (a := 0) (b := t)⟩

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

Proof state:
case h
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
I : 0 < 1 ⊓ t
H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (1 ⊓ t)) volume
x : ℝ
hx : x ∈ Set.Ioo 0 (1 ⊓ t)
⊢ x < 1

Tactic:
exact lt_of_lt_of_le hx.2 (min_le_left _ _)

Result:
no goals