case pos
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (∫ (x : α) in t, f x ∂μ) = 0

case neg
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (∫ (x : α) in t, f x ∂μ) = 0
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
⊢ (∫ (x : α) in t, f x ∂μ) = 0
by_cases hf : AEStronglyMeasurable f (μ.restrict t)
case neg
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (∫ (x : α) in t, f x ∂μ) = 0

case pos
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (∫ (x : α) in t, f x ∂μ) = 0
case pos
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (∫ (x : α) in t, f x ∂μ) = 0

case neg
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (∫ (x : α) in t, f x ∂μ) = 0
swap
case pos
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
this : (∫ (x : α) in t, AEStronglyMeasurable.mk f hf x ∂μ) = 0
⊢ (∫ (x : α) in t, f x ∂μ) = 0
case pos
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (∫ (x : α) in t, f x ∂μ) = 0
have : (∫ x in t, hf.mk f x ∂μ) = 0 := by
  refine' integral_eq_zero_of_ae _
  rw [EventuallyEq,
    ae_restrict_iff (hf.stronglyMeasurable_mk.measurableSet_eq_fun stronglyMeasurable_zero)]
  filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x
  rw [← hx h''x]
  exact h'x h''x
case pos
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
this : (∫ (x : α) in t, AEStronglyMeasurable.mk f hf x ∂μ) = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in t, AEStronglyMeasurable.mk f hf x ∂μ
case pos
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
this : (∫ (x : α) in t, AEStronglyMeasurable.mk f hf x ∂μ) = 0
⊢ (∫ (x : α) in t, f x ∂μ) = 0
rw [← this]
no goals
case pos
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
this : (∫ (x : α) in t, AEStronglyMeasurable.mk f hf x ∂μ) = 0
⊢ (∫ (x : α) in t, f x ∂μ) = ∫ (x : α) in t, AEStronglyMeasurable.mk f hf x ∂μ
exact integral_congr_ae hf.ae_eq_mk
case neg
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (Measure.restrict μ t)
⊢ ¬Integrable fun x => f x
case neg
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (∫ (x : α) in t, f x ∂μ) = 0
rw [integral_undef]
case neg
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : Integrable fun x => f x
⊢ AEStronglyMeasurable f (Measure.restrict μ t)
case neg
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (Measure.restrict μ t)
⊢ ¬Integrable fun x => f x
contrapose! hf
no goals
case neg
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : Integrable fun x => f x
⊢ AEStronglyMeasurable f (Measure.restrict μ t)
exact hf.1
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (fun x => AEStronglyMeasurable.mk f hf x) =ᵐ[Measure.restrict μ t] 0
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (∫ (x : α) in t, AEStronglyMeasurable.mk f hf x ∂μ) = 0
refine' integral_eq_zero_of_ae _
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t → AEStronglyMeasurable.mk f hf x = OfNat.ofNat 0 x
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
⊢ (fun x => AEStronglyMeasurable.mk f hf x) =ᵐ[Measure.restrict μ t] 0
rw [EventuallyEq,
  ae_restrict_iff (hf.stronglyMeasurable_mk.measurableSet_eq_fun stronglyMeasurable_zero)]
case h
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
x : α
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ AEStronglyMeasurable.mk f hf x = OfNat.ofNat 0 x
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t → AEStronglyMeasurable.mk f hf x = OfNat.ofNat 0 x
filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x
case h
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
x : α
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ f x = OfNat.ofNat 0 x
case h
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
x : α
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ AEStronglyMeasurable.mk f hf x = OfNat.ofNat 0 x
rw [← hx h''x]
no goals
case h
α : Type u_1
β : Type ?u.72393
E : Type u_2
F : Type ?u.72399
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht_eq : ∀ᵐ (x : α) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (Measure.restrict μ t)
x : α
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ f x = OfNat.ofNat 0 x
exact h'x h''x