-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem uniformIntegrable_average
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (hp : 1 ≤ p) {f : ℕ → α → E} (hf : UniformIntegrable f p μ) :
    UniformIntegrable (fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i ∈ Finset.range n, f i)) p μ

Proof state:
case intro.intro.refine_2.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (∑ i ∈ Finset.range n, s.indicator ((↑n)⁻¹ • f i)) p μ ≤ ENNReal.ofReal ε

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

Result:
case intro.intro.refine_2.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator ((↑n)⁻¹ • f i)) p μ ≤ ENNReal.ofReal ε

Proof state:
case intro.intro.refine_3.intro.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
hn : n ≠ 0
⊢ ‖(↑n)⁻¹‖ₑ * ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ ↑C

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

Result:
case intro.intro.refine_3.intro.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
hn : n ≠ 0
⊢ (∑ i ∈ Finset.range n, eLpNorm (f i) p μ) / ↑n ≤ ↑C

Proof state:
case intro.intro.refine_3.intro.inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
⊢ ∑ i ∈ Finset.range 0, eLpNorm ((↑0)⁻¹ • f i) p μ ≤ ↑C

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
this : ∀ (i : ℕ), s.indicator ((↑n)⁻¹ • f i) = (↑n)⁻¹ • s.indicator (f i)
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.refine_3.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
⊢ ∑ i ∈ Finset.range n, eLpNorm ((↑n)⁻¹ • f i) p μ ≤ ↑C

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case intro.intro.refine_3.intro.inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
⊢ ∑ i ∈ Finset.range 0, eLpNorm ((↑0)⁻¹ • f i) p μ ≤ ↑C

case intro.intro.refine_3.intro.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm ((↑n)⁻¹ • f i) p μ ≤ ↑C

Proof state:
case intro.intro.refine_3.intro.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
hn : n ≠ 0
⊢ (∑ i ∈ Finset.range n, eLpNorm (f i) p μ) / ↑n ≤ ↑C

Tactic:
refine ENNReal.div_le_of_le_mul' ?_

Result:
case intro.intro.refine_3.intro.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ ↑n * ↑C

Proof state:
case intro.intro.refine_2.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator ((↑n)⁻¹ • f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
have this i : s.indicator ((n : ℝ) ⁻¹ • f i) = (↑n : ℝ)⁻¹ • s.indicator (f i) :=
  indicator_const_smul _ _ _

Result:
case intro.intro.refine_2.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
this : ∀ (i : ℕ), s.indicator ((↑n)⁻¹ • f i) = (↑n)⁻¹ • s.indicator (f i)
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator ((↑n)⁻¹ • f i)) p μ ≤ ENNReal.ofReal ε