-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem lintegral_rpow_tsum_coe_enorm_sub_le_tsum {f : ℕ → α → E}
    (hf : ∀ n, AEStronglyMeasurable (f n) μ) {p : ℝ} (hp1 : 1 ≤ p) {B : ℕ → ℝ≥0∞}
    (h : ∀ n, ∫⁻ a, (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' i, B i) ^ p) :
    (∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' i, B i

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
⊢ ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop

Tactic:
intro g

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
g : ℕ → ℝ≥0∞
⊢ ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop
h_liminf_pow :
  ∫⁻ (a : α), liminf (fun n => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop ^ p ∂μ =
    ∫⁻ (a : α), liminf (fun n => (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p) atTop ∂μ
n : ℕ
⊢ AEMeasurable (fun a => (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p) μ

Tactic:
exact ((Finset.range _).aemeasurable_sum fun i _ ↦ ((hf _).sub (hf i)).enorm).pow_const _

Result:
no goals

Proof state:
case refine_1
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop
x : α
h_rpow_mono : StrictMono fun x => x ^ p
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun n => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ

case refine_2
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop
x : α
h_rpow_mono : StrictMono fun x => x ^ p
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun n => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ

case refine_3
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop
x : α
h_rpow_mono : StrictMono fun x => x ^ p
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun x_1 =>
    (StrictMono.orderIsoOfSurjective (fun x => x ^ p) h_rpow_mono h_rpow_surj)
      (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)

case refine_4
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop
x : α
h_rpow_mono : StrictMono fun x => x ^ p
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun x_1 =>
    (StrictMono.orderIsoOfSurjective (fun x => x ^ p) h_rpow_mono h_rpow_surj)
      (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)

Tactic:
all_goals isBoundedDefault

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop
h_liminf_pow :
  ∫⁻ (a : α), liminf (fun n => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop ^ p ∂μ =
    ∫⁻ (a : α), liminf (fun n => (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p) atTop ∂μ
⊢ ∫⁻ (a : α), liminf (fun n => (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p) atTop ∂μ ≤
    (∑' (i : ℕ), B i) ^ p

Tactic:
refine (lintegral_liminf_le' fun n ↦ ?_).trans <| liminf_le_of_frequently_le' <| .of_forall h

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop
h_liminf_pow :
  ∫⁻ (a : α), liminf (fun n => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop ^ p ∂μ =
    ∫⁻ (a : α), liminf (fun n => (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p) atTop ∂μ
n : ℕ
⊢ AEMeasurable (fun a => (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p) μ