awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
x : α
⊢ StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p

Tactic:
have h_rpow_mono := ENNReal.strictMono_rpow_of_pos (zero_lt_one.trans_le hp1)
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
⊢ Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p

Tactic:
have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ) atTop) p =
    liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ) p) atTop

Tactic:
(h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_

Premises used: ENNReal.rpow, OrderIso.liminf_apply, StrictMono.orderIsoOfSurjective
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
refine_1 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ
refine_2 :
  IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ
refine_3 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)
refine_4 :
  IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ) atTop) p =
    liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ) p) atTop

Tactic:
refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_

Premises used: OrderIso.liminf_apply, StrictMono.orderIsoOfSurjective
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ₑ

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
x : α
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (∑ i ∈ Finset.range (x_1 + 1), ‖f (i + 1) x - f i x‖ₑ)

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
⊢ ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ =
    ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ

Tactic:
have h_liminf_pow :
    ∫⁻ a, (atTop.liminf fun n => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ =
      ∫⁻ a, atTop.liminf fun n => (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ := by
    refine lintegral_congr fun x => ?_
    have h_rpow_mono := ENNReal.strictMono_rpow_of_pos (zero_lt_one.trans_le hp1)
    have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
    refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
    all_goals isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
h_liminf_pow :
  ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ =
    ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ
rw :
  ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
⊢ ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p

Tactic:
rw [h_liminf_pow]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
h_liminf_pow :
  ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ =
    ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ
⊢ ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p

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

Premises used: Filter.Frequently.of_forall, Filter.liminf_le_of_frequently_le', LE.le.trans, MeasureTheory.lintegral_liminf_le'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
h_liminf_pow :
  ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ =
    ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ
refine :
  ∀ (n : ℕ),
    AEMeasurable (β := ℝ≥0∞)
      (fun (a : α) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) μ
⊢ ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p

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

Premises used: Filter.liminf_le_of_frequently_le', LE.le.trans, MeasureTheory.lintegral_liminf_le'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
h_liminf_pow :
  ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ =
    ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ
n : ℕ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p)
    μ

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

Premises used: AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.sub, Finset.aemeasurable_fun_sum, Finset.range, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
hp_pos : 0 < p
h_tsum_1 :
  ∀ (g : ℕ → ℝ≥0∞), Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
h_liminf_pow :
  ∫⁻ (a : α),
      HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop) p ∂μ =
    ∫⁻ (a : α),
      liminf (fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p) atTop ∂μ
n : ℕ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p)
    μ

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

Premises used: AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.sub, Finset.aemeasurable_fun_sum, Finset.range, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
⊢ 0 < p

Tactic:
have hp_pos : 0 < p := zero_lt_one.trans_le hp1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞

Tactic:
have h_tsum_lt_top : (∑' i, B i) ^ p < ∞ := ENNReal.rpow_lt_top_of_nonneg hp_pos.le hB
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞

Tactic:
lt_of_le_of_lt ?_ h_tsum_lt_top

Premises used: lt_of_le_of_lt
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞
refine :
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞

Tactic:
refine lt_of_le_of_lt ?_ h_tsum_lt_top

Premises used: lt_of_le_of_lt
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞
⊢ 0 < p⁻¹

Tactic:
simp [hp_pos]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞
rwa :
  ∀ (h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i)
    (hp_pos : 0 < p) (h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
rwa₁ :
  ∀
    (h :
      ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
        HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p⁻¹⁻¹)
    (hp_pos : 0 < p) (h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (h :
      ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
        HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p)
    (hp_pos : 0 < p) (h_tsum_lt_top : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p < ∞),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p

Tactic:
rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv] at h

Premises used: ENNReal.le_rpow_inv_iff, inv_inv, one_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞

Tactic:
have h_integral : ∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ < ∞ := by
    have h_tsum_lt_top : (∑' i, B i) ^ p < ∞ := ENNReal.rpow_lt_top_of_nonneg hp_pos.le hB
    refine lt_of_le_of_lt ?_ h_tsum_lt_top
    rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv] at h
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
⊢ ∀ᵐ (x : α) ∂μ, HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞

Tactic:
ae_lt_top' (AEMeasurable.pow_const ?_ _) h_integral.ne

Premises used: AEMeasurable.pow_const, MeasureTheory.ae_lt_top', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
refine : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) μ
⊢ ∀ᵐ (x : α) ∂μ, HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞

Tactic:
refine ae_lt_top' (AEMeasurable.pow_const ?_ _) h_integral.ne

Premises used: AEMeasurable.pow_const, MeasureTheory.ae_lt_top', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) μ

Tactic:
AEMeasurable.tsum fun n => ((hf (n + 1)).sub (hf n)).enorm

Premises used: MeasureTheory.AEStronglyMeasurable.sub, HAdd.hAdd, AEMeasurable.tsum, MeasureTheory.AEStronglyMeasurable.enorm, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) μ

Tactic:
exact AEMeasurable.tsum fun n => ((hf (n + 1)).sub (hf n)).enorm

Premises used: MeasureTheory.AEStronglyMeasurable.sub, HAdd.hAdd, AEMeasurable.tsum, MeasureTheory.AEStronglyMeasurable.enorm, OfNat.ofNat