α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
⊢ IntegrableOn f t
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
⊢ IntegrableOn f t
let u := { x ∈ s | f x ≠ 0 }
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
⊢ IntegrableOn f t
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
⊢ IntegrableOn f t
have hu : IntegrableOn f u μ := hf.mono_set fun x hx => hx.1
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
⊢ IntegrableOn f t
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
⊢ IntegrableOn f t
let v := toMeasurable μ u
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
B : IntegrableOn f (t \ v)
⊢ t ⊆ v ∪ t \ v
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
B : IntegrableOn f (t \ v)
⊢ IntegrableOn f t
apply (A.union B).mono_set _
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
B : IntegrableOn f (t \ v)
⊢ t ⊆ v ∪ t
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
B : IntegrableOn f (t \ v)
⊢ t ⊆ v ∪ t \ v
rw [union_diff_self]
no goals
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
B : IntegrableOn f (t \ v)
⊢ t ⊆ v ∪ t
exact subset_union_right _ _
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
⊢ Integrable f

α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
⊢ ∀ (x : α), x ∈ u → f x ≠ 0
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
⊢ IntegrableOn f v
rw [IntegrableOn, hu.restrict_toMeasurable]
no goals
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
⊢ Integrable f
exact hu
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
x : α
hx : x ∈ u
⊢ f x ≠ 0
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
⊢ ∀ (x : α), x ∈ u → f x ≠ 0
intro x hx
no goals
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
x : α
hx : x ∈ u
⊢ f x ≠ 0
exact hx.2
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
⊢ (fun x => 0) =ᵐ[Measure.restrict μ (t \ v)] f
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
⊢ IntegrableOn f (t \ v)
apply integrableOn_zero.congr
case h
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ toMeasurable μ {x | x ∈ s ∧ f x ≠ 0}
⊢ 0 = f x
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
⊢ (fun x => 0) =ᵐ[Measure.restrict μ (t \ v)] f
filter_upwards [ae_restrict_of_ae h't,
  ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx
case pos
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ toMeasurable μ {x | x ∈ s ∧ f x ≠ 0}
h'x : x ∈ s
⊢ 0 = f x

case neg
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ toMeasurable μ {x | x ∈ s ∧ f x ≠ 0}
h'x : ¬x ∈ s
⊢ 0 = f x
case h
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ toMeasurable μ {x | x ∈ s ∧ f x ≠ 0}
⊢ 0 = f x
by_cases h'x : x ∈ s
case pos
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ toMeasurable μ {x | x ∈ s ∧ f x ≠ 0}
h'x : x ∈ s
H : ¬0 = f x
⊢ False
case pos
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ toMeasurable μ {x | x ∈ s ∧ f x ≠ 0}
h'x : x ∈ s
⊢ 0 = f x
by_contra H
no goals
case pos
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ toMeasurable μ {x | x ∈ s ∧ f x ≠ 0}
h'x : x ∈ s
H : ¬0 = f x
⊢ False
exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)
no goals
case neg
α : Type u_1
β : Type ?u.1647552
E : Type u_2
F : Type ?u.1647558
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
ht : NullMeasurableSet t
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u
v : Set α := toMeasurable μ u
A : IntegrableOn f v
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ toMeasurable μ {x | x ∈ s ∧ f x ≠ 0}
h'x : ¬x ∈ s
⊢ 0 = f x
exact (hxt ⟨hx.1, h'x⟩).symm