[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : TopologicalSpace β
l l' : Filter α
f✝ g : α → β
μ ν : Measure α
f : α → β
⊢ AEStronglyMeasurable f (Measure.restrict μ ∅)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : TopologicalSpace β
l l' : Filter α
f g : α → β
μ ν : Measure α
h : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (Measure.restrict μ univ)
[PROOFSTEP]
rwa [Measure.restrict_univ]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
C : ℝ
hs : ↑↑μ s < ⊤
hf : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
⊢ ↑↑(Measure.restrict μ s) univ < ⊤
[PROOFSTEP]
rwa [Measure.restrict_apply_univ]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
⊢ IntegrableOn f ∅
[PROOFSTEP]
simp [IntegrableOn, integrable_zero_measure]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
⊢ IntegrableOn f univ ↔ Integrable f
[PROOFSTEP]
rw [IntegrableOn, Measure.restrict_univ]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
C : E
⊢ C = 0 ∨ ↑↑(Measure.restrict μ s) univ < ⊤ ↔ C = 0 ∨ ↑↑μ s < ⊤
[PROOFSTEP]
rw [Measure.restrict_apply_univ]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h : IntegrableOn f s
hs : MeasurableSet s
⊢ IntegrableOn f s
[PROOFSTEP]
rw [IntegrableOn, Measure.restrict_restrict hs]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h : IntegrableOn f s
hs : MeasurableSet s
⊢ Integrable f
[PROOFSTEP]
exact h.mono_set (inter_subset_left _ _)
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
⊢ IntegrableOn f {x} ↔ f x = 0 ∨ ↑↑μ {x} < ⊤
[PROOFSTEP]
have : f =ᵐ[μ.restrict { x }] fun _ => f x :=
  by
  filter_upwards [ae_restrict_mem (measurableSet_singleton x)] with _ ha
  simp only [mem_singleton_iff.1 ha]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
⊢ f =ᵐ[Measure.restrict μ {x}] fun x_1 => f x
[PROOFSTEP]
filter_upwards [ae_restrict_mem (measurableSet_singleton x)] with _ ha
[GOAL]
case h
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
a✝ : α
ha : a✝ ∈ {x}
⊢ f a✝ = f x
[PROOFSTEP]
simp only [mem_singleton_iff.1 ha]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
this : f =ᵐ[Measure.restrict μ {x}] fun x_1 => f x
⊢ IntegrableOn f {x} ↔ f x = 0 ∨ ↑↑μ {x} < ⊤
[PROOFSTEP]
rw [IntegrableOn, integrable_congr this, integrable_const_iff]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
x : α
inst✝ : MeasurableSingletonClass α
this : f =ᵐ[Measure.restrict μ {x}] fun x_1 => f x
⊢ f x = 0 ∨ ↑↑(Measure.restrict μ {x}) univ < ⊤ ↔ f x = 0 ∨ ↑↑μ {x} < ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝ t✝ : Set α
μ ν : Measure α
s : Set β
hs : Set.Finite s
t : β → Set α
⊢ IntegrableOn f (⋃ (i : β) (_ : i ∈ s), t i) ↔ ∀ (i : β), i ∈ s → IntegrableOn f (t i)
[PROOFSTEP]
refine hs.induction_on ?_ ?_
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝ t✝ : Set α
μ ν : Measure α
s : Set β
hs : Set.Finite s
t : β → Set α
⊢ IntegrableOn f (⋃ (i : β) (_ : i ∈ ∅), t i) ↔ ∀ (i : β), i ∈ ∅ → IntegrableOn f (t i)
[PROOFSTEP]
simp
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝ t✝ : Set α
μ ν : Measure α
s : Set β
hs : Set.Finite s
t : β → Set α
⊢ ∀ {a : β} {s : Set β},
    ¬a ∈ s →
      Set.Finite s →
        (IntegrableOn f (⋃ (i : β) (_ : i ∈ s), t i) ↔ ∀ (i : β), i ∈ s → IntegrableOn f (t i)) →
          (IntegrableOn f (⋃ (i : β) (_ : i ∈ insert a s), t i) ↔ ∀ (i : β), i ∈ insert a s → IntegrableOn f (t i))
[PROOFSTEP]
intro a s _ _ hf
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝¹ t✝ : Set α
μ ν : Measure α
s✝ : Set β
hs : Set.Finite s✝
t : β → Set α
a : β
s : Set β
a✝¹ : ¬a ∈ s
a✝ : Set.Finite s
hf : IntegrableOn f (⋃ (i : β) (_ : i ∈ s), t i) ↔ ∀ (i : β), i ∈ s → IntegrableOn f (t i)
⊢ IntegrableOn f (⋃ (i : β) (_ : i ∈ insert a s), t i) ↔ ∀ (i : β), i ∈ insert a s → IntegrableOn f (t i)
[PROOFSTEP]
simp [hf, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
inst✝ : Finite β
t : β → Set α
⊢ IntegrableOn f (⋃ (i : β), t i) ↔ ∀ (i : β), IntegrableOn f (t i)
[PROOFSTEP]
cases nonempty_fintype β
[GOAL]
case intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
inst✝ : Finite β
t : β → Set α
val✝ : Fintype β
⊢ IntegrableOn f (⋃ (i : β), t i) ↔ ∀ (i : β), IntegrableOn f (t i)
[PROOFSTEP]
simpa using @integrableOn_finset_iUnion _ _ _ _ _ f μ Finset.univ t
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hμ : IntegrableOn f s
hν : IntegrableOn f s
⊢ IntegrableOn f s
[PROOFSTEP]
delta IntegrableOn
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hμ : IntegrableOn f s
hν : IntegrableOn f s
⊢ Integrable f
[PROOFSTEP]
rw [Measure.restrict_add]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hμ : IntegrableOn f s
hν : IntegrableOn f s
⊢ Integrable f
[PROOFSTEP]
exact hμ.integrable.add_measure hν
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f✝ g : α → E
s✝ t : Set α
μ✝ ν : Measure α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure α
s : Set β
⊢ IntegrableOn f s ↔ IntegrableOn (f ∘ e) (e ⁻¹' s)
[PROOFSTEP]
simp only [IntegrableOn, he.restrict_map, he.integrable_map_iff]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f✝ g : α → E
s✝ t : Set α
μ✝ ν : Measure α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
f : β → E
μ : Measure α
s : Set β
⊢ IntegrableOn f s ↔ IntegrableOn (f ∘ ↑e) (↑e ⁻¹' s)
[PROOFSTEP]
simp only [IntegrableOn, e.restrict_map, integrable_map_equiv e]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hs : MeasurableSet s
⊢ Integrable (indicator s f) ↔ IntegrableOn f s
[PROOFSTEP]
simp [IntegrableOn, Integrable, HasFiniteIntegral, nnnorm_indicator_eq_indicator_nnnorm, ENNReal.coe_indicator,
  lintegral_indicator _ hs, aestronglyMeasurable_indicator_iff hs]
[GOAL]
α : Type u_1
β : Type u_2
E✝ : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ Integrable ↑↑(indicatorConstLp p hs hμs c)
[PROOFSTEP]
rw [integrable_congr indicatorConstLp_coeFn, integrable_indicator_iff hs, IntegrableOn, integrable_const_iff,
  lt_top_iff_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
E✝ : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ c = 0 ∨ ↑↑(Measure.restrict μ s) univ ≠ ⊤
[PROOFSTEP]
right
[GOAL]
case h
α : Type u_1
β : Type u_2
E✝ : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
⊢ ↑↑(Measure.restrict μ s) univ ≠ ⊤
[PROOFSTEP]
simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply] using hμs
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
⊢ Measure.restrict μ (toMeasurable μ s) = Measure.restrict μ s
[PROOFSTEP]
rcases exists_seq_strictAnti_tendsto (0 : ℝ) with ⟨u, _, u_pos, u_lim⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ Measure.restrict μ (toMeasurable μ s) = Measure.restrict μ s
[PROOFSTEP]
let v n := toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
⊢ Measure.restrict μ (toMeasurable μ s) = Measure.restrict μ s
[PROOFSTEP]
have A : ∀ n, μ (s ∩ v n) ≠ ∞ := by
  intro n
  rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]
  exact (hf.measure_ge_lt_top (u_pos n)).ne
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
⊢ ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
n : ℕ
⊢ ↑↑μ (s ∩ v n) ≠ ⊤
[PROOFSTEP]
rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
n : ℕ
⊢ ↑↑(Measure.restrict μ s) {x | u n ≤ ‖f x‖} ≠ ⊤
[PROOFSTEP]
exact (hf.measure_ge_lt_top (u_pos n)).ne
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
⊢ Measure.restrict μ (toMeasurable μ s) = Measure.restrict μ s
[PROOFSTEP]
apply Measure.restrict_toMeasurable_of_cover _ A
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
⊢ s ⊆ ⋃ (n : ℕ), v n
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (n : ℕ), v n
[PROOFSTEP]
have : 0 < ‖f x‖ := by simp only [h's x hx, norm_pos_iff, Ne.def, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
x : α
hx : x ∈ s
⊢ 0 < ‖f x‖
[PROOFSTEP]
simp only [h's x hx, norm_pos_iff, Ne.def, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
x : α
hx : x ∈ s
this : 0 < ‖f x‖
⊢ x ∈ ⋃ (n : ℕ), v n
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ n, u n < ‖f x‖
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
x : α
hx : x ∈ s
this : 0 < ‖f x‖
⊢ ∃ n, u n < ‖f x‖
case intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
x : α
hx : x ∈ s
this : 0 < ‖f x‖
n : ℕ
hn : u n < ‖f x‖
⊢ x ∈ ⋃ (n : ℕ), v n
[PROOFSTEP]
exact ((tendsto_order.1 u_lim).2 _ this).exists
[GOAL]
case intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
x : α
hx : x ∈ s
this : 0 < ‖f x‖
n : ℕ
hn : u n < ‖f x‖
⊢ x ∈ ⋃ (n : ℕ), v n
[PROOFSTEP]
refine' mem_iUnion.2 ⟨n, _⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h's : ∀ (x : α), x ∈ s → f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (Measure.restrict μ s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
x : α
hx : x ∈ s
this : 0 < ‖f x‖
n : ℕ
hn : u n < ‖f x‖
⊢ x ∈ v n
[PROOFSTEP]
exact subset_toMeasurable _ _ hn.le
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
let u := {x ∈ s | f x ≠ 0}
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
have hu : IntegrableOn f u μ := hf.mono_set fun x hx => hx.1
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
let v := toMeasurable μ u
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
have A : IntegrableOn f v μ := by
  rw [IntegrableOn, hu.restrict_toMeasurable]
  · exact hu
  · intro x hx; exact hx.2
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
rw [IntegrableOn, hu.restrict_toMeasurable]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
exact hu
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
exact hx.2
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
have B : IntegrableOn f (t \ v) μ := by
  apply integrableOn_zero.congr
  filter_upwards [ae_restrict_of_ae h't,
    ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx
  by_cases h'x : x ∈ s
  · by_contra H
    exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)
  · exact (hxt ⟨hx.1, h'x⟩).symm
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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)
[PROOFSTEP]
apply integrableOn_zero.congr
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
filter_upwards [ae_restrict_of_ae h't,
  ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx
[GOAL]
case h
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
by_cases h'x : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
by_contra H
[GOAL]
case pos
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)
[GOAL]
case neg
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
exact (hxt ⟨hx.1, h'x⟩).symm
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
apply (A.union B).mono_set _
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
rw [union_diff_self]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
exact subset_union_right _ _
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h't : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ Integrable f
[PROOFSTEP]
rw [← integrableOn_univ]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h't : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ IntegrableOn f univ
[PROOFSTEP]
apply hf.of_ae_diff_eq_zero nullMeasurableSet_univ
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h't : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
[PROOFSTEP]
filter_upwards [h't] with x hx h'x using hx h'x.2
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
⊢ IntegrableOn f s ↔ Integrable f
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.integrableOn⟩
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s
⊢ Integrable f
[PROOFSTEP]
refine h.integrable_of_forall_not_mem_eq_zero fun x hx => ?_
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s
x : α
hx : ¬x ∈ s
⊢ f x = 0
[PROOFSTEP]
contrapose! hx
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s
x : α
hx : f x ≠ 0
⊢ x ∈ s
[PROOFSTEP]
exact h1s (mem_support.2 hx)
[GOAL]
α : Type u_1
β : Type u_2
E✝ : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
⊢ IntegrableOn (↑↑f) s
[PROOFSTEP]
refine' memℒp_one_iff_integrable.mp _
[GOAL]
α : Type u_1
β : Type u_2
E✝ : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
⊢ Memℒp (↑↑f) 1
[PROOFSTEP]
have hμ_restrict_univ : (μ.restrict s) Set.univ < ∞ := by
  simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
E✝ : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
⊢ ↑↑(Measure.restrict μ s) univ < ⊤
[PROOFSTEP]
simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
E✝ : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
hμ_restrict_univ : ↑↑(Measure.restrict μ s) univ < ⊤
⊢ Memℒp (↑↑f) 1
[PROOFSTEP]
haveI hμ_finite : IsFiniteMeasure (μ.restrict s) := ⟨hμ_restrict_univ⟩
[GOAL]
α : Type u_1
β : Type u_2
E✝ : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E✝
f✝ g : α → E✝
s✝ t : Set α
μ ν : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : { x // x ∈ Lp E p }
hp : 1 ≤ p
hμs : ↑↑μ s ≠ ⊤
hμ_restrict_univ : ↑↑(Measure.restrict μ s) univ < ⊤
hμ_finite : IsFiniteMeasure (Measure.restrict μ s)
⊢ Memℒp (↑↑f) 1
[PROOFSTEP]
exact ((Lp.memℒp _).restrict s).memℒp_of_exponent_le hp
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
hf : IntegrableAtFilter f l
hg : IntegrableAtFilter g l
⊢ IntegrableAtFilter (f + g) l
[PROOFSTEP]
rcases hf with ⟨s, sl, hs⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
hg : IntegrableAtFilter g l
s : Set α
sl : s ∈ l
hs : IntegrableOn f s
⊢ IntegrableAtFilter (f + g) l
[PROOFSTEP]
rcases hg with ⟨t, tl, ht⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s✝ t✝ : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s
t : Set α
tl : t ∈ l
ht : IntegrableOn g t
⊢ IntegrableAtFilter (f + g) l
[PROOFSTEP]
refine ⟨s ∩ t, inter_mem sl tl, ?_⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s✝ t✝ : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s
t : Set α
tl : t ∈ l
ht : IntegrableOn g t
⊢ IntegrableOn (f + g) (s ∩ t)
[PROOFSTEP]
exact (hs.mono_set (inter_subset_left _ _)).add (ht.mono_set (inter_subset_right _ _))
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f : α → E
hf : IntegrableAtFilter f l
⊢ IntegrableAtFilter (-f) l
[PROOFSTEP]
rcases hf with ⟨s, sl, hs⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
f : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s
⊢ IntegrableAtFilter (-f) l
[PROOFSTEP]
exact ⟨s, sl, hs.neg⟩
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
hf : IntegrableAtFilter f l
hg : IntegrableAtFilter g l
⊢ IntegrableAtFilter (f - g) l
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
hf : IntegrableAtFilter f l
hg : IntegrableAtFilter g l
⊢ IntegrableAtFilter (f + -g) l
[PROOFSTEP]
exact hf.add hg.neg
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l✝ l' l : Filter α
⊢ IntegrableAtFilter f (l ⊓ Measure.ae μ) ↔ IntegrableAtFilter f l
[PROOFSTEP]
refine' ⟨_, fun h => h.filter_mono inf_le_left⟩
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l✝ l' l : Filter α
⊢ IntegrableAtFilter f (l ⊓ Measure.ae μ) → IntegrableAtFilter f l
[PROOFSTEP]
rintro ⟨s, ⟨t, ht, u, hu, rfl⟩, hf⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
⊢ IntegrableAtFilter f l
[PROOFSTEP]
refine' ⟨t, ht, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
⊢ IntegrableOn f t
[PROOFSTEP]
refine' hf.integrable.mono_measure fun v hv => _
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
v : Set α
hv : MeasurableSet v
⊢ ↑↑(Measure.restrict μ t) v ≤ ↑↑(Measure.restrict μ (t ∩ u)) v
[PROOFSTEP]
simp only [Measure.restrict_apply hv]
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
v : Set α
hv : MeasurableSet v
⊢ ↑↑μ (v ∩ t) ≤ ↑↑μ (v ∩ (t ∩ u))
[PROOFSTEP]
refine' measure_mono_ae (mem_of_superset hu fun x hx => _)
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t✝ : Set α
μ ν : Measure α
l✝ l' l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ Measure.ae μ
hf : IntegrableOn f (t ∩ u)
v : Set α
hv : MeasurableSet v
x : α
hx : x ∈ u
⊢ x ∈ {x | (fun x => (v ∩ t) x ≤ (v ∩ (t ∩ u)) x) x}
[PROOFSTEP]
exact fun ⟨hv, ht⟩ => ⟨hv, ⟨ht, hx⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l✝ l' l : Filter α
inst✝ : IsMeasurablyGenerated l
hfm : StronglyMeasurableAtFilter f l
hμ : FiniteAtFilter μ l
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
⊢ IntegrableAtFilter f l
[PROOFSTEP]
obtain ⟨C, hC⟩ : ∃ C, ∀ᶠ s in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l✝ l' l : Filter α
inst✝ : IsMeasurablyGenerated l
hfm : StronglyMeasurableAtFilter f l
hμ : FiniteAtFilter μ l
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
⊢ ∃ C, ∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
case intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l✝ l' l : Filter α
inst✝ : IsMeasurablyGenerated l
hfm : StronglyMeasurableAtFilter f l
hμ : FiniteAtFilter μ l
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
C : ℝ
hC : ∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l
[PROOFSTEP]
exact hf.imp fun C hC => eventually_smallSets.2 ⟨_, hC, fun t => id⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l✝ l' l : Filter α
inst✝ : IsMeasurablyGenerated l
hfm : StronglyMeasurableAtFilter f l
hμ : FiniteAtFilter μ l
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
C : ℝ
hC : ∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l
[PROOFSTEP]
rcases(hfm.eventually.and (hμ.eventually.and hC)).exists_measurable_mem_of_smallSets with ⟨s, hsl, hsm, hfm, hμ, hC⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l✝ l' l : Filter α
inst✝ : IsMeasurablyGenerated l
hfm✝ : StronglyMeasurableAtFilter f l
hμ✝ : FiniteAtFilter μ l
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (restrict μ s)
hμ : ↑↑μ s < ⊤
hC : ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l
[PROOFSTEP]
refine' ⟨s, hsl, ⟨hfm, hasFiniteIntegral_restrict_of_bounded hμ _⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l✝ l' l : Filter α
inst✝ : IsMeasurablyGenerated l
hfm✝ : StronglyMeasurableAtFilter f l
hμ✝ : FiniteAtFilter μ l
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (restrict μ s)
hμ : ↑↑μ s < ⊤
hC : ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
⊢ ℝ
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l✝ l' l : Filter α
inst✝ : IsMeasurablyGenerated l
hfm✝ : StronglyMeasurableAtFilter f l
hμ✝ : FiniteAtFilter μ l
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (restrict μ s)
hμ : ↑↑μ s < ⊤
hC : ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂restrict μ s, ‖f x‖ ≤ ?intro.intro.intro.intro.intro.intro.refine'_1
[PROOFSTEP]
exact C
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l✝ l' l : Filter α
inst✝ : IsMeasurablyGenerated l
hfm✝ : StronglyMeasurableAtFilter f l
hμ✝ : FiniteAtFilter μ l
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (restrict μ s)
hμ : ↑↑μ s < ⊤
hC : ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂restrict μ s, ‖f x‖ ≤ C
[PROOFSTEP]
rw [ae_restrict_eq hsm, eventually_inf_principal]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l✝ l' l : Filter α
inst✝ : IsMeasurablyGenerated l
hfm✝ : StronglyMeasurableAtFilter f l
hμ✝ : FiniteAtFilter μ l
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (restrict μ s)
hμ : ↑↑μ s < ⊤
hC : ∀ (x : α), x ∈ s → ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
[PROOFSTEP]
exact eventually_of_forall hC
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ Integrable (f + g) ↔ Integrable f ∧ Integrable g
[PROOFSTEP]
refine' ⟨fun hfg => ⟨_, _⟩, fun h => h.1.add h.2⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable f
[PROOFSTEP]
rw [← indicator_add_eq_left h]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable (indicator (support f) (f + g))
[PROOFSTEP]
exact hfg.indicator hf.measurableSet_support
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable g
[PROOFSTEP]
rw [← indicator_add_eq_right h]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ g✝ : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g)
⊢ Integrable (indicator (support g) (f + g))
[PROOFSTEP]
exact hfg.indicator hg.measurableSet_support
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
⊢ AEMeasurable f
[PROOFSTEP]
nontriviality α
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
⊢ AEMeasurable f
[PROOFSTEP]
inhabit α
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f
[PROOFSTEP]
have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
⊢ AEMeasurable f
[PROOFSTEP]
refine' ⟨Set.piecewise s f fun _ => f default, _, this.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
⊢ Measurable (Set.piecewise s f fun x => f default)
[PROOFSTEP]
apply measurable_of_isOpen
[GOAL]
case hf
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
⊢ ∀ (s_1 : Set β), IsOpen s_1 → MeasurableSet ((Set.piecewise s f fun x => f default) ⁻¹' s_1)
[PROOFSTEP]
intro t ht
[GOAL]
case hf
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
t : Set β
ht : IsOpen t
⊢ MeasurableSet ((Set.piecewise s f fun x => f default) ⁻¹' t)
[PROOFSTEP]
obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s := _root_.continuousOn_iff'.1 hf t ht
[GOAL]
case hf.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet ((Set.piecewise s f fun x => f default) ⁻¹' t)
[PROOFSTEP]
rw [piecewise_preimage, Set.ite, hu]
[GOAL]
case hf.intro.intro
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (u ∩ s ∪ (fun x => f default) ⁻¹' t \ s)
[PROOFSTEP]
exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetrizableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
[PROOFSTEP]
letI := pseudoMetrizableSpacePseudoMetric α
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetrizableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
[PROOFSTEP]
borelize β
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetrizableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
[PROOFSTEP]
rw [aestronglyMeasurable_iff_aemeasurable_separable]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetrizableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEMeasurable f ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ∈ t
[PROOFSTEP]
refine' ⟨hf.aemeasurable hs, f '' s, hf.isSeparable_image h's, _⟩
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetrizableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ∈ f '' s
[PROOFSTEP]
exact mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
[PROOFSTEP]
borelize β
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
[PROOFSTEP]
refine'
  aestronglyMeasurable_iff_aemeasurable_separable.2
    ⟨hf.aemeasurable hs, f '' s, _, mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)⟩
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (f '' s)
[PROOFSTEP]
cases h.out
[GOAL]
case inl
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ IsSeparable (f '' s)
[PROOFSTEP]
let f' : s → β := s.restrict f
[GOAL]
case inl
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
f' : ↑s → β := Set.restrict s f
⊢ IsSeparable (f '' s)
[PROOFSTEP]
have A : Continuous f' := continuousOn_iff_continuous_restrict.1 hf
[GOAL]
case inl
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
f' : ↑s → β := Set.restrict s f
A : Continuous f'
⊢ IsSeparable (f '' s)
[PROOFSTEP]
have B : IsSeparable (univ : Set s) := isSeparable_of_separableSpace _
[GOAL]
case inl
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
f' : ↑s → β := Set.restrict s f
A : Continuous f'
B : IsSeparable univ
⊢ IsSeparable (f '' s)
[PROOFSTEP]
convert IsSeparable.image B A using 1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
f' : ↑s → β := Set.restrict s f
A : Continuous f'
B : IsSeparable univ
⊢ f '' s = f' '' univ
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
f' : ↑s → β := Set.restrict s f
A : Continuous f'
B : IsSeparable univ
x : β
⊢ x ∈ f '' s ↔ x ∈ f' '' univ
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology β
⊢ IsSeparable (f '' s)
[PROOFSTEP]
exact isSeparable_of_separableSpace _
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
[PROOFSTEP]
letI := pseudoMetrizableSpacePseudoMetric β
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
[PROOFSTEP]
borelize β
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (Measure.restrict μ s)
[PROOFSTEP]
rw [aestronglyMeasurable_iff_aemeasurable_separable]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEMeasurable f ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ∈ t
[PROOFSTEP]
refine' ⟨hf.aemeasurable h's, f '' s, _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (f '' s)
[PROOFSTEP]
exact (hs.image_of_continuousOn hf).isSeparable
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
h's : MeasurableSet s
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, f x ∈ f '' s
[PROOFSTEP]
exact mem_of_superset (self_mem_ae_restrict h's) (subset_preimage_image _ _)
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous f
a : α
⊢ IntegrableAtFilter f (𝓝 a)
[PROOFSTEP]
rw [← nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous f
a : α
⊢ IntegrableAtFilter f (𝓝[univ] a)
[PROOFSTEP]
exact hf.continuousOn.integrableAt_nhdsWithin MeasurableSet.univ (mem_univ a)
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioc a b)
[PROOFSTEP]
by_cases hab : a ≤ b
[GOAL]
case pos
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioc a b)
[PROOFSTEP]
rw [← Ioc_union_left hab, integrableOn_union, eq_true (integrableOn_singleton_iff.mpr <| Or.inr ha.lt_top),
  and_true_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioc a b)
[PROOFSTEP]
rw [Icc_eq_empty hab, Ioc_eq_empty]
[GOAL]
case neg
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : ¬a ≤ b
⊢ ¬a < b
[PROOFSTEP]
contrapose! hab
[GOAL]
case neg
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : a < b
⊢ a ≤ b
[PROOFSTEP]
exact hab.le
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ico a b)
[PROOFSTEP]
by_cases hab : a ≤ b
[GOAL]
case pos
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ico a b)
[PROOFSTEP]
rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top),
  and_true_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ico a b)
[PROOFSTEP]
rw [Icc_eq_empty hab, Ico_eq_empty]
[GOAL]
case neg
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : ¬a ≤ b
⊢ ¬a < b
[PROOFSTEP]
contrapose! hab
[GOAL]
case neg
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : a < b
⊢ a ≤ b
[PROOFSTEP]
exact hab.le
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
⊢ IntegrableOn f (Ico a b) ↔ IntegrableOn f (Ioo a b)
[PROOFSTEP]
by_cases hab : a < b
[GOAL]
case pos
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : a < b
⊢ IntegrableOn f (Ico a b) ↔ IntegrableOn f (Ioo a b)
[PROOFSTEP]
rw [← Ioo_union_left hab, integrableOn_union, eq_true (integrableOn_singleton_iff.mpr <| Or.inr ha.lt_top),
  and_true_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hab : ¬a < b
⊢ IntegrableOn f (Ico a b) ↔ IntegrableOn f (Ioo a b)
[PROOFSTEP]
rw [Ioo_eq_empty hab, Ico_eq_empty hab]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
⊢ IntegrableOn f (Ioc a b) ↔ IntegrableOn f (Ioo a b)
[PROOFSTEP]
by_cases hab : a < b
[GOAL]
case pos
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : a < b
⊢ IntegrableOn f (Ioc a b) ↔ IntegrableOn f (Ioo a b)
[PROOFSTEP]
rw [← Ioo_union_right hab, integrableOn_union, eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top),
  and_true_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
hab : ¬a < b
⊢ IntegrableOn f (Ioc a b) ↔ IntegrableOn f (Ioo a b)
[PROOFSTEP]
rw [Ioo_eq_empty hab, Ioc_eq_empty hab]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : ↑↑μ {a} ≠ ⊤
hb : ↑↑μ {b} ≠ ⊤
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioo a b)
[PROOFSTEP]
rw [integrableOn_Icc_iff_integrableOn_Ioc' ha, integrableOn_Ioc_iff_integrableOn_Ioo' hb]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
⊢ IntegrableOn f (Ici b) ↔ IntegrableOn f (Ioi b)
[PROOFSTEP]
rw [← Ioi_union_left, integrableOn_union, eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top), and_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
⊢ IntegrableOn f (Iic b) ↔ IntegrableOn f (Iio b)
[PROOFSTEP]
rw [← Iio_union_right, integrableOn_union, eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top), and_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ ↑↑μ {a} ≠ ⊤
[PROOFSTEP]
rw [measure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
[PROOFSTEP]
exact ENNReal.zero_ne_top
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ ↑↑μ {b} ≠ ⊤
[PROOFSTEP]
rw [measure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
[PROOFSTEP]
exact ENNReal.zero_ne_top
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ ↑↑μ {a} ≠ ⊤
[PROOFSTEP]
rw [measure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
[PROOFSTEP]
exact ENNReal.zero_ne_top
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ ↑↑μ {b} ≠ ⊤
[PROOFSTEP]
rw [measure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
[PROOFSTEP]
exact ENNReal.zero_ne_top
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ IntegrableOn f (Icc a b) ↔ IntegrableOn f (Ioo a b)
[PROOFSTEP]
rw [integrableOn_Icc_iff_integrableOn_Ioc, integrableOn_Ioc_iff_integrableOn_Ioo]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ ↑↑μ {b} ≠ ⊤
[PROOFSTEP]
rw [measure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
[PROOFSTEP]
exact ENNReal.zero_ne_top
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ ↑↑μ {b} ≠ ⊤
[PROOFSTEP]
rw [measure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
[PROOFSTEP]
exact ENNReal.zero_ne_top