α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5427188
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : rnDeriv (withDensity μ (limRatioMeas v hρ)) μ =ᶠ[ae μ] limRatioMeas v hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv ρ μ x))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5427188
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv ρ μ x))
have A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ :=
  rnDeriv_withDensity μ (v.limRatioMeas_measurable hρ)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5427188
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : rnDeriv ρ μ =ᶠ[ae μ] limRatioMeas v hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv ρ μ x))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5427188
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : rnDeriv (withDensity μ (limRatioMeas v hρ)) μ =ᶠ[ae μ] limRatioMeas v hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv ρ μ x))
rw [v.withDensity_limRatioMeas_eq hρ] at A
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5427188
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : rnDeriv ρ μ =ᶠ[ae μ] limRatioMeas v hρ
a✝¹ : α
a✝ : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a✝¹) (𝓝 (limRatioMeas v hρ a✝¹))
h'x : rnDeriv ρ μ a✝¹ = limRatioMeas v hρ a✝¹
⊢ Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a✝¹) (𝓝 (rnDeriv ρ μ a✝¹))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5427188
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : rnDeriv ρ μ =ᶠ[ae μ] limRatioMeas v hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv ρ μ x))
filter_upwards [v.ae_tendsto_limRatioMeas hρ, A] with _ _ h'x
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5427188
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : rnDeriv ρ μ =ᶠ[ae μ] limRatioMeas v hρ
a✝¹ : α
a✝ : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a✝¹) (𝓝 (limRatioMeas v hρ a✝¹))
h'x : rnDeriv ρ μ a✝¹ = limRatioMeas v hρ a✝¹
⊢ Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a✝¹) (𝓝 (rnDeriv ρ μ a✝¹))
rwa [h'x]