α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
let ρ := μ.withDensity f
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
have : IsFiniteMeasure ρ := isFiniteMeasure_withDensity h'f
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
h'x : rnDeriv (withDensity μ f) μ x = f x
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
filter_upwards [ae_tendsto_rnDeriv v ρ, rnDeriv_withDensity μ hf] with x hx h'x
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
h'x : rnDeriv (withDensity μ f) μ x = f x
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
h'x : rnDeriv (withDensity μ f) μ x = f x
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
rw [← h'x]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
h'x : rnDeriv (withDensity μ f) μ x = f x
⊢ (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) =ᶠ[filterAt v x] fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
h'x : rnDeriv (withDensity μ f) μ x = f x
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
apply hx.congr' _
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
h'x : rnDeriv (withDensity μ f) μ x = f x
a : Set α
ha : MeasurableSet a
⊢ ↑↑(withDensity μ f) a / ↑↑μ a = (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
h'x : rnDeriv (withDensity μ f) μ x = f x
⊢ (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) =ᶠ[filterAt v x] fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a
filter_upwards [v.eventually_filterAt_measurableSet x] with a ha
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6627850
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ✝ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ✝
f : α → ℝ≥0∞
hf : Measurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
ρ : MeasureTheory.Measure α := withDensity μ f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a => ↑↑(withDensity μ f) a / ↑↑μ a) (filterAt v x) (𝓝 (rnDeriv (withDensity μ f) μ x))
h'x : rnDeriv (withDensity μ f) μ x = f x
a : Set α
ha : MeasurableSet a
⊢ ↑↑(withDensity μ f) a / ↑↑μ a = (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a
rw [← withDensity_apply f ha]