awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ bound n a
bound_integrable : Integrable (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
⊢ HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
have hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun (a : α) ↦ ∑' (n : ι), bound n a
Tactic: have hb_le_tsum : ∀ n, bound n ≤ᵐ[μ] fun a => ∑' n, bound n a := by
    intro n
    filter_upwards [hb_nonneg, bound_summable]
      with _ ha0 ha_sum using ha_sum.le_tsum _ fun i _ => ha0 i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ bound n a
bound_integrable : Integrable (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun (a : α) ↦ ∑' (n : ι), bound n a
⊢ ∀ (n : ι), Integrable (F n) μ
have refine : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ ∑' (n : ι), bound n a
Tactic: refine fun n => bound_integrable.mono' (hF_meas n) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ bound n a
bound_integrable : Integrable (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun (a : α) ↦ ∑' (n : ι), bound n a
⊢ HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
have hF_integrable : ∀ (n : ι), Integrable (F n) μ
Tactic: have hF_integrable : ∀ n, Integrable (F n) μ := by
    refine fun n => bound_integrable.mono' (hF_meas n) ?_
    exact EventuallyLE.trans (h_bound n) (hb_le_tsum n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ bound n a
bound_integrable : Integrable (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun (a : α) ↦ ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
⊢ HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
have simp : Tendsto.{u_4, u_3} (β := G) (fun (s : Finset ι) ↦ ∫ (a : α), ∑ i ∈ s, F i a ∂μ) (SummationFilter.unconditional ι).filter
  (𝓝 (∫ (a : α), f a ∂μ))
Tactic: simp only [HasSum, ← integral_finsetSum _ fun n _ => hF_integrable n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ bound n a
bound_integrable : Integrable (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun (a : α) ↦ ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
⊢ Tendsto.{u_4, u_3} (β := G) (fun (s : Finset ι) ↦ ∫ (a : α), ∑ i ∈ s, F i a ∂μ)
    (SummationFilter.unconditional ι).filter (𝓝 (∫ (a : α), f a ∂μ))
have refine_1 : ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
  AEStronglyMeasurable.{u_1, u_3} (β := G) (fun (a : α) ↦ ∑ i ∈ n, F i a) μ
Tactic: refine tendsto_integral_filter_of_dominated_convergence
      (fun a => ∑' n, bound n a) ?_ ?_ bound_integrable h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ bound n a
bound_integrable : Integrable (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun (a : α) ↦ ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
refine_1 :
  ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
    AEStronglyMeasurable.{u_1, u_3} (β := G) (fun (a : α) ↦ ∑ i ∈ n, F i a) μ
⊢ Tendsto.{u_4, u_3} (β := G) (fun (s : Finset ι) ↦ ∫ (a : α), ∑ i ∈ s, F i a ∂μ)
    (SummationFilter.unconditional ι).filter (𝓝 (∫ (a : α), f a ∂μ))
have refine_2 : ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
  ∀ᵐ (a : α) ∂μ, norm.{u_3} (E := G) (∑ i ∈ n, F i a) ≤ (fun (a : α) ↦ (∑' (n : ι), bound n a : ℝ)) a
Tactic: refine tendsto_integral_filter_of_dominated_convergence
      (fun a => ∑' n, bound n a) ?_ ?_ bound_integrable h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ bound n a
bound_integrable : Integrable (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun (a : α) ↦ ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
⊢ ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
    ∀ᵐ (a : α) ∂μ, norm.{u_3} (E := G) (∑ i ∈ n, F i a) ≤ (fun (a : α) ↦ (∑' (n : ι), bound n a : ℝ)) a
have refine_2 : ∀ (s : Finset ι), ∀ᵐ (a : α) ∂μ, norm.{u_3} (E := G) (∑ i ∈ s, F i a) ≤ ∑' (n : ι), bound n a
Tactic: filter_upwards with s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ bound n a
bound_integrable : Integrable (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun (n : ι) ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᶠ[ae μ] fun (a : α) ↦ ∑' (n : ι), bound n a
hF_integrable : ∀ (n : ι), Integrable (F n) μ
s : Finset ι
⊢ ∀ᵐ (a : α) ∂μ, norm.{u_3} (E := G) (∑ i ∈ s, F i a) ≤ ∑' (n : ι), bound n a
have h : ∀ (a : α) (hFa : ∀ (i : ι), ‖F i a‖ ≤ bound i a) (ha0 : ∀ (n : ι), 0 ≤ bound n a)
  (has : Summable (α := ℝ) fun (n : ι) ↦ bound n a), norm.{u_3} (E := G) (∑ i ∈ s, F i a) ≤ ∑' (n : ι), bound n a
Tactic: filter_upwards [eventually_countable_forall.2 h_bound, hb_nonneg, bound_summable]
      with a hFa ha0 has
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
have pos : ∀ (hG : CompleteSpace G), Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
pos :
  ∀ (hG : CompleteSpace G), Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
have neg : ∀ (hG : ¬CompleteSpace G), Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
have hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
Tactic: have hf'' i : AEMeasurable (‖f i ·‖ₑ) μ := (hf i).enorm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
⊢ ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
have hf'₁ : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
Tactic: rw [← lintegral_tsum hf''] at hf'
Cleared hypotheses: hf', hG, hf''
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
⊢ ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
have refine : ∀ (x : α), LT.lt (α := ℝ≥0∞) (∑' (i : ι), ‖f i x‖ₑ) ∞ → Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n x‖₊ : ℝ)
Tactic: refine (ae_lt_top' (AEMeasurable.tsum hf'') hf').mono ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∫⁻ (a : α), ∑' (i : ι), ‖f i a‖ₑ ∂μ ≠ ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
x : α
hx : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ‖f i x‖ₑ) ∞
⊢ Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n x‖₊ : ℝ)
have rw : Ne (α := ℝ≥0∞) (∑' (a : ι), (↑‖f a x‖₊ : ℝ≥0∞)) ∞
Tactic: rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
have hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
Tactic: have hhh : ∀ᵐ a : α ∂μ, Summable fun n => (‖f n a‖₊ : ℝ) := by
    rw [← lintegral_tsum hf''] at hf'
    refine (ae_lt_top' (AEMeasurable.tsum hf'') hf').mono ?_
    intro x hx
    rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]
    exact hx.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
have pos : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖f n a‖ ≤ (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a
Tactic: convert!
    (MeasureTheory.hasSum_integral_of_dominated_convergence (fun i a => ‖f i a‖₊) hf _ hhh ⟨_, _⟩
        _).tsum_eq.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
pos : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖f n a‖ ≤ (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
have pos₁ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ∑' (n : ι), (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a) μ
Tactic: convert!
    (MeasureTheory.hasSum_integral_of_dominated_convergence (fun i a => ‖f i a‖₊) hf _ hhh ⟨_, _⟩
        _).tsum_eq.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
pos : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖f n a‖ ≤ (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a
pos₁ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ∑' (n : ι), (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a) μ
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
have pos₂ : HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a) μ
Tactic: convert!
    (MeasureTheory.hasSum_integral_of_dominated_convergence (fun i a => ‖f i a‖₊) hf _ hhh ⟨_, _⟩
        _).tsum_eq.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
pos : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖f n a‖ ≤ (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a
pos₁ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ∑' (n : ι), (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a) μ
pos₂ : HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a) μ
⊢ Eq.{u_3 + 1} (α := G) (∫ (a : α), ∑' (i : ι), f i a ∂μ) (∑' (i : ι), ∫ (a : α), f i a ∂μ)
have pos₃ : ∀ᵐ (a : α) ∂μ, HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ f n a) (∑' (i : ι), f i a)
Tactic: convert!
    (MeasureTheory.hasSum_integral_of_dominated_convergence (fun i a => ‖f i a‖₊) hf _ hhh ⟨_, _⟩
        _).tsum_eq.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
n : ι
⊢ ∀ᵐ (a : α) ∂μ, ‖f n a‖ ≤ (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a
have pos : ∀ (x : α), ‖f n x‖ ≤ ‖f n x‖
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
⊢ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ∑' (n : ι), (fun (i : ι) (a : α) ↦ (↑‖f i a‖₊ : ℝ)) n a) μ
have pos : ∫⁻ (a : α), enorm (E := ℝ) (∑' (n : ι), ‖f n a‖) ∂μ < ∞
Tactic: dsimp [HasFiniteIntegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
⊢ ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
have rwa : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
Tactic: rwa [lintegral_tsum hf'', lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
⊢ ∫⁻ (a : α), enorm (E := ℝ) (∑' (n : ι), ‖f n a‖) ∂μ < ∞
have this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
Tactic: have : ∫⁻ a, ∑' n, ‖f n a‖ₑ ∂μ < ⊤ := by rwa [lintegral_tsum hf'', lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), enorm (E := ℝ) (∑' (n : ι), ‖f n a‖) ∂μ < ∞
have h : ∫⁻ (a : α), enorm (E := ℝ) (∑' (n : ι), ‖f n a‖) ∂μ = ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), enorm (E := ℝ) (∑' (n : ι), ‖f n a‖) ∂μ = ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ
have h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ enorm (E := ℝ) (∑' (n : ι), ‖f n a‖)) fun (a : α) ↦ ∑' (n : ι), ‖f n a‖ₑ
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ enorm (E := ℝ) (∑' (n : ι), ‖f n a‖)) fun (a : α) ↦
    ∑' (n : ι), ‖f n a‖ₑ
have h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (↑(∑' (a_1 : ι), ‖f a_1 a‖₊) : ℝ≥0∞)) fun (a : α) ↦
  ∑' (n : ι), (↑‖f n a‖₊ : ℝ≥0∞)
Tactic: simp_rw [← coe_nnnorm, ← NNReal.coe_tsum, enorm_eq_nnnorm, NNReal.nnnorm_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (↑(∑' (a_1 : ι), ‖f a_1 a‖₊) : ℝ≥0∞)) fun (a : α) ↦
    ∑' (n : ι), (↑‖f n a‖₊ : ℝ≥0∞)
have h : ∀ (a : α) (ha : Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)),
  (↑(∑' (a_1 : ι), ‖f a_1 a‖₊) : ℝ≥0∞) = ∑' (n : ι), (↑‖f n a‖₊ : ℝ≥0∞)
Tactic: filter_upwards [hhh] with a ha