α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 0)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 0)
have A : ∀ ε > (0 : ℝ≥0), ∀ᵐ x ∂μ, ∀ᶠ a in v.filterAt x, ρ a < ε * μ a := by
  intro ε εpos
  set s := {x | ¬∀ᶠ a in v.filterAt x, ρ a < ε * μ a} with hs
  change μ s = 0
  obtain ⟨o, _, ρo, μo⟩ : ∃ o : Set α, MeasurableSet o ∧ ρ o = 0 ∧ μ (oᶜ) = 0 := hρ
  apply le_antisymm _ bot_le
  calc
    μ s ≤ μ (s ∩ o ∪ oᶜ) := by
      conv_lhs => rw [← inter_union_compl s o]
      exact measure_mono (union_subset_union_right _ (inter_subset_right _ _))
    _ ≤ μ (s ∩ o) + μ (oᶜ) := (measure_union_le _ _)
    _ = μ (s ∩ o) := by rw [μo, add_zero]
    _ = (ε : ℝ≥0∞)⁻¹ * (ε • μ) (s ∩ o) := by
      simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]
      rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
    _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ (s ∩ o) := by
      refine' mul_le_mul_left' _ _
      refine' v.measure_le_of_frequently_le ρ ((Measure.AbsolutelyContinuous.refl μ).smul ε) _ _
      intro x hx
      rw [hs] at hx
      simp only [mem_inter_iff, not_lt, not_eventually, mem_setOf_eq] at hx
      exact hx.1
    _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ o := (mul_le_mul_left' (measure_mono (inter_subset_right _ _)) _)
    _ = 0 := by rw [ρo, MulZeroClass.mul_zero]
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 0)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 0)
obtain ⟨u, _, u_pos, u_lim⟩ :
  ∃ u : ℕ → ℝ≥0, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
  exists_seq_strictAnti_tendsto (0 : ℝ≥0)
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 0)
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 0)
have B : ∀ᵐ x ∂μ, ∀ n, ∀ᶠ a in v.filterAt x, ρ a < u n * μ a :=
  ae_all_iff.2 fun n => A (u n) (u_pos n)
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
⊢ ∀ (a : α),
    (∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v a, ↑↑ρ a < ↑(u n) * ↑↑μ a) →
      (∀ᶠ (a : Set α) in filterAt v a, 0 < ↑↑μ a) → Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 0)
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 0)
filter_upwards [B, v.ae_eventually_measure_pos]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
⊢ Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 0)
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
⊢ ∀ (a : α),
    (∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v a, ↑↑ρ a < ↑(u n) * ↑↑μ a) →
      (∀ᶠ (a : Set α) in filterAt v a, 0 < ↑↑μ a) → Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 0)
intro x hx h'x
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
⊢ ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < z
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
⊢ Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 0)
refine' tendsto_order.2 ⟨fun z hz => (ENNReal.not_lt_zero hz).elim, fun z hz => _⟩
case h.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
⊢ ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < z
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
⊢ ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < z
obtain ⟨w, w_pos, w_lt⟩ : ∃ w : ℝ≥0, (0 : ℝ≥0∞) < w ∧ (w : ℝ≥0∞) < z :=
  ENNReal.lt_iff_exists_nnreal_btwn.1 hz
case h.intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
⊢ ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < z
case h.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
⊢ ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < z
obtain ⟨n, hn⟩ : ∃ n, u n < w := ((tendsto_order.1 u_lim).2 w (ENNReal.coe_pos.1 w_pos)).exists
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
⊢ ∀ (a : Set α), ↑↑ρ a < ↑(u n) * ↑↑μ a → 0 < ↑↑μ a → ↑↑μ a < ⊤ → ↑↑ρ a / ↑↑μ a < z
case h.intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
⊢ ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < z
filter_upwards [hx n, h'x, v.eventually_measure_lt_top x]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
a : Set α
ha : ↑↑ρ a < ↑(u n) * ↑↑μ a
μa_pos : 0 < ↑↑μ a
μa_lt_top : ↑↑μ a < ⊤
⊢ ↑↑ρ a / ↑↑μ a < z
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
⊢ ∀ (a : Set α), ↑↑ρ a < ↑(u n) * ↑↑μ a → 0 < ↑↑μ a → ↑↑μ a < ⊤ → ↑↑ρ a / ↑↑μ a < z
intro a ha μa_pos μa_lt_top
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
a : Set α
ha : ↑↑ρ a < ↑(u n) * ↑↑μ a
μa_pos : 0 < ↑↑μ a
μa_lt_top : ↑↑μ a < ⊤
⊢ ↑↑ρ a < z * ↑↑μ a
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
a : Set α
ha : ↑↑ρ a < ↑(u n) * ↑↑μ a
μa_pos : 0 < ↑↑μ a
μa_lt_top : ↑↑μ a < ⊤
⊢ ↑↑ρ a / ↑↑μ a < z
rw [ENNReal.div_lt_iff (Or.inl μa_pos.ne') (Or.inl μa_lt_top.ne)]
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑(u n) * ↑↑μ a
h'x : ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
a : Set α
ha : ↑↑ρ a < ↑(u n) * ↑↑μ a
μa_pos : 0 < ↑↑μ a
μa_lt_top : ↑↑μ a < ⊤
⊢ ↑↑ρ a < z * ↑↑μ a
exact ha.trans_le (mul_le_mul_right' ((ENNReal.coe_le_coe.2 hn.le).trans w_lt.le) _)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
⊢ ∀ (ε : ℝ≥0), ε > 0 → ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
intro ε εpos
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
set s := {x | ¬∀ᶠ a in v.filterAt x, ρ a < ε * μ a} with hs
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
⊢ ↑↑μ s = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a
change μ s = 0
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ s = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
⊢ ↑↑μ s = 0
obtain ⟨o, _, ρo, μo⟩ : ∃ o : Set α, MeasurableSet o ∧ ρ o = 0 ∧ μ (oᶜ) = 0 := hρ
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ s ≤ ⊥
case intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ s = 0
apply le_antisymm _ bot_le
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ s ≤ ⊥
calc
  μ s ≤ μ (s ∩ o ∪ oᶜ) := by
    conv_lhs => rw [← inter_union_compl s o]
    exact measure_mono (union_subset_union_right _ (inter_subset_right _ _))
  _ ≤ μ (s ∩ o) + μ (oᶜ) := (measure_union_le _ _)
  _ = μ (s ∩ o) := by rw [μo, add_zero]
  _ = (ε : ℝ≥0∞)⁻¹ * (ε • μ) (s ∩ o) := by
    simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]
    rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
  _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ (s ∩ o) := by
    refine' mul_le_mul_left' _ _
    refine' v.measure_le_of_frequently_le ρ ((Measure.AbsolutelyContinuous.refl μ).smul ε) _ _
    intro x hx
    rw [hs] at hx
    simp only [mem_inter_iff, not_lt, not_eventually, mem_setOf_eq] at hx
    exact hx.1
  _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ o := (mul_le_mul_left' (measure_mono (inter_subset_right _ _)) _)
  _ = 0 := by rw [ρo, MulZeroClass.mul_zero]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ (s ∩ o ∪ s ∩ oᶜ) ≤ ↑↑μ (s ∩ o ∪ oᶜ)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ s ≤ ↑↑μ (s ∩ o ∪ oᶜ)
conv_lhs => rw [← inter_union_compl s o]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ (s ∩ o ∪ s ∩ oᶜ) ≤ ↑↑μ (s ∩ o ∪ oᶜ)
exact measure_mono (union_subset_union_right _ (inter_subset_right _ _))
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ (s ∩ o) + ↑↑μ (oᶜ) = ↑↑μ (s ∩ o)
rw [μo, add_zero]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ ({x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a} ∩ o) =
    ↑ε * (↑ε)⁻¹ * ↑↑μ ({x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a} ∩ o)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ (s ∩ o) = (↑ε)⁻¹ * ↑↑(ε • μ) (s ∩ o)
simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑μ ({x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a} ∩ o) =
    ↑ε * (↑ε)⁻¹ * ↑↑μ ({x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a} ∩ o)
rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑(ε • μ) (s ∩ o) ≤ ↑↑ρ (s ∩ o)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ (↑ε)⁻¹ * ↑↑(ε • μ) (s ∩ o) ≤ (↑ε)⁻¹ * ↑↑ρ (s ∩ o)
refine' mul_le_mul_left' _ _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ∀ (x : α), x ∈ s ∩ o → ∃ᶠ (a : Set α) in filterAt v x, ↑↑(ε • μ) a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ↑↑(ε • μ) (s ∩ o) ≤ ↑↑ρ (s ∩ o)
refine' v.measure_le_of_frequently_le ρ ((Measure.AbsolutelyContinuous.refl μ).smul ε) _ _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
x : α
hx : x ∈ s ∩ o
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(ε • μ) a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ ∀ (x : α), x ∈ s ∩ o → ∃ᶠ (a : Set α) in filterAt v x, ↑↑(ε • μ) a ≤ ↑↑ρ a
intro x hx
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
x : α
hx : x ∈ {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a} ∩ o
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(ε • μ) a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
x : α
hx : x ∈ s ∩ o
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(ε • μ) a ≤ ↑↑ρ a
rw [hs] at hx
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
x : α
hx : (∃ᶠ (x : Set α) in filterAt v x, ↑ε * ↑↑μ x ≤ ↑↑ρ x) ∧ x ∈ o
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(ε • μ) a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
x : α
hx : x ∈ {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a} ∩ o
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(ε • μ) a ≤ ↑↑ρ a
simp only [mem_inter_iff, not_lt, not_eventually, mem_setOf_eq] at hx
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
x : α
hx : (∃ᶠ (x : Set α) in filterAt v x, ↑ε * ↑↑μ x ≤ ↑↑ρ x) ∧ x ∈ o
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(ε • μ) a ≤ ↑↑ρ a
exact hx.1
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.1306254
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, ↑↑ρ a < ↑ε * ↑↑μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ↑↑ρ o = 0
μo : ↑↑μ (oᶜ) = 0
⊢ (↑ε)⁻¹ * ↑↑ρ o = 0
rw [ρo, MulZeroClass.mul_zero]