case h
α : Type ?u.1047956
inst✝¹¹ : MetricSpace α
β : Type u
inst✝¹⁰ : SecondCountableTopology α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : OpensMeasurableSpace α
inst✝⁷ : HasBesicovitchCovering α
inst✝⁶ : MetricSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : SecondCountableTopology β
inst✝² : HasBesicovitchCovering β
ρ μ : MeasureTheory.Measure β
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsLocallyFiniteMeasure ρ
x : β
hx : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 (Measure.rnDeriv ρ μ x))
⊢ Tendsto (fun r => ↑↑ρ (closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 (Measure.rnDeriv ρ μ x))
α : Type ?u.1047956
inst✝¹¹ : MetricSpace α
β : Type u
inst✝¹⁰ : SecondCountableTopology α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : OpensMeasurableSpace α
inst✝⁷ : HasBesicovitchCovering α
inst✝⁶ : MetricSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : SecondCountableTopology β
inst✝² : HasBesicovitchCovering β
ρ μ : MeasureTheory.Measure β
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsLocallyFiniteMeasure ρ
⊢ ∀ᵐ (x : β) ∂μ, Tendsto (fun r => ↑↑ρ (closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 (Measure.rnDeriv ρ μ x))
filter_upwards [VitaliFamily.ae_tendsto_rnDeriv (Besicovitch.vitaliFamily μ) ρ] with x hx
no goals
case h
α : Type ?u.1047956
inst✝¹¹ : MetricSpace α
β : Type u
inst✝¹⁰ : SecondCountableTopology α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : OpensMeasurableSpace α
inst✝⁷ : HasBesicovitchCovering α
inst✝⁶ : MetricSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : SecondCountableTopology β
inst✝² : HasBesicovitchCovering β
ρ μ : MeasureTheory.Measure β
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsLocallyFiniteMeasure ρ
x : β
hx : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 (Measure.rnDeriv ρ μ x))
⊢ Tendsto (fun r => ↑↑ρ (closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 (Measure.rnDeriv ρ μ x))
exact hx.comp (tendsto_filterAt μ x)