case intro.intro.intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
rcases exists_seq_strictAnti_tendsto (0 : ℝ) with ⟨u, _, u_pos, u_lim⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
case intro.intro.intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
let v n := toMeasurable (μ.restrict s) { x | u n ≤ ‖f x‖ }
case intro.intro.intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
case intro.intro.intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
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
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
case intro.intro.intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
apply Measure.restrict_toMeasurable_of_cover _ A
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
intro x hx
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
have : 0 < ‖f x‖ := by simp only [h's x hx, norm_pos_iff, Ne.def, not_false_iff]
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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.1644972
E : Type u_2
F : Type ?u.1644978
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
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
obtain ⟨n, hn⟩ : ∃ n, u n < ‖f x‖
case intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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.1644972
E : Type u_2
F : Type ?u.1644978
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
exact ((tendsto_order.1 u_lim).2 _ this).exists
case intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
case intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
refine' mem_iUnion.2 ⟨n, _⟩
no goals
case intro
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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
exact subset_toMeasurable _ _ hn.le
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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) ≠ ⊤
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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) ≠ ⊤
intro n
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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‖} ≠ ⊤
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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) ≠ ⊤
rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _),
  measure_toMeasurable]
no goals
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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‖} ≠ ⊤
exact (hf.measure_ge_lt_top (u_pos n)).ne
no goals
α : Type u_1
β : Type ?u.1644972
E : Type u_2
F : Type ?u.1644978
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‖
simp only [h's x hx, norm_pos_iff, Ne.def, not_false_iff]