[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
⊢ VitaliFamily μ
[PROOFSTEP]
let R := scalingScaleOf μ (max (4 * K + 3) 3)
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ VitaliFamily μ
[PROOFSTEP]
have Rpos : 0 < R := scalingScaleOf_pos _ _
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
⊢ VitaliFamily μ
[PROOFSTEP]
have A :
  ∀ x : α,
    ∃ᶠ r in 𝓝[>] (0 : ℝ), μ (closedBall x (3 * r)) ≤ scalingConstantOf μ (max (4 * K + 3) 3) * μ (closedBall x r) :=
  by
  intro x
  apply frequently_iff.2 fun {U} hU => ?_
  obtain ⟨ε, εpos, hε⟩ := mem_nhdsWithin_Ioi_iff_exists_Ioc_subset.1 hU
  refine' ⟨min ε R, hε ⟨lt_min εpos Rpos, min_le_left _ _⟩, _⟩
  exact measure_mul_le_scalingConstantOf_mul μ ⟨zero_lt_three, le_max_right _ _⟩ (min_le_right _ _)
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
⊢ ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[Ioi 0] 0,
      ↑↑μ (closedBall x (3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall x r)
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
⊢ ∃ᶠ (r : ℝ) in 𝓝[Ioi 0] 0,
    ↑↑μ (closedBall x (3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall x r)
[PROOFSTEP]
apply frequently_iff.2 fun {U} hU => ?_
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
U : Set ℝ
hU : U ∈ 𝓝[Ioi 0] 0
⊢ ∃ x_1, x_1 ∈ U ∧ ↑↑μ (closedBall x (3 * x_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall x x_1)
[PROOFSTEP]
obtain ⟨ε, εpos, hε⟩ := mem_nhdsWithin_Ioi_iff_exists_Ioc_subset.1 hU
[GOAL]
case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
U : Set ℝ
hU : U ∈ 𝓝[Ioi 0] 0
ε : ℝ
εpos : ε ∈ Ioi 0
hε : Ioc 0 ε ⊆ U
⊢ ∃ x_1, x_1 ∈ U ∧ ↑↑μ (closedBall x (3 * x_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall x x_1)
[PROOFSTEP]
refine' ⟨min ε R, hε ⟨lt_min εpos Rpos, min_le_left _ _⟩, _⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
U : Set ℝ
hU : U ∈ 𝓝[Ioi 0] 0
ε : ℝ
εpos : ε ∈ Ioi 0
hε : Ioc 0 ε ⊆ U
⊢ ↑↑μ (closedBall x (3 * min ε R)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall x (min ε R))
[PROOFSTEP]
exact measure_mul_le_scalingConstantOf_mul μ ⟨zero_lt_three, le_max_right _ _⟩ (min_le_right _ _)
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
A :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[Ioi 0] 0,
      ↑↑μ (closedBall x (3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall x r)
⊢ VitaliFamily μ
[PROOFSTEP]
exact (Vitali.vitaliFamily μ (scalingConstantOf μ (max (4 * K + 3) 3)) A).enlarge (R / 4) (by linarith)
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
A :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[Ioi 0] 0,
      ↑↑μ (closedBall x (3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall x r)
⊢ 0 < R / 4
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
⊢ closedBall y r ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
[PROOFSTEP]
let R := scalingScaleOf μ (max (4 * K + 3) 3)
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ closedBall y r ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
[PROOFSTEP]
simp only [vitaliFamily, VitaliFamily.enlarge, Vitali.vitaliFamily, mem_union, mem_setOf_eq, isClosed_ball,
  true_and_iff, (nonempty_ball.2 rpos).mono ball_subset_interior_closedBall, measurableSet_closedBall]
  /- The measure is doubling on scales smaller than `R`. Therefore, we treat differently small
      and large balls. For large balls, this follows directly from the enlargement we used in the
      definition. -/
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ (∃ r_1,
      closedBall y r ⊆ closedBall x r_1 ∧
        ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
[PROOFSTEP]
by_cases H : closedBall y r ⊆ closedBall x (R / 4)
[GOAL]
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
⊢ (∃ r_1,
      closedBall y r ⊆ closedBall x r_1 ∧
        ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
case neg
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : ¬closedBall y r ⊆ closedBall x (R / 4)
⊢ (∃ r_1,
      closedBall y r ⊆ closedBall x r_1 ∧
        ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : ¬closedBall y r ⊆ closedBall x (R / 4)
⊢ (∃ r_1,
      closedBall y r ⊆ closedBall x r_1 ∧
        ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
[PROOFSTEP]
exact Or.inr H
[GOAL]
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
⊢ (∃ r_1,
      closedBall y r ⊆ closedBall x r_1 ∧
        ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)) ∨
    ¬closedBall y r ⊆ closedBall x (scalingScaleOf μ (max (4 * K + 3) 3) / 4)
[PROOFSTEP]
left
  /- For small balls, there is the difficulty that `r` could be large but still the ball could be
      small, if the annulus `{y | ε ≤ dist y x ≤ R/4}` is empty. We split between the cases `r ≤ R`
      and `r > R`, and use the doubling for the former and rough estimates for the latter. -/
[GOAL]
case pos.h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
⊢ ∃ r_1,
    closedBall y r ⊆ closedBall x r_1 ∧
      ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
rcases le_or_lt r R with (hr | hr)
[GOAL]
case pos.h.inl
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ ∃ r_1,
    closedBall y r ⊆ closedBall x r_1 ∧
      ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
refine' ⟨(K + 1) * r, _⟩
[GOAL]
case pos.h.inl
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r) ∧
    ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
constructor
[GOAL]
case pos.h.inl.left
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r)
[PROOFSTEP]
apply closedBall_subset_closedBall'
[GOAL]
case pos.h.inl.left.h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ r + dist y x ≤ (K + 1) * r
[PROOFSTEP]
rw [dist_comm]
[GOAL]
case pos.h.inl.left.h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ r + dist x y ≤ (K + 1) * r
[PROOFSTEP]
linarith
[GOAL]
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
have I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r) :=
  by
  apply closedBall_subset_closedBall'
  linarith
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
[PROOFSTEP]
apply closedBall_subset_closedBall'
[GOAL]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ 3 * ((K + 1) * r) + dist x y ≤ (4 * K + 3) * r
[PROOFSTEP]
linarith
[GOAL]
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
⊢ ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
have I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r) :=
  by
  apply closedBall_subset_closedBall
  exact mul_le_mul_of_nonneg_right (le_max_left _ _) rpos.le
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
⊢ closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r)
[PROOFSTEP]
apply closedBall_subset_closedBall
[GOAL]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
⊢ (4 * K + 3) * r ≤ max (4 * K + 3) 3 * r
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right (le_max_left _ _) rpos.le
[GOAL]
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r)
⊢ ↑↑μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
apply (measure_mono (I1.trans I2)).trans
[GOAL]
case pos.h.inl.right
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r)
⊢ ↑↑μ (closedBall y (max (4 * K + 3) 3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
exact measure_mul_le_scalingConstantOf_mul _ ⟨zero_lt_three.trans_le (le_max_right _ _), le_rfl⟩ hr
[GOAL]
case pos.h.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ ∃ r_1,
    closedBall y r ⊆ closedBall x r_1 ∧
      ↑↑μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
refine' ⟨R / 4, H, _⟩
[GOAL]
case pos.h.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ ↑↑μ (closedBall x (3 * (R / 4))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
have : closedBall x (3 * (R / 4)) ⊆ closedBall y r :=
  by
  apply closedBall_subset_closedBall'
  have A : y ∈ closedBall y r := mem_closedBall_self rpos.le
  have B := mem_closedBall'.1 (H A)
  linarith
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ closedBall x (3 * (R / 4)) ⊆ closedBall y r
[PROOFSTEP]
apply closedBall_subset_closedBall'
[GOAL]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ 3 * (R / 4) + dist x y ≤ r
[PROOFSTEP]
have A : y ∈ closedBall y r := mem_closedBall_self rpos.le
[GOAL]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
A : y ∈ closedBall y r
⊢ 3 * (R / 4) + dist x y ≤ r
[PROOFSTEP]
have B := mem_closedBall'.1 (H A)
[GOAL]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
A : y ∈ closedBall y r
B : dist x y ≤ R / 4
⊢ 3 * (R / 4) + dist x y ≤ r
[PROOFSTEP]
linarith
[GOAL]
case pos.h.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
this : closedBall x (3 * (R / 4)) ⊆ closedBall y r
⊢ ↑↑μ (closedBall x (3 * (R / 4))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
apply (measure_mono this).trans _
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
this : closedBall x (3 * (R / 4)) ⊆ closedBall y r
⊢ ↑↑μ (closedBall y r) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * ↑↑μ (closedBall y r)
[PROOFSTEP]
refine' le_mul_of_one_le_left (zero_le _) _
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
this : closedBall x (3 * (R / 4)) ⊆ closedBall y r
⊢ 1 ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3))
[PROOFSTEP]
exact ENNReal.one_le_coe_iff.2 (le_max_right _ _)
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
⊢ Tendsto (fun j => closedBall (w j) (δ j)) l (VitaliFamily.filterAt (vitaliFamily μ K) x)
[PROOFSTEP]
refine' (vitaliFamily μ K).tendsto_filterAt_iff.mpr ⟨_, fun ε hε => _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
[PROOFSTEP]
filter_upwards [xmem, δlim self_mem_nhdsWithin] with j hj h'j
[GOAL]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : j ∈ δ ⁻¹' Ioi 0
⊢ closedBall (w j) (δ j) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
[PROOFSTEP]
exact closedBall_mem_vitaliFamily_of_dist_le_mul μ hj h'j
[GOAL]
case refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
[PROOFSTEP]
rcases l.eq_or_neBot with rfl | h
[GOAL]
case refine'_2.inl
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
w : ι → α
δ : ι → ℝ
ε : ℝ
hε : ε > 0
δlim : Tendsto δ ⊥ (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in ⊥, x ∈ closedBall (w j) (K * δ j)
⊢ ∀ᶠ (i : ι) in ⊥, closedBall (w i) (δ i) ⊆ closedBall x ε
[PROOFSTEP]
simp
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
[PROOFSTEP]
have hK : 0 ≤ K := by
  rcases(xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩
  have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩
  exact (mul_nonneg_iff_left_nonneg_of_pos (mem_Ioi.1 h'j)).1 this
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
⊢ 0 ≤ K
[PROOFSTEP]
rcases(xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : δ j ∈ Ioi 0
⊢ 0 ≤ K
[PROOFSTEP]
have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : δ j ∈ Ioi 0
this : 0 ≤ K * δ j
⊢ 0 ≤ K
[PROOFSTEP]
exact (mul_nonneg_iff_left_nonneg_of_pos (mem_Ioi.1 h'j)).1 this
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
[PROOFSTEP]
have δpos := eventually_mem_of_tendsto_nhdsWithin δlim
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
[PROOFSTEP]
replace δlim := tendsto_nhds_of_tendsto_nhdsWithin δlim
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
[PROOFSTEP]
replace hK : 0 < K + 1
[GOAL]
case hK
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
⊢ 0 < K + 1
[PROOFSTEP]
linarith
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
[PROOFSTEP]
apply (((Metric.tendsto_nhds.mp δlim _ (div_pos hε hK)).and δpos).and xmem).mono
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
⊢ ∀ (x_1 : ι),
    (dist (δ x_1) 0 < ε / (K + 1) ∧ δ x_1 ∈ Ioi 0) ∧ x ∈ closedBall (w x_1) (K * δ x_1) →
      closedBall (w x_1) (δ x_1) ⊆ closedBall x ε
[PROOFSTEP]
rintro j ⟨⟨hjε, hj₀ : 0 < δ j⟩, hx⟩ y hy
[GOAL]
case refine'_2.inr.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hjε : dist (δ j) 0 < ε / (K + 1)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
⊢ y ∈ closedBall x ε
[PROOFSTEP]
replace hjε : (K + 1) * δ j < ε := by simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff' hK).mp hjε
[GOAL]
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hjε : dist (δ j) 0 < ε / (K + 1)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
⊢ (K + 1) * δ j < ε
[PROOFSTEP]
simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff' hK).mp hjε
[GOAL]
case refine'_2.inr.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
hjε : (K + 1) * δ j < ε
⊢ y ∈ closedBall x ε
[PROOFSTEP]
simp only [mem_closedBall] at hx hy ⊢
[GOAL]
case refine'_2.inr.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hj₀ : 0 < δ j
y : α
hjε : (K + 1) * δ j < ε
hx : dist x (w j) ≤ K * δ j
hy : dist y (w j) ≤ δ j
⊢ dist y x ≤ ε
[PROOFSTEP]
linarith [dist_triangle_right y x (w j)]
[GOAL]
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : IsUnifLocDoublingMeasure μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
E : Type u_2
inst✝ : NormedAddCommGroup E
S : Set α
K : ℝ
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ S,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[Ioi 0] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j => ↑↑μ (S ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
[PROOFSTEP]
filter_upwards [(vitaliFamily μ K).ae_tendsto_measure_inter_div S] with x hx ι l w δ δlim xmem using
  hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)
[GOAL]
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : IsUnifLocDoublingMeasure μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
E : Type u_2
inst✝ : NormedAddCommGroup E
f : α → E
hf : LocallyIntegrable f
K : ℝ
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[Ioi 0] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j => ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0)
[PROOFSTEP]
filter_upwards [(vitaliFamily μ K).ae_tendsto_average_norm_sub hf] with x hx ι l w δ δlim xmem using
  hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)
[GOAL]
α : Type u_1
inst✝⁸ : MetricSpace α
inst✝⁷ : MeasurableSpace α
μ : Measure α
inst✝⁶ : IsUnifLocDoublingMeasure μ
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : BorelSpace α
inst✝³ : IsLocallyFiniteMeasure μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f
K : ℝ
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[Ioi 0] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j => ⨍ (y : α) in closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x))
[PROOFSTEP]
filter_upwards [(vitaliFamily μ K).ae_tendsto_average hf] with x hx ι l w δ δlim xmem using
  hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)
