awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∈ k
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ
have hv₁ : ‖f p y - f q y‖ < δ
Tactic: specialize hv p hp y hy
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∈ k
hv : ‖f p y - f q y‖ < δ
⊢ ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ ≤ ‖L‖ * ‖g y‖ * δ
have ha : 0 ≤ ‖L‖ * ‖g y‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∈ k
hv : ‖f p y - f q y‖ < δ
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ
have p₁ : ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
      ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ =
  norm.{u_3} (E := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y - f q y) : E)
Tactic: calc
          ‖L (g y) (f p y) - L (g y) (f q y)‖
            = ‖L (g y) (f p y - f q y)‖ := by simp only [map_sub]
          _ ≤ ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ := le_opNorm₂ _ _ _
          _ ≤ ‖L‖ * ‖g y‖ * δ := by gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∈ k
hv : ‖f p y - f q y‖ < δ
p₁ :
  ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ =
    norm.{u_3} (E := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y - f q y) : E)
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ
have p₂ : ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ ≤ ‖L‖ * ‖g y‖ * δ
Tactic: calc
          ‖L (g y) (f p y) - L (g y) (f q y)‖
            = ‖L (g y) (f p y - f q y)‖ := by simp only [map_sub]
          _ ≤ ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ := le_opNorm₂ _ _ _
          _ ≤ ‖L‖ * ‖g y‖ * δ := by gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∉ k
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ
have neg : 0 ≤ ‖L‖ * ‖g y‖ * δ
Tactic: simp only [hfs p y h'p hy, hfs q y hq hy, sub_self, norm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ ‖HSub.hSub (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) ∂μ)
        (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ)‖ <
    ε
have L₁ : ‖HSub.hSub (α := E) (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
      (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖ =
  ‖HSub.hSub (α := E) (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
      (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖
Tactic: calc
  ‖∫ x, L (g x) (f p x) ∂μ - ∫ x, L (g x) (f q x) ∂μ‖
    = ‖∫ x in k, L (g x) (f p x) ∂μ - ∫ x in k, L (g x) (f q x) ∂μ‖ := by
      congr 2
      · refine (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
        simp [hfs p y h'p hy]
      · refine (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
        simp [hfs q y hq hy]
  _ = ‖∫ x in k, L (g x) (f p x) - L (g x) (f q x) ∂μ‖ := by rw [integral_sub (I p h'p) (I q hq)]
  _ ≤ ∫ x in k, ‖L (g x) (f p x) - L (g x) (f q x)‖ ∂μ := norm_integral_le_integral_norm _
  _ ≤ ∫ x in k, ‖L‖ * ‖g x‖ * δ ∂μ := by
      apply integral_mono_of_nonneg (Eventually.of_forall (fun y ↦ by positivity))
      · exact (hg.norm.const_mul _).mul_const _
      · filter_upwards with y
        by_cases hy : y ∈ k
        · dsimp only
          specialize hv p hp y hy
          calc
          ‖L (g y) (f p y) - L (g y) (f q y)‖
            = ‖L (g y) (f p y - f q y)‖ := by simp only [map_sub]
          _ ≤ ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ := le_opNorm₂ _ _ _
          _ ≤ ‖L‖ * ‖g y‖ * δ := by gcongr
        · simp only [hfs p y h'p hy, hfs q y hq hy, sub_self, norm_zero]
          positivity
  _ < ε := hδ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ Integrable f (Measure.sum μ)
have refine : HasFiniteIntegral f (Measure.sum μ)
Tactic: refine ⟨aestronglyMeasurable_sum_measure_iff.mpr fun i ↦ (hf i).aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ HasFiniteIntegral f (Measure.sum μ)
have rw : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) ∞
Tactic: rw [HasFiniteIntegral, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) ∞
have h₁ : ∀ (i : ι), ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ENNReal.ofReal (∫ (x : X), ‖f x‖ ∂μ i)
Tactic: convert! h.tsum_ofReal_lt_top with i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ENNReal.ofReal (∫ (x : X), ‖f x‖ ∂μ i)
have h₁ : ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ∫⁻ (x : X), ENNReal.ofReal ‖f x‖ ∂μ i
Tactic: rw [ofReal_integral_eq_lintegral_ofReal (hf i).norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
h₁ : ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ∫⁻ (x : X), ENNReal.ofReal ‖f x‖ ∂μ i
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ENNReal.ofReal (∫ (x : X), ‖f x‖ ∂μ i)
have h₂ : (ae (μ i)).EventuallyLE (β := ℝ) 0 fun (a : X) ↦ ‖f a‖
Tactic: rw [ofReal_integral_eq_lintegral_ofReal (hf i).norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
⊢ Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
have h : ∀ (i : ι), ∫ (x : X), ‖f x‖ ∂μ i = (∫⁻ (x : X), ‖f x‖ₑ ∂μ i).toReal
Tactic: convert! ENNReal.summable_toReal (f := fun i ↦ ∫⁻ x, ‖f x‖ₑ ∂μ i) ?_ with i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
h : ∀ (i : ι), ∫ (x : X), ‖f x‖ ∂μ i = (∫⁻ (x : X), ‖f x‖ₑ ∂μ i).toReal
⊢ Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
have convert! : Ne (α := ℝ≥0∞) (∑' (x : ι), (fun (i : ι) ↦ ∫⁻ (x : X), ‖f x‖ₑ ∂μ i) x) ∞
Tactic: convert! ENNReal.summable_toReal (f := fun i ↦ ∫⁻ x, ‖f x‖ₑ ∂μ i) ?_ with i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ ∫ (x : X), ‖f x‖ ∂μ i = (∫⁻ (x : X), ‖f x‖ₑ ∂μ i).toReal
have h : Eq (α := ℝ) (∫ (x : X), ‖f x‖ ∂μ i) (∫ (a : X), ‖f a‖ₑ.toReal ∂μ i)
Tactic: rw [← integral_toReal ?_ (by simp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
h : Eq (α := ℝ) (∫ (x : X), ‖f x‖ ∂μ i) (∫ (a : X), ‖f a‖ₑ.toReal ∂μ i)
⊢ ∫ (x : X), ‖f x‖ ∂μ i = (∫⁻ (x : X), ‖f x‖ₑ ∂μ i).toReal
have rw : AEMeasurable (β := ℝ≥0∞) (fun (x : X) ↦ ‖f x‖ₑ) (μ i)
Tactic: rw [← integral_toReal ?_ (by simp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
⊢ Ne (α := ℝ≥0∞) (∑' (x : ι), (fun (i : ι) ↦ ∫⁻ (x : X), ‖f x‖ₑ ∂μ i) x) ∞
have rw : ∫⁻ (a : X), ‖f a‖ₑ ∂Measure.sum μ ≠ ∞
Tactic: rw [← lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
⊢ HasSum.{u_3, u_1} (α := E) (fun (i : ι) ↦ ∫ (x : X), f x ∂μ i) (∫ (x : X), f x ∂Measure.sum μ)
have hfi : ∀ (i : ι), Integrable f (μ i)
Tactic: have hfi : ∀ i, Integrable f (μ i) := fun i ↦ hf.mono_measure (Measure.le_sum _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
⊢ HasSum.{u_3, u_1} (α := E) (fun (i : ι) ↦ ∫ (x : X), f x ∂μ i) (∫ (x : X), f x ∂Measure.sum μ)
have simp : Tendsto.{u_1, u_3} (β := E) (fun (s : Finset ι) ↦ @integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
  (SummationFilter.unconditional ι).filter (𝓝 (∫ (x : X), f x ∂Measure.sum μ))
Tactic: simp only [HasSum, ← integral_finsetSum_measure fun i _ ↦ hfi i]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
⊢ Tendsto.{u_1, u_3} (β := E) (fun (s : Finset ι) ↦ @integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
    (SummationFilter.unconditional ι).filter (𝓝 (∫ (x : X), f x ∂Measure.sum μ))
have refine : ∀ (ε : ℝ) (ε0 : 0 < ε),
  ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) ε)
      (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)
Tactic: refine Metric.nhds_basis_ball.tendsto_right_iff.mpr fun ε ε0 ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) ε)
      (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)
have lift : ∀ (ε : ℝ≥0) (ε0 : 0 < (↑ε : ℝ)),
  ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
      (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)
Tactic: lift ε to ℝ≥0 using ε0.le
Cleared hypotheses: ε, ε0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
⊢ ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
      (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)
have hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
Tactic: have hf_lt : (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < ∞ := hf.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
⊢ ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
have refine_1 : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ ≠ ∞
Tactic: refine tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
refine_1 : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ ≠ ∞
⊢ ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
have refine_2 : (↑ε : ℝ≥0∞) ≠ 0
Tactic: refine tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
⊢ ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
      (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)
have hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
Tactic: have hmem : ∀ᶠ y in 𝓝 (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ), (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < y + ε := by
    refine tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right ?_ ?_)
    exacts [hf_lt.ne, ENNReal.coe_ne_zero.2 (NNReal.coe_ne_zero.1 ε0.ne')]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
⊢ ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
      (@integral _ _ _ _ mX (∑ i ∈ x, μ i) fun (x : X) ↦ f x)
have refine : ∀ (s : Finset ι)
  (hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)),
  Membership.mem (γ := Set E) (Metric.ball (∫ (x : X), f x ∂Measure.sum μ) (↑ε : ℝ))
    (@integral _ _ _ _ mX (∑ i ∈ s, μ i) fun (x : X) ↦ f x)
Tactic: refine ((hasSum_lintegral_measure (fun x ↦ ‖f x‖ₑ) μ).eventually hmem).mono fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (goal)
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst_1 : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + (↑ε : ℝ≥0∞)
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun (i : ι) ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + (↑ε : ℝ≥0∞)
⊢ ∃ (ν : Measure X), ∑ i ∈ s, μ i + ν = Measure.sum μ
have refine : HAdd.hAdd (α := Measure X) (∑ i ∈ s, μ i) (Measure.sum fun (i : (↑(↑s : Set ι)ᶜ : Type u_1)) ↦ μ (↑i : ι)) =
  Measure.sum μ
Tactic: refine ⟨Measure.sum fun i : ↥(sᶜ : Set ι) ↦ μ i, ?_⟩