α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
let k := f ⁻¹' {0}
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
have h's : IntegrableOn f s μ := H.mono (subset_union_left _ _) le_rfl
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
have A : ∀ u : Set α, (∫ x in u ∩ k, f x ∂μ) = 0 := fun u =>
  set_integral_eq_zero_of_forall_eq_zero fun x hx => hx.2
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ (∫ (x : α) in t \ k ∪ s \ k, f x ∂μ) = ∫ (x : α) in s \ k, f x ∂μ
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
rw [← integral_inter_add_diff hk h's, ← integral_inter_add_diff hk H, A, A, zero_add, zero_add,
  union_diff_distrib, union_comm]
case hst
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ t \ k ∪ s \ k =ᵐ[μ] s \ k
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ (∫ (x : α) in t \ k ∪ s \ k, f x ∂μ) = ∫ (x : α) in s \ k, f x ∂μ
apply set_integral_congr_set_ae
case hst
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ ↑↑μ ((t \ k) \ (s \ k)) = 0
case hst
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ t \ k ∪ s \ k =ᵐ[μ] s \ k
rw [union_ae_eq_right]
case hst
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ ↑↑μ (t \ k) = 0
case hst
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ ↑↑μ ((t \ k) \ (s \ k)) = 0
apply measure_mono_null (diff_subset _ _)
case hst
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ ∀ᵐ (a : α) ∂μ, ¬a ∈ t \ k
case hst
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ ↑↑μ (t \ k) = 0
rw [measure_zero_iff_ae_nmem]
no goals
case hst
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s
A : ∀ (u : Set α), (∫ (x : α) in u ∩ k, f x ∂μ) = 0
⊢ ∀ᵐ (a : α) ∂μ, ¬a ∈ t \ k
filter_upwards [ae_imp_of_ae_restrict ht_eq] with x hx h'x using h'x.2 (hx h'x.1)
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MeasurableSet k
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
⊢ MeasurableSet k
borelize E
no goals
α : Type u_1
β : Type ?u.77763
E : Type u_2
F : Type ?u.77769
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t)
k : Set α := f ⁻¹' {0}
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MeasurableSet k
exact haux.measurable (measurableSet_singleton _)