awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun (n : Fin N) ↦ f (↑n : ℕ)
hF : ∀ (n : Fin N), MemLp (F n) p μ
δ₁ : ℝ
hδpos₁ : 0 < δ₁
hδ₁ :
  ∀ (i : Fin N) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (F i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁
hn : N ≤ n
⊢ eLpNorm (s.indicator (f n)) p μ ≤ ENNReal.ofReal ε

Tactic:
exact (eLpNorm_indicator_le _).trans (hN n hn)

Premises used: MeasureTheory.eLpNorm_indicator_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
h : ∀ (n : ℕ), f n = HAdd.hAdd (α := ℕ → α → β) (β := (n : ℕ) → α → β) (fun (x : ℕ) ↦ g) (fun (n : ℕ) ↦ f n - g) n
⊢ f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g

Tactic:
ext1 n
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
n : ℕ
⊢ f n = HAdd.hAdd (α := ℕ → α → β) (β := (n : ℕ) → α → β) (fun (x : ℕ) ↦ g) (fun (n : ℕ) ↦ f n - g) n

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
⊢ f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g

Tactic:
have : f = (fun _ => g) + fun n => f n - g := by ext1 n; simp
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
rw : UnifIntegrable (HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g) p μ
⊢ UnifIntegrable f p μ

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifIntegrable (HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g) p μ

Tactic:
UnifIntegrable.add ?_ ?_ hp (fun _ => hg.aestronglyMeasurable)
      fun n => (hf n).1.sub hg.aestronglyMeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.sub, And.left, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.UnifIntegrable.add
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
refine_1 : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (x : ℕ) ↦ g) p μ
refine_2 : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ f n - g) p μ
⊢ UnifIntegrable (HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g) p μ

Tactic:
refine UnifIntegrable.add ?_ ?_ hp (fun _ => hg.aestronglyMeasurable)
      fun n => (hf n).1.sub hg.aestronglyMeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.sub, And.left, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.UnifIntegrable.add
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (x : ℕ) ↦ g) p μ

Tactic:
unifIntegrable_const hp hp' hg

Premises used: MeasureTheory.unifIntegrable_const
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (x : ℕ) ↦ g) p μ

Tactic:
exact unifIntegrable_const hp hp' hg

Premises used: MeasureTheory.unifIntegrable_const
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ f n - g) p μ

Tactic:
unifIntegrable_of_tendsto_Lp_zero hp hp' (fun n => (hf n).sub hg) hfg

Premises used: MeasureTheory.unifIntegrable_of_tendsto_Lp_zero, MeasureTheory.MemLp.sub
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = HAdd.hAdd (α := ℕ → α → β) (fun (x : ℕ) ↦ g) fun (n : ℕ) ↦ f n - g
⊢ UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ f n - g) p μ

Tactic:
exact unifIntegrable_of_tendsto_Lp_zero hp hp' (fun n => (hf n).sub hg) hfg

Premises used: MeasureTheory.unifIntegrable_of_tendsto_Lp_zero, MeasureTheory.MemLp.sub
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
tendsto_of_subseq_tendsto fun ns hns => ?_

Premises used: Filter.tendsto_of_subseq_tendsto
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
refine :
  ∀ (ns : ℕ → ℕ) (hns : Tendsto ns atTop atTop),
    ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_of_subseq_tendsto fun ns hns => ?_

Premises used: Filter.tendsto_of_subseq_tendsto
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
obtain :
  ∀ (ms : ℕ → ℕ),
    StrictMono ms →
      ∀ (hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ms i)) x) atTop (𝓝 (g x))),
        ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
⊢ ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns

Premises used: MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
⟨ms,
    tendsto_Lp_finite_of_tendsto_ae hp hp' (fun _ => hf _) hg (fun ε hε =>
      let ⟨δ, hδ, hδ'⟩ := hui hε
      ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
      hms'⟩

Premises used: Exists, Exists.intro, _private.0.MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure.match_1, MeasureTheory.tendsto_Lp_finite_of_tendsto_ae
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
exact ⟨ms,
    tendsto_Lp_finite_of_tendsto_ae hp hp' (fun _ => hf _) hg (fun ε hε =>
      let ⟨δ, hδ, hδ'⟩ := hui hε
      ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
      hms'⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
⊢ TendstoInMeasure μ f atTop g ∧ UnifIntegrable f p μ ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
⟨fun h => tendsto_Lp_finite_of_tendstoInMeasure hp hp' (fun n => (hf n).1) hg h.2 h.1, fun h =>
    ⟨tendstoInMeasure_of_tendsto_eLpNorm (lt_of_lt_of_le zero_lt_one hp).ne.symm
        (fun n => (hf n).aestronglyMeasurable) hg.aestronglyMeasurable h,
      unifIntegrable_of_tendsto_Lp hp hp' hf hg h⟩⟩

Premises used: MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm, Ne.symm, zero_lt_one, And.right, And.left, And.intro, Iff.intro, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure, lt_of_lt_of_le, LT.lt.ne, MeasureTheory.unifIntegrable_of_tendsto_Lp
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ p ≠ 0

Tactic:
have hpzero := (lt_of_lt_of_le zero_lt_one hp).ne.symm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
pos : ∀ (hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)), UnifIntegrable f p μ
neg : ∀ (hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)), UnifIntegrable f p μ
⊢ UnifIntegrable f p μ

Tactic:
by_cases hμ : μ Set.univ = 0

Premises used: Set.univ, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0

Tactic:
rw [Measure.measure_univ_eq_zero] at hμ

Premises used: MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : μ = 0
⊢ UnifIntegrable f p μ

Tactic:
hμ.symm ▸ unifIntegrable_zero_meas

Premises used: MeasureTheory.unifIntegrable_zero_meas, Eq.rec, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : μ = 0
⊢ UnifIntegrable f p μ

Tactic:
exact hμ.symm ▸ unifIntegrable_zero_meas
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
neg :
  ∀ (C : ℝ≥0) (hCpos : 0 < C)
    (hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨C, hCpos, hC⟩ := h (ε / 2) (half_pos hε)

Premises used: half_pos, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
⟨(ε / (2 * C)) ^ ENNReal.toReal p,
    Real.rpow_pos_of_pos (div_pos hε (mul_pos two_pos (NNReal.coe_pos.2 hCpos))) _,
    fun i s hs hμs => ?_⟩

Premises used: Iff.mpr, Real.rpow_pos_of_pos, HMul.hMul, two_pos, HDiv.hDiv, mul_pos, ENNReal.toReal, HPow.hPow, Exists.intro, NNReal.coe_pos, div_pos, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
neg :
  ∀ (i : ι) (s : Set α) (hs : MeasurableSet s)
    (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)),
    eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨(ε / (2 * C)) ^ ENNReal.toReal p,
    Real.rpow_pos_of_pos (div_pos hε (mul_pos two_pos (NNReal.coe_pos.2 hCpos))) _,
    fun i s hs hμs => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
pos :
  ∀ (hμs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
neg :
  ∀ (hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
by_cases hμs' : μ s = 0

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos : 0 ≤ ENNReal.ofReal ε
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
rw [(eLpNorm_eq_zero_iff ((hf i).indicator hs).aestronglyMeasurable hpzero).2
        (indicator_meas_zero hμs')]

Premises used: Iff.mpr, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.eLpNorm_eq_zero_iff, indicator_meas_zero, MeasureTheory.StronglyMeasurable.indicator
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 0 ≤ ENNReal.ofReal ε

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ eLpNorm (s.indicator (f i)) p μ ≤
    eLpNorm ((s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i)) p μ +
      eLpNorm ((s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)) p μ

Tactic:
le_trans (Eq.le ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (hs.inter (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (hs.inter ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const))))
        hp)

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.StronglyMeasurable.measurableSet_lt, MeasureTheory.StronglyMeasurable.measurableSet_le, Eq.le, MeasureTheory.StronglyMeasurable.indicator, MeasureTheory.StronglyMeasurable.nnnorm, MeasureTheory.eLpNorm_add_le, le_trans, MeasurableSet.inter