mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : 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 = ∫⁻ (x : X), ENNReal.ofReal ‖f x‖ ∂μ i

pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
⊢ 0 ≤ᵐ[μ i] fun a ↦ ‖f a‖

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : 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 = ∫⁻ (x : X), ENNReal.ofReal ‖f x‖ ∂μ i

ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
⊢ 0 ≤ᵐ[μ i] fun a ↦ ‖f a‖
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : 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 = ∫ (a : X), ‖f a‖ₑ.toReal ∂μ i

pp: ι : 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 : ι
⊢ AEMeasurable (fun x ↦ ‖f x‖ₑ) (μ i)

Tactic:
]

Goal state after:
ι : 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 = ∫ (a : X), ‖f a‖ₑ.toReal ∂μ i

ι : 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 : ι
⊢ AEMeasurable (fun x ↦ ‖f x‖ₑ) (μ i)
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : 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 μ)
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂Measure.sum μ ≠ ∞

Tactic:
]

Goal state after:
ι : 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 μ)
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂Measure.sum μ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
⊢ Tendsto (fun i ↦ (f' i a).toReal + f 0 a) atTop (𝓝 ((F' a).toReal + f 0 a))

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
⊢ Tendsto (fun i ↦ (f' i a).toReal + f 0 a) atTop (𝓝 ((F' a).toReal + f 0 a))
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : 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 + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (x : X), f x ∂∑ i ∈ s, μ i) (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) < ↑ε

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : 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 + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (x : X), f x ∂∑ i ∈ s, μ i) (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) < ↑ε
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
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 + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (x : X), f x ∂∑ i ∈ s, μ i) (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) < ↑ε

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
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 + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (x : X), f x ∂∑ i ∈ s, μ i) (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) < ↑ε
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
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 + ↑ε
s : Finset ι
ν : Measure X
hs : ∑ i ∈ s, ∫⁻ (a : X), ‖f a‖ₑ ∂μ i + ∫⁻ (a : X), ‖f a‖ₑ ∂ν < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂ν < ↑ε

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
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 + ↑ε
s : Finset ι
ν : Measure X
hs : ∑ i ∈ s, ∫⁻ (a : X), ‖f a‖ₑ ∂μ i + ∫⁻ (a : X), ‖f a‖ₑ ∂ν < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂ν < ↑ε
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: case pos
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ ∑' (i : ι), ∫ (x : X), f x ∂c i • Measure.dirac (x i) = ∑' (i : ι), (c i).toReal • f (x i)

Tactic:
]

Goal state after:
case pos
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ ∑' (i : ι), ∫ (x : X), f x ∂c i • Measure.dirac (x i) = ∑' (i : ι), (c i).toReal • f (x i)
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: case pos.e_f
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
i : ι
⊢ (c i).toReal • f (x i) = (c i).toReal • f (x i)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : ¬Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ 0 = 0

pp: case neg
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : ¬Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ ¬Summable fun i ↦ (c i).toReal • f (x i)

Tactic:
]

Goal state after:
case neg
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : ¬Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ ¬Summable fun i ↦ (c i).toReal • f (x i)
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
⊢ ∫ (x : X), f x ∂μ = ∑' (x : X), μ.real {x} • f x

Tactic:
]

Goal state after:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
⊢ ∫ (x : X), f x ∂μ = ∑' (x : X), μ.real {x} • f x
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
⊢ ∑' (i : X), ∫ (x : X), f x ∂μ {i} • Measure.dirac i =
    ∑' (x : X), (Measure.sum fun a ↦ μ {a} • Measure.dirac a).real {x} • f x

Tactic:
]

Goal state after:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
⊢ ∑' (i : X), ∫ (x : X), f x ∂μ {i} • Measure.dirac i =
    ∑' (x : X), (Measure.sum fun a ↦ μ {a} • Measure.dirac a).real {x} • f x
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: case e_f
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
a : X
⊢ (μ {a}).toReal • f a = (μ {a}).toReal • f a

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)

pp: case hg
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEStronglyMeasurable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))

pp: case hf
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEMeasurable Subtype.val (Measure.comap Subtype.val μ)

pp: case hs
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ MeasurableSet s

Tactic:
]

Goal state after:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)

case hg
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEStronglyMeasurable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))

case hf
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEMeasurable Subtype.val (Measure.comap Subtype.val μ)

case hs
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = 0
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = 0
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)
⊢ ∑' (x : ↑s), (Measure.comap Subtype.val μ).real {x} • f ↑x = ∑' (x : ↑s), μ.real {↑x} • f ↑x

Tactic:
]

Goal state after:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)
⊢ ∑' (x : ↑s), (Measure.comap Subtype.val μ).real {x} • f ↑x = ∑' (x : ↑s), μ.real {↑x} • f ↑x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
x✝ : ℕ
⊢ -∫ (a : α), f x✝ a ∂μ = -∫ (a : α), f x✝ a ∂μ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
hF : CompleteSpace F
⊢ (L1.setToL1 hT) (Integrable.toL1 f ?pos.hf✝) + (L1.setToL1 hT) (Integrable.toL1 g ?pos.hg✝) =
    (L1.setToL1 hT) (Integrable.toL1 f hf) + (L1.setToL1 hT) (Integrable.toL1 g hg)

pp: case pos.hf
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
hF : CompleteSpace F
⊢ Integrable f μ

pp: case pos.hg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
hF : CompleteSpace F
⊢ Integrable g μ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: case e_f
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)
a : ↑s
⊢ (μ (Subtype.val '' {a})).toReal • f ↑a = μ.real {↑a} • f ↑a

Tactic:
]

Goal state after:
case e_f
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)
a : ↑s
⊢ (μ (Subtype.val '' {a})).toReal • f ↑a = μ.real {↑a} • f ↑a
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case e'_5
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
⊢ -∫ (a : α), F a ∂μ = -∫ (a : α), F a ∂μ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
s : Finset X
hf : IntegrableOn f (↑s) μ
⊢ ∑' (x : ↑↑s), μ.real {↑x} • f ↑x = ∑' (x : ↑↑s), μ.real {↑x} • f ↑x

Tactic:
]

Goal state after: