case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (filterAt v x) (𝓝 0)
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (filterAt v x) (𝓝 0)
filter_upwards [v.ae_tendsto_lintegral_nnnorm_sub_div hf, v.ae_eventually_measure_pos] with x hx
  h'x
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this :
  Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (ENNReal.toReal 0))
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (filterAt v x) (𝓝 0)
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (filterAt v x) (𝓝 0)
have := (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp hx
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (filterAt v x) (𝓝 0)
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this :
  Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 (ENNReal.toReal 0))
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (filterAt v x) (𝓝 0)
simp only [ENNReal.zero_toReal] at this
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
⊢ (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) =ᶠ[filterAt v x] fun a =>
    ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (filterAt v x) (𝓝 0)
apply Tendsto.congr' _ this
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
⊢ (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) a = ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
⊢ (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) =ᶠ[filterAt v x] fun a =>
    ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
filter_upwards [h'x, v.eventually_measure_lt_top x] with a _ h'a
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
⊢ (ENNReal.toReal (↑↑μ a))⁻¹ * ENNReal.toReal (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) =
    (ENNReal.toReal (↑↑μ a))⁻¹ • ∫ (x_1 : α) in a, ‖f x_1 - f x‖ ∂μ
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
⊢ (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) a = ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
simp only [Function.comp_apply, ENNReal.toReal_div, set_average_eq, div_eq_inv_mul]
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ (ENNReal.toReal (↑↑μ a))⁻¹ * ENNReal.toReal (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) =
    (ENNReal.toReal (↑↑μ a))⁻¹ • ∫ (x_1 : α) in a, ‖f x_1 - f x‖ ∂μ
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
⊢ (ENNReal.toReal (↑↑μ a))⁻¹ * ENNReal.toReal (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) =
    (ENNReal.toReal (↑↑μ a))⁻¹ • ∫ (x_1 : α) in a, ‖f x_1 - f x‖ ∂μ
have A : IntegrableOn (fun y => (‖f y - f x‖₊ : ℝ)) a μ := by
  simp_rw [coe_nnnorm]
  exact (hf.integrableOn.sub (integrableOn_const.2 (Or.inr h'a))).norm
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ ((ENNReal.toReal (↑↑μ a))⁻¹ * ∫ (a : α) in a, ↑‖f a - f x‖₊ ∂μ) =
    (ENNReal.toReal (↑↑μ a))⁻¹ • ∫ (x_1 : α) in a, ‖f x_1 - f x‖ ∂μ

case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ 0 ≤ ∫ (a : α) in a, ↑‖f a - f x‖₊ ∂μ
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ (ENNReal.toReal (↑↑μ a))⁻¹ * ENNReal.toReal (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) =
    (ENNReal.toReal (↑↑μ a))⁻¹ • ∫ (x_1 : α) in a, ‖f x_1 - f x‖ ∂μ
rw [lintegral_coe_eq_integral _ A, ENNReal.toReal_ofReal]
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
⊢ IntegrableOn (fun y => ‖f y - f x‖) a
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
⊢ IntegrableOn (fun y => ↑‖f y - f x‖₊) a
simp_rw [coe_nnnorm]
no goals
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
⊢ IntegrableOn (fun y => ‖f y - f x‖) a
exact (hf.integrableOn.sub (integrableOn_const.2 (Or.inr h'a))).norm
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ ((ENNReal.toReal (↑↑μ a))⁻¹ * ∫ (a : α) in a, ‖f a - f x‖ ∂μ) =
    (ENNReal.toReal (↑↑μ a))⁻¹ • ∫ (x_1 : α) in a, ‖f x_1 - f x‖ ∂μ
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ ((ENNReal.toReal (↑↑μ a))⁻¹ * ∫ (a : α) in a, ↑‖f a - f x‖₊ ∂μ) =
    (ENNReal.toReal (↑↑μ a))⁻¹ • ∫ (x_1 : α) in a, ‖f x_1 - f x‖ ∂μ
simp_rw [coe_nnnorm]
no goals
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ ((ENNReal.toReal (↑↑μ a))⁻¹ * ∫ (a : α) in a, ‖f a - f x‖ ∂μ) =
    (ENNReal.toReal (↑↑μ a))⁻¹ • ∫ (x_1 : α) in a, ‖f x_1 - f x‖ ∂μ
rfl
case h.hf
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ 0 ≤ fun a => ↑‖f a - f x‖₊
case h
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ 0 ≤ ∫ (a : α) in a, ↑‖f a - f x‖₊ ∂μ
apply integral_nonneg
case h.hf
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x✝ : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x✝‖₊ ∂μ) / ↑↑μ a) (filterAt v x✝) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x✝, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x✝‖₊ ∂μ) / ↑↑μ a) (filterAt v x✝) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x✝‖₊) a
x : α
⊢ OfNat.ofNat 0 x ≤ (fun a => ↑‖f a - f x✝‖₊) x
case h.hf
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / ↑↑μ a) (filterAt v x) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a
⊢ 0 ≤ fun a => ↑‖f a - f x‖₊
intro x
no goals
case h.hf
α : Type u_2
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
f : α → E
hf : Integrable f
x✝ : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x✝‖₊ ∂μ) / ↑↑μ a) (filterAt v x✝) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in filterAt v x✝, 0 < ↑↑μ a
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x✝‖₊ ∂μ) / ↑↑μ a) (filterAt v x✝) (𝓝 0)
a : Set α
a✝ : 0 < ↑↑μ a
h'a : ↑↑μ a < ⊤
A : IntegrableOn (fun y => ↑‖f y - f x✝‖₊) a
x : α
⊢ OfNat.ofNat 0 x ≤ (fun a => ↑‖f a - f x✝‖₊) x
exact NNReal.coe_nonneg _