α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = ⊤}] x ∧ ↑↑μ u = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ↑↑μ {x | limRatioMeas v hρ x = ⊤} = 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.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = ⊤}] x ∧ ↑↑μ u = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = ⊤}] 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.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = ⊤}] x ∧ ↑↑μ u = 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = ⊤}] x ∧ ↑↑μ u = 0
let s := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
⊢ ↑↑μ s ≤ 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
⊢ ∃ u, u ∈ 𝓝[{x | limRatioMeas v hρ x = ⊤}] 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.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
⊢ ↑↑μ s ≤ 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ 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.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ↑↑ρ s) atTop (𝓝 (⊤⁻¹ * ↑↑ρ s))
⊢ ↑↑μ s ≤ 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
⊢ ↑↑μ s ≤ 0
have B : Tendsto (fun q : ℝ≥0 => (q : ℝ≥0∞)⁻¹ * ρ s) atTop (𝓝 (∞⁻¹ * ρ s)) := by
  apply ENNReal.Tendsto.mul_const _ (Or.inr ρs)
  exact ENNReal.tendsto_inv_iff.2 (ENNReal.tendsto_coe_nhds_top.2 tendsto_id)
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ↑↑ρ ({x | limRatioMeas v hρ x = ⊤} ∩ o)) atTop (𝓝 0)
⊢ ↑↑μ s ≤ 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ↑↑ρ s) atTop (𝓝 (⊤⁻¹ * ↑↑ρ s))
⊢ ↑↑μ s ≤ 0
simp only [MulZeroClass.zero_mul, ENNReal.inv_top] at B
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ↑↑ρ ({x | limRatioMeas v hρ x = ⊤} ∩ o)) atTop (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in atTop, ↑↑μ s ≤ (↑c)⁻¹ * ↑↑ρ ({x | limRatioMeas v hρ x = ⊤} ∩ o)
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ↑↑ρ ({x | limRatioMeas v hρ x = ⊤} ∩ o)) atTop (𝓝 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.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ↑↑ρ ({x | limRatioMeas v hρ x = ⊤} ∩ o)) atTop (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in atTop, ↑↑μ s ≤ (↑c)⁻¹ * ↑↑ρ ({x | limRatioMeas v hρ x = ⊤} ∩ o)
exact eventually_atTop.2 ⟨1, A⟩
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
⊢ ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
intro q hq
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ ↑q * ↑↑μ s ≤ ↑↑ρ s

α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ ↑q ≠ 0 ∨ ↑↑ρ s ≠ 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
rw [mul_comm, ← div_eq_mul_inv, ENNReal.le_div_iff_mul_le _ (Or.inr ρs), mul_comm]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ s ⊆ {x | ↑q < limRatioMeas v hρ x}
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ ↑q * ↑↑μ s ≤ ↑↑ρ s
apply v.mul_measure_le_of_subset_lt_limRatioMeas hρ
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
y : α
hy : y ∈ s
⊢ y ∈ {x | ↑q < limRatioMeas v hρ x}
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ s ⊆ {x | ↑q < limRatioMeas v hρ x}
intro y hy
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
y : α
hy : y ∈ s
this : limRatioMeas v hρ y = ⊤
⊢ y ∈ {x | ↑q < limRatioMeas v hρ x}
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
y : α
hy : y ∈ s
⊢ y ∈ {x | ↑q < limRatioMeas v hρ x}
have : v.limRatioMeas hρ y = ∞ := hy.1
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
y : α
hy : y ∈ s
this : limRatioMeas v hρ y = ⊤
⊢ y ∈ {x | ↑q < limRatioMeas v hρ x}
simp only [this, ENNReal.coe_lt_top, mem_setOf_eq]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ ↑q ≠ 0 ∨ ↑↑ρ s ≠ 0
simp only [(zero_lt_one.trans_le hq).ne', true_or_iff, ENNReal.coe_eq_zero, Ne.def,
  not_false_iff]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
⊢ Tendsto (fun x => (↑x)⁻¹) atTop (𝓝 ⊤⁻¹)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
⊢ Tendsto (fun q => (↑q)⁻¹ * ↑↑ρ s) atTop (𝓝 (⊤⁻¹ * ↑↑ρ s))
apply ENNReal.Tendsto.mul_const _ (Or.inr ρs)
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.4203614
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | limRatioMeas v hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ↑↑ρ o < ⊤
s : Set α := {x | limRatioMeas v hρ x = ⊤} ∩ o
ρs : ↑↑ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → ↑↑μ s ≤ (↑q)⁻¹ * ↑↑ρ s
⊢ Tendsto (fun x => (↑x)⁻¹) atTop (𝓝 ⊤⁻¹)
exact ENNReal.tendsto_inv_iff.2 (ENNReal.tendsto_coe_nhds_top.2 tendsto_id)