α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
have ht : IntegrableOn f t μ := by apply integrableOn_zero.congr_fun_ae; symm; exact ht_eq
case pos
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ

case neg
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : ¬IntegrableOn f (s ∪ t)
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
by_cases H : IntegrableOn f (s ∪ t) μ
case neg
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : ¬IntegrableOn f (s ∪ t)
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ

case pos
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
case pos
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ

case neg
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : ¬IntegrableOn f (s ∪ t)
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
swap
case pos
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t)))
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
case pos
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
let f' := H.1.mk f
no goals
case pos
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t)))
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
calc
  (∫ x : α in s ∪ t, f x ∂μ) = ∫ x : α in s ∪ t, f' x ∂μ := integral_congr_ae H.1.ae_eq_mk
  _ = ∫ x in s, f' x ∂μ := by
    apply
      integral_union_eq_left_of_ae_aux _ H.1.stronglyMeasurable_mk (H.congr_fun_ae H.1.ae_eq_mk)
    filter_upwards [ht_eq,
      ae_mono (Measure.restrict_mono (subset_union_right s t) le_rfl) H.1.ae_eq_mk] with x hx h'x
    rw [← h'x, hx]
  _ = ∫ x in s, f x ∂μ :=
    integral_congr_ae
      (ae_mono (Measure.restrict_mono (subset_union_left s t) le_rfl) H.1.ae_eq_mk.symm)
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
⊢ (fun x => 0) =ᵐ[Measure.restrict μ t] f
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
⊢ IntegrableOn f t
apply integrableOn_zero.congr_fun_ae
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
⊢ f =ᵐ[Measure.restrict μ t] fun x => 0
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
⊢ (fun x => 0) =ᵐ[Measure.restrict μ t] f
symm
no goals
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
⊢ f =ᵐ[Measure.restrict μ t] fun x => 0
exact ht_eq
case neg
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : ¬IntegrableOn f (s ∪ t)
⊢ ¬Integrable fun x => f x
case neg
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : ¬IntegrableOn f (s ∪ t)
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
rw [integral_undef H, integral_undef]
no goals
case neg
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : ¬IntegrableOn f (s ∪ t)
⊢ ¬Integrable fun x => f x
simpa [integrableOn_union, ht] using H
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t)))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ t,
    AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t))) x = 0
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t)))
⊢ (∫ (x : α) in s ∪ t, f' x ∂μ) = ∫ (x : α) in s, f' x ∂μ
apply
  integral_union_eq_left_of_ae_aux _ H.1.stronglyMeasurable_mk (H.congr_fun_ae H.1.ae_eq_mk)
case h
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t)))
x : α
hx : f x = 0
h'x : f x = AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t))) x
⊢ AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t))) x = 0
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t)))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ t,
    AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t))) x = 0
filter_upwards [ht_eq,
  ae_mono (Measure.restrict_mono (subset_union_right s t) le_rfl) H.1.ae_eq_mk] with x hx h'x
no goals
case h
α : Type u_1
β : Type ?u.82166
E : Type u_2
F : Type ?u.82172
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
ht : IntegrableOn f t
H : IntegrableOn f (s ∪ t)
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t)))
x : α
hx : f x = 0
h'x : f x = AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t))) x
⊢ AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ (s ∪ t))) x = 0
rw [← h'x, hx]