α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
let t := toMeasurable μ s
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
have A :
  ∀ᵐ x ∂μ.restrict s,
    Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x)) := by
  apply ae_mono restrict_le_self
  apply ae_tendsto_measure_inter_div_of_measurableSet
  exact measurableSet_toMeasurable _ _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
have B : ∀ᵐ x ∂μ.restrict s, t.indicator 1 x = (1 : ℝ≥0∞) := by
  refine' ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) _
  filter_upwards [ae_restrict_mem (measurableSet_toMeasurable μ s)] with _ hx
  simp only [hx, Pi.one_apply, indicator_of_mem]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator (toMeasurable μ s) 1 x))
h'x : indicator (toMeasurable μ s) 1 x = 1
⊢ Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
filter_upwards [A, B] with x hx h'x
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
h'x : indicator (toMeasurable μ s) 1 x = 1
⊢ Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator (toMeasurable μ s) 1 x))
h'x : indicator (toMeasurable μ s) 1 x = 1
⊢ Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
rw [h'x] at hx
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
h'x : indicator (toMeasurable μ s) 1 x = 1
⊢ (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) =ᶠ[filterAt v x] fun a => ↑↑μ (s ∩ a) / ↑↑μ a
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
h'x : indicator (toMeasurable μ s) 1 x = 1
⊢ Tendsto (fun a => ↑↑μ (s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
apply hx.congr' _
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
h'x : indicator (toMeasurable μ s) 1 x = 1
a✝ : Set α
ha : MeasurableSet a✝
⊢ ↑↑μ (toMeasurable μ s ∩ a✝) / ↑↑μ a✝ = ↑↑μ (s ∩ a✝) / ↑↑μ a✝
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
h'x : indicator (toMeasurable μ s) 1 x = 1
⊢ (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) =ᶠ[filterAt v x] fun a => ↑↑μ (s ∩ a) / ↑↑μ a
filter_upwards [v.eventually_filterAt_measurableSet x] with _ ha
case h.e_a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
h'x : indicator (toMeasurable μ s) 1 x = 1
a✝ : Set α
ha : MeasurableSet a✝
⊢ ↑↑μ (toMeasurable μ s ∩ a✝) = ↑↑μ (s ∩ a✝)
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
h'x : indicator (toMeasurable μ s) 1 x = 1
a✝ : Set α
ha : MeasurableSet a✝
⊢ ↑↑μ (toMeasurable μ s ∩ a✝) / ↑↑μ a✝ = ↑↑μ (s ∩ a✝) / ↑↑μ a✝
congr 1
no goals
case h.e_a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
B : ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
x : α
hx : Tendsto (fun a => ↑↑μ (toMeasurable μ s ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 1)
h'x : indicator (toMeasurable μ s) 1 x = 1
a✝ : Set α
ha : MeasurableSet a✝
⊢ ↑↑μ (toMeasurable μ s ∩ a✝) = ↑↑μ (s ∩ a✝)
exact measure_toMeasurable_inter_of_sigmaFinite ha _
case a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
⊢ {x | (fun x => Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))) x} ∈ ae μ
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
apply ae_mono restrict_le_self
case a.hs
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
⊢ MeasurableSet t
case a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
⊢ {x | (fun x => Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))) x} ∈ ae μ
apply ae_tendsto_measure_inter_div_of_measurableSet
no goals
case a.hs
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
⊢ MeasurableSet t
exact measurableSet_toMeasurable _ _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ (toMeasurable μ s), indicator t 1 x = 1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, indicator t 1 x = 1
refine' ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) _
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
a✝ : α
hx : a✝ ∈ toMeasurable μ s
⊢ indicator (toMeasurable μ s) 1 a✝ = 1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ (toMeasurable μ s), indicator t 1 x = 1
filter_upwards [ae_restrict_mem (measurableSet_toMeasurable μ s)] with _ hx
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.6387832
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂Measure.restrict μ s, Tendsto (fun a => ↑↑μ (t ∩ a) / ↑↑μ a) (filterAt v x) (𝓝 (indicator t 1 x))
a✝ : α
hx : a✝ ∈ toMeasurable μ s
⊢ indicator (toMeasurable μ s) 1 a✝ = 1
simp only [hx, Pi.one_apply, indicator_of_mem]