α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
⊢ ∀ᵐ (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.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
have A : (∫⁻ y, hf.mk f y ∂μ) ≠ ∞ := by
  convert h'f using 1
  apply lintegral_congr_ae
  exact hf.ae_eq_mk.symm
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf 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.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
filter_upwards [v.ae_tendsto_lintegral_div' hf.measurable_mk A, hf.ae_eq_mk] with x hx h'x
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (f x))
rw [h'x]
case h.e'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) = fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
convert hx using 1
case h.e'_3.h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a = (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a
case h.e'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ (fun a => (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a) = fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a
ext1 a
case h.e'_3.h.e_a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ (∫⁻ (y : α) in a, f y ∂μ) = ∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ
case h.e'_3.h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ (∫⁻ (y : α) in a, f y ∂μ) / ↑↑μ a = (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a
congr 1
case h.e'_3.h.e_a.h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ (fun a => f a) =ᶠ[ae (Measure.restrict μ a)] fun a => AEMeasurable.mk f hf a
case h.e'_3.h.e_a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ (∫⁻ (y : α) in a, f y ∂μ) = ∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ
apply lintegral_congr_ae
no goals
case h.e'_3.h.e_a.h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
A : (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ (fun a => f a) =ᶠ[ae (Measure.restrict μ a)] fun a => AEMeasurable.mk f hf a
exact ae_restrict_of_ae hf.ae_eq_mk
case h.e'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
⊢ (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) = ∫⁻ (y : α), f y ∂μ
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
⊢ (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) ≠ ⊤
convert h'f using 1
case h.e'_2.h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
⊢ (fun a => AEMeasurable.mk f hf a) =ᶠ[ae μ] fun a => f a
case h.e'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
⊢ (∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ) = ∫⁻ (y : α), f y ∂μ
apply lintegral_congr_ae
no goals
case h.e'_2.h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6865941
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : (∫⁻ (y : α), f y ∂μ) ≠ ⊤
⊢ (fun a => AEMeasurable.mk f hf a) =ᶠ[ae μ] fun a => f a
exact hf.ae_eq_mk.symm