awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
pos : ∀ (hfx : C ≤ ‖f i x‖₊), Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
pos₁ pos₂ pos₃ pos₄ :
  ∀ (hfx : C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊),
    Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
⊢ Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x

Tactic:
rwa [Set.mem_setOf, hx] at hfx

Premises used: Set.mem_setOf
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
neg : x ∉ {x : α | C ≤ ‖g i x‖₊}
⊢ indicator {x : α | C ≤ ‖f i x‖₊} (f i) x = indicator {x : α | C ≤ ‖g i x‖₊} (g i) x

Tactic:
rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]

Premises used: Set.indicator_of_notMem
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
neg : ∀ (hfx : ¬C ≤ ‖f i x‖₊), x ∉ {x : α | C ≤ ‖g i x‖₊}
neg₁ neg₂ neg₃ neg₄ :
  ∀ (hfx : ¬C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x‖₊),
    x ∉ {x : α | C ≤ ‖g i x‖₊}
⊢ x ∉ {x : α | C ≤ ‖g i x‖₊}

Tactic:
rwa [Set.mem_setOf, hx] at hfx

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

Tactic:
⟨fun h => ⟨h.1, fun _ => h.spec (lt_of_lt_of_le zero_lt_one hp).ne.symm hp'⟩,
    fun h => uniformIntegrable_of hp hp' h.1 h.2⟩

Premises used: Ne.symm, MeasureTheory.uniformIntegrable_of, zero_lt_one, And.right, And.left, And.intro, Iff.intro, MeasureTheory.UniformIntegrable.spec, lt_of_lt_of_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf : UniformIntegrable f p μ
⊢ ∀ (i : ℕ), AEStronglyMeasurable (f i) μ

Tactic:
obtain ⟨hf₁, hf₂, hf₃⟩ := hf
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf : UniformIntegrable f p μ
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
⊢ UnifIntegrable f p μ

Tactic:
obtain ⟨hf₁, hf₂, hf₃⟩ := hf
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf : UniformIntegrable f p μ
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
⊢ ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)

Tactic:
obtain ⟨hf₁, hf₂, hf₃⟩ := hf
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ UniformIntegrable.{u_1, u_4, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) p μ

Tactic:
⟨fun n => ?_, fun ε hε => ?_, ?_⟩

Premises used: MeasureTheory.UniformIntegrable, And.intro
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
refine_1 :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_4} (β := E)
      ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n) μ
refine_2 :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ℕ) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
            eLpNorm.{u_1, u_4} (ε := E)
                (s.indicator
                  ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
                p μ ≤
              ENNReal.ofReal ε
refine_3 :
  ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E)
          ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i) p μ ≤
        (↑C : ℝ≥0∞)
⊢ UniformIntegrable.{u_1, u_4, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) p μ

Tactic:
refine ⟨fun n => ?_, fun ε hε => ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
⊢ AEStronglyMeasurable.{u_1, u_4} (β := E)
    ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n) μ

Tactic:
(Finset.aestronglyMeasurable_sum _ fun i _ => hf₁ i).const_smul _

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul, Finset.aestronglyMeasurable_sum
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
⊢ AEStronglyMeasurable.{u_1, u_4} (β := E)
    ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n) μ

Tactic:
exact (Finset.aestronglyMeasurable_sum _ fun i _ => hf₁ i).const_smul _

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul, Finset.aestronglyMeasurable_sum
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
refine_2 :
  ∀ (δ : ℝ) (hδ₁ : 0 < δ)
    (hδ₂ :
      ∀ (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.{u_1, u_4} (ε := E)
                (s.indicator
                  ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
                p μ ≤
              ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_4} (ε := E)
              (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
              p μ ≤
            ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδ₁, hδ₂⟩ := hf₂ hε
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (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.{u_1, u_4} (ε := E)
              (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
              p μ ≤
            ENNReal.ofReal ε

Tactic:
⟨δ, hδ₁, fun n s hs hle => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
refine_2 :
  ∀ (n : ℕ) (s : Set α) (hs : MeasurableSet s) (hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
    eLpNorm.{u_1, u_4} (ε := E)
        (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n)) p μ ≤
      ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_4} (ε := E)
              (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
              p μ ≤
            ENNReal.ofReal ε

Tactic:
refine ⟨δ, hδ₁, fun n s hs hle => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
refine_2 :
  eLpNorm.{u_1, u_4} (ε := E) (∑ i ∈ Finset.range n, s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤
    ENNReal.ofReal ε
⊢ eLpNorm.{u_1, u_4} (ε := E)
      (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n)) p μ ≤
    ENNReal.ofReal ε

Tactic:
simp_rw [Finset.smul_sum, Finset.indicator_sum]

Premises used: Finset.indicator_sum, Finset.smul_sum
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm.{u_1, u_4} (ε := E) (∑ i ∈ Finset.range n, s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤
    ENNReal.ofReal ε

Tactic:
le_trans (eLpNorm_sum_le (fun i _ => ((hf₁ i).const_smul _).indicator hs) hp) ?_

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul, Nat.cast, Inv.inv, MeasureTheory.AEStronglyMeasurable.indicator, MeasureTheory.eLpNorm_sum_le, le_trans
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
refine_2 : ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm.{u_1, u_4} (ε := E) (∑ i ∈ Finset.range n, s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤
    ENNReal.ofReal ε

Tactic:
refine le_trans (eLpNorm_sum_le (fun i _ => ((hf₁ i).const_smul _).indicator hs) hp) ?_

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul, MeasureTheory.AEStronglyMeasurable.indicator, MeasureTheory.eLpNorm_sum_le, le_trans
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))

Tactic:
have this i : s.indicator ((n : ℝ)⁻¹ • f i) = (↑n : ℝ)⁻¹ • s.indicator (f i) :=
      indicator_const_smul _ _ _
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
refine_2 :
  ∀
    (this :
      ∀ (i : ℕ),
        s.indicator (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.indicator (f i))),
    ∑ i ∈ Finset.range 0, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
refine_2₁ :
  ∀ (hn : n ≠ 0),
    ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.indicator (f i))
⊢ ∑ i ∈ Finset.range 0, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
hn : n ≠ 0
refine_2 : enorm (E := ℝ) (↑n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε

Tactic:
simp_rw [this, eLpNorm_const_smul, ← Finset.mul_sum]

Premises used: Finset.mul_sum, MeasureTheory.eLpNorm_const_smul
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
hn : n ≠ 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
hn : n ≠ 0
refine_2 : HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ) (↑n : ℝ≥0∞) ≤ ENNReal.ofReal ε
⊢ enorm (E := ℝ) (↑n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
rw [enorm_inv (by positivity), Real.enorm_natCast, ← ENNReal.div_eq_inv_mul]

Premises used: Real.enorm_natCast, enorm_inv, ENNReal.div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
hn : n ≠ 0
⊢ HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ) (↑n : ℝ≥0∞) ≤ ENNReal.ofReal ε

Tactic:
ENNReal.div_le_of_le_mul' ?_

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
hn : n ≠ 0
refine_2 : ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ (↑n : ℝ≥0∞) * ENNReal.ofReal ε
⊢ HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ) (↑n : ℝ≥0∞) ≤ ENNReal.ofReal ε

Tactic:
refine ENNReal.div_le_of_le_mul' ?_

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ (↑n : ℝ≥0∞) * ENNReal.ofReal ε

Tactic:
simpa using Finset.sum_le_card_nsmul (.range n) _ _ fun i _ => hδ₂ _ _ hs hle

Premises used: Finset.range, Finset.sum_le_card_nsmul