α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = 0}] x ∧ ↑↑ρ u = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ↑↑ρ {x | limRatioMeas v hρ x = 0} = 0
refine' null_of_locally_null _ fun x _ => _
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = 0}] x ∧ ↑↑ρ u = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = 0}] x ∧ ↑↑ρ u = 0
obtain ⟨o, xo, o_open, μo⟩ : ∃ o : Set α, x ∈ o ∧ IsOpen o ∧ μ o < ∞ :=
  Measure.exists_isOpen_measure_lt_top μ x
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = 0}] x ∧ ↑↑ρ u = 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = 0}] x ∧ ↑↑ρ u = 0
let s := {x : α | v.limRatioMeas hρ x = 0} ∩ o
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
⊢ ↑↑ρ s ≤ 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = 0}] x ∧ ↑↑ρ u = 0
refine' ⟨s, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), le_antisymm _ bot_le⟩
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
⊢ ↑↑ρ s ≤ 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
⊢ ↑↑ρ s ≤ 0
have μs : μ s ≠ ∞ := ((measure_mono (inter_subset_right _ _)).trans_lt μo).ne
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
⊢ ↑↑ρ s ≤ 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
⊢ ↑↑ρ s ≤ 0
have A : ∀ q : ℝ≥0, 0 < q → ρ s ≤ q * μ s := by
  intro q hq
  apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
  intro y hy
  have : v.limRatioMeas hρ y = 0 := hy.1
  simp only [this, mem_setOf_eq, hq, ENNReal.coe_pos]
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
B : Tendsto (fun q => ↑q * ↑↑μ s) (𝓝[Ioi 0] 0) (𝓝 (↑0 * ↑↑μ s))
⊢ ↑↑ρ s ≤ 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
⊢ ↑↑ρ s ≤ 0
have B : Tendsto (fun q : ℝ≥0 => (q : ℝ≥0∞) * μ s) (𝓝[>] (0 : ℝ≥0)) (𝓝 ((0 : ℝ≥0) * μ s)) := by
  apply ENNReal.Tendsto.mul_const _ (Or.inr μs)
  rw [ENNReal.tendsto_coe]
  exact nhdsWithin_le_nhds
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
B : Tendsto (fun q => ↑q * ↑↑μ ({x | limRatioMeas v hρ x = 0} ∩ o)) (𝓝[Ioi 0] 0) (𝓝 0)
⊢ ↑↑ρ s ≤ 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
B : Tendsto (fun q => ↑q * ↑↑μ s) (𝓝[Ioi 0] 0) (𝓝 (↑0 * ↑↑μ s))
⊢ ↑↑ρ s ≤ 0
simp only [MulZeroClass.zero_mul, ENNReal.coe_zero] at B
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
B : Tendsto (fun q => ↑q * ↑↑μ ({x | limRatioMeas v hρ x = 0} ∩ o)) (𝓝[Ioi 0] 0) (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[Ioi 0] 0, ↑↑ρ s ≤ ↑c * ↑↑μ ({x | limRatioMeas v hρ x = 0} ∩ o)
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
B : Tendsto (fun q => ↑q * ↑↑μ ({x | limRatioMeas v hρ x = 0} ∩ o)) (𝓝[Ioi 0] 0) (𝓝 0)
⊢ ↑↑ρ s ≤ 0
apply ge_of_tendsto B
no goals
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
B : Tendsto (fun q => ↑q * ↑↑μ ({x | limRatioMeas v hρ x = 0} ∩ o)) (𝓝[Ioi 0] 0) (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[Ioi 0] 0, ↑↑ρ s ≤ ↑c * ↑↑μ ({x | limRatioMeas v hρ x = 0} ∩ o)
filter_upwards [self_mem_nhdsWithin] using A
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
⊢ ↑↑ρ s ≤ ↑q * ↑↑μ s
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
⊢ ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
intro q hq
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
⊢ s ⊆ {x | limRatioMeas v hρ x < ↑q}
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
⊢ ↑↑ρ s ≤ ↑q * ↑↑μ s
apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
⊢ y ∈ {x | limRatioMeas v hρ x < ↑q}
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
⊢ s ⊆ {x | limRatioMeas v hρ x < ↑q}
intro y hy
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
this : limRatioMeas v hρ y = 0
⊢ y ∈ {x | limRatioMeas v hρ x < ↑q}
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
⊢ y ∈ {x | limRatioMeas v hρ x < ↑q}
have : v.limRatioMeas hρ y = 0 := hy.1
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
this : limRatioMeas v hρ y = 0
⊢ y ∈ {x | limRatioMeas v hρ x < ↑q}
simp only [this, mem_setOf_eq, hq, ENNReal.coe_pos]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
⊢ Tendsto (fun x => ↑x) (𝓝[Ioi 0] 0) (𝓝 ↑0)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
⊢ Tendsto (fun q => ↑q * ↑↑μ s) (𝓝[Ioi 0] 0) (𝓝 (↑0 * ↑↑μ s))
apply ENNReal.Tendsto.mul_const _ (Or.inr μs)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
⊢ Tendsto (fun x => x) (𝓝[Ioi 0] 0) (𝓝 0)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
⊢ Tendsto (fun x => ↑x) (𝓝[Ioi 0] 0) (𝓝 ↑0)
rw [ENNReal.tendsto_coe]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4445000
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑μ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = 0} ∩ o
μs : ↑↑μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ↑↑ρ s ≤ ↑q * ↑↑μ s
⊢ Tendsto (fun x => x) (𝓝[Ioi 0] 0) (𝓝 0)
exact nhdsWithin_le_nhds