α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6149244
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (Measure.restrict μ s)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator s 1 x))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6149244
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator s 1 x))
haveI : IsLocallyFiniteMeasure (μ.restrict s) :=
  isLocallyFiniteMeasure_of_le restrict_le_self
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6149244
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (Measure.restrict μ s)
⊢ ∀ (a : α),
    Tendsto (fun a => ↑↑(Measure.restrict μ s) a / ↑↑μ a) (filterAt v a) (𝓝 (rnDeriv (Measure.restrict μ s) μ a)) →
      rnDeriv (Measure.restrict μ s) μ a = indicator s 1 a →
        Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v a) (𝓝 (indicator s 1 a))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6149244
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (Measure.restrict μ s)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator s 1 x))
filter_upwards [ae_tendsto_rnDeriv v (μ.restrict s), rnDeriv_restrict μ hs]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6149244
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (Measure.restrict μ s)
x : α
hx : Tendsto (fun a => ↑↑(Measure.restrict μ s) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (Measure.restrict μ s) μ x))
h'x : rnDeriv (Measure.restrict μ s) μ x = indicator s 1 x
⊢ Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator s 1 x))
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6149244
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (Measure.restrict μ s)
⊢ ∀ (a : α),
    Tendsto (fun a => ↑↑(Measure.restrict μ s) a / ↑↑μ a) (filterAt v a) (𝓝 (rnDeriv (Measure.restrict μ s) μ a)) →
      rnDeriv (Measure.restrict μ s) μ a = indicator s 1 a →
        Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v a) (𝓝 (indicator s 1 a))
intro x hx h'x
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6149244
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (Measure.restrict μ s)
x : α
hx : Tendsto (fun a => ↑↑(Measure.restrict μ s) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (Measure.restrict μ s) μ x))
h'x : rnDeriv (Measure.restrict μ s) μ x = indicator s 1 x
⊢ Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator s 1 x))
simpa only [h'x, restrict_apply' hs, inter_comm] using hx