case pos
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ

case neg
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
by_cases h : IntegrableOn f t μ
case neg
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ

case pos
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
case pos
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ

case neg
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
swap
case pos
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
case pos
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
let f' := h.1.mk f
no goals
case pos
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
calc
  (∫ x in t, f x ∂μ) = ∫ x in t, f' x ∂μ := integral_congr_ae h.1.ae_eq_mk
  _ = ∫ x in s, f' x ∂μ := by
    apply
      set_integral_eq_of_subset_of_ae_diff_eq_zero_aux hts _ h.1.stronglyMeasurable_mk
        (h.congr h.1.ae_eq_mk)
    filter_upwards [h't, ae_imp_of_ae_restrict h.1.ae_eq_mk] with x hx h'x h''x
    rw [← h'x h''x.1, hx h''x]
  _ = ∫ x in s, f x ∂μ := by
    apply integral_congr_ae
    apply ae_restrict_of_ae_restrict_of_subset hts
    exact h.1.ae_eq_mk.symm
case neg
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t
this : ¬IntegrableOn f s
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
case neg
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
have : ¬IntegrableOn f s μ := fun H => h (H.of_ae_diff_eq_zero ht h't)
no goals
case neg
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t
this : ¬IntegrableOn f s
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
rw [integral_undef h, integral_undef this]
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t \ s → AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t)) x = 0
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ (∫ (x : α) in t, f' x ∂μ) = ∫ (x : α) in s, f' x ∂μ
apply
  set_integral_eq_of_subset_of_ae_diff_eq_zero_aux hts _ h.1.stronglyMeasurable_mk
    (h.congr h.1.ae_eq_mk)
case h
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
x : α
hx : x ∈ t \ s → f x = 0
h'x : x ∈ t → f x = AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t)) x
h''x : x ∈ t \ s
⊢ AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t)) x = 0
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t \ s → AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t)) x = 0
filter_upwards [h't, ae_imp_of_ae_restrict h.1.ae_eq_mk] with x hx h'x h''x
no goals
case h
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
x : α
hx : x ∈ t \ s → f x = 0
h'x : x ∈ t → f x = AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t)) x
h''x : x ∈ t \ s
⊢ AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t)) x = 0
rw [← h'x h''x.1, hx h''x]
case h
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ (fun a => f' a) =ᵐ[Measure.restrict μ s] fun a => f a
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ (∫ (x : α) in s, f' x ∂μ) = ∫ (x : α) in s, f x ∂μ
apply integral_congr_ae
case h
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ t, (fun a => f' a) x = (fun a => f a) x
case h
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ (fun a => f' a) =ᵐ[Measure.restrict μ s] fun a => f a
apply ae_restrict_of_ae_restrict_of_subset hts
no goals
case h
α : Type u_1
β : Type ?u.95878
E : Type u_2
F : Type ?u.95884
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : NullMeasurableSet t
hts : s ⊆ t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t
f' : α → E := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f (Measure.restrict μ t))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ t, (fun a => f' a) x = (fun a => f a) x
exact h.1.ae_eq_mk.symm