α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
⊢ ↑q * ↑↑μ s ≤ ↑↑ρ s
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
⊢ ↑q * ↑↑μ s ≤ ↑↑ρ s
let t := {x : α | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
⊢ ↑q * ↑↑μ s ≤ ↑↑ρ s
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
⊢ ↑q * ↑↑μ s ≤ ↑↑ρ s
have A : μ (tᶜ) = 0 := v.ae_tendsto_limRatioMeas hρ
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑q * ↑↑μ s ≤ ↑↑ρ s

case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
⊢ ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
⊢ ↑q * ↑↑μ s ≤ ↑↑ρ s
suffices H : (q • μ) (s ∩ t) ≤ ρ (s ∩ t)
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
⊢ ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑q * ↑↑μ s ≤ ↑↑ρ s

case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
⊢ ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
exact
  calc
    (q • μ) s = (q • μ) (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ (q • μ) (s ∩ t) + (q • μ) (s ∩ tᶜ) := (measure_union_le _ _)
    _ ≤ ρ (s ∩ t) + q * μ (tᶜ) := by
      apply add_le_add H
      rw [coe_nnreal_smul_apply]
      exact mul_le_mul_left' (measure_mono (inter_subset_right _ _)) _
    _ ≤ ρ s := by
      rw [A, MulZeroClass.mul_zero, add_zero]; exact measure_mono (inter_subset_left _ _)
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
⊢ ∀ (x : α), x ∈ s ∩ t → ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
⊢ ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
refine' v.measure_le_of_frequently_le _ (AbsolutelyContinuous.rfl.smul _) _ _
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
x : α
hx : x ∈ s ∩ t
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
⊢ ∀ (x : α), x ∈ s ∩ t → ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
intro x hx
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in filterAt v x, ↑q < ↑↑ρ a / ↑↑μ a
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
x : α
hx : x ∈ s ∩ t
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
have I : ∀ᶠ a in v.filterAt x, (q : ℝ≥0∞) < ρ a / μ a := (tendsto_order.1 hx.2).1 _ (h hx.1)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in filterAt v x, ↑q < ↑↑ρ a / ↑↑μ a
a : Set α
ha : ↑q < ↑↑ρ a / ↑↑μ a
⊢ ↑↑(q • μ) a ≤ ↑↑ρ a
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in filterAt v x, ↑q < ↑↑ρ a / ↑↑μ a
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
apply I.frequently.mono fun a ha => ?_
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in filterAt v x, ↑q < ↑↑ρ a / ↑↑μ a
a : Set α
ha : ↑q < ↑↑ρ a / ↑↑μ a
⊢ ↑q * ↑↑μ a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in filterAt v x, ↑q < ↑↑ρ a / ↑↑μ a
a : Set α
ha : ↑q < ↑↑ρ a / ↑↑μ a
⊢ ↑↑(q • μ) a ≤ ↑↑ρ a
rw [coe_nnreal_smul_apply]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in filterAt v x, ↑q < ↑↑ρ a / ↑↑μ a
a : Set α
ha : ↑q < ↑↑ρ a / ↑↑μ a
⊢ ↑q * ↑↑μ a ≤ ↑↑ρ a
exact ENNReal.mul_le_of_le_div ha.le
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑↑(q • μ) s = ↑↑(q • μ) (s ∩ t ∪ s ∩ tᶜ)
rw [inter_union_compl]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑↑(q • μ) (s ∩ tᶜ) ≤ ↑q * ↑↑μ (tᶜ)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑↑(q • μ) (s ∩ t) + ↑↑(q • μ) (s ∩ tᶜ) ≤ ↑↑ρ (s ∩ t) + ↑q * ↑↑μ (tᶜ)
apply add_le_add H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑q * ↑↑μ (s ∩ tᶜ) ≤ ↑q * ↑↑μ (tᶜ)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑↑(q • μ) (s ∩ tᶜ) ≤ ↑q * ↑↑μ (tᶜ)
rw [coe_nnreal_smul_apply]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑q * ↑↑μ (s ∩ tᶜ) ≤ ↑q * ↑↑μ (tᶜ)
exact mul_le_mul_left' (measure_mono (inter_subset_right _ _)) _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑↑ρ (s ∩ t) ≤ ↑↑ρ s
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑↑ρ (s ∩ t) + ↑q * ↑↑μ (tᶜ) ≤ ↑↑ρ s
rw [A, MulZeroClass.mul_zero, add_zero]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3960181
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < limRatioMeas v hρ x}
t : Set α := {x | Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))}
A : ↑↑μ (tᶜ) = 0
H : ↑↑(q • μ) (s ∩ t) ≤ ↑↑ρ (s ∩ t)
⊢ ↑↑ρ (s ∩ t) ≤ ↑↑ρ s
exact measure_mono (inter_subset_left _ _)