ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, m u = 0<GOAL>m s = 0
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<VAR>hs : m s ≠ 0<GOAL>∃ x ∈ s, ∀ t ∈ 𝓝[s] x, 0 < m t
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : ι → Set α<VAR>l : Filter ι<VAR>l.NeBot<VAR>h0 : Filter.Tendsto (fun k => m ((⋃ n, s n) \ s k)) l (𝓝 0)<GOAL>m (⋃ n, s n) = ⨆ n, m (s n)
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<GOAL>m (⋃ n, s n) = ⨆ n, m (s n)
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>t : Set α<VAR>s : Set α<GOAL>m t ≤ m (t ∩ s) + m (t \ s)
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<VAR>t : Set α<VAR>ht : m t = 0<GOAL>m (s \ t) = m s
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>s₁ s₂ : Set α<VAR>h₁ : m s₁ = 0<VAR>h₂ : m s₂ = 0<GOAL>m (s₁ ∪ s₂) = 0
<VAR>α : Type u_1<GOAL>Function.Injective fun μ s => μ s
<VAR>α : Type u_1<VAR>μ₁ μ₂ : MeasureTheory.OuterMeasure α<VAR>h : ∀ (s : Set α), μ₁ s = μ₂ s<GOAL>μ₁ = μ₂
<VAR>α : Type u_1<VAR>μ₁ μ₂ : MeasureTheory.OuterMeasure α<VAR>h : ∀ (s : Set α), s.Nonempty → μ₁ s = μ₂ s<GOAL>μ₁ = μ₂
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s : Set α<GOAL>s ∈ MeasureTheory.ae μ ↔ μ sᶜ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>p : α → Prop<GOAL>(∀ᵐ (a : α) ∂μ, p a) ↔ μ {a | ¬p a} = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s : Set α<GOAL>sᶜ ∈ MeasureTheory.ae μ ↔ μ s = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>p : α → Prop<GOAL>(∃ᵐ (a : α) ∂μ, p a) ↔ μ {a | p a} ≠ 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s : Set α<GOAL>(∃ᵐ (a : α) ∂μ, a ∈ s) ↔ μ s ≠ 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s : Set α<GOAL>μ s = 0 ↔ ∀ᵐ (a : α) ∂μ, a ∉ s
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>p : α → Prop<VAR>μ : F<GOAL>(∀ (a : α), p a) → ∀ᵐ (a : α) ∂μ, p a
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>ι : Sort u_4<VAR>Countable ι<VAR>p : α → ι → Prop<GOAL>(∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) ↔ ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>ι : Sort u_4<VAR>p : α → ι → Prop<VAR>hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i<VAR>i : ι<GOAL>∀ᵐ (a : α) ∂μ, p a i
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>Countable α<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), μ {x} ≠ 0 → p x
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>p : α → (i : ι) → i ∈ S → Prop<GOAL>(∀ᵐ (x : α) ∂μ, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᵐ (x : α) ∂μ, p x i hi
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>f : α → β<GOAL>f =ᵐ[μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>f g : α → β<VAR>h : f =ᵐ[μ] g<GOAL>g =ᵐ[μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>f g h : α → β<VAR>h₁ : f =ᵐ[μ] g<VAR>h₂ : g =ᵐ[μ] h<GOAL>f =ᵐ[μ] h
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>β : Type u_4<VAR>Preorder β<VAR>f g : α → β<VAR>h : ∀ᵐ (x : α) ∂μ, f x < g x<GOAL>f ≤ᵐ[μ] g
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s : Set α<GOAL>s =ᵐ[μ] ∅ ↔ μ s = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s : Set α<GOAL>s =ᵐ[μ] Set.univ ↔ μ sᶜ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>s ≤ᵐ[μ] t ↔ μ (s \ t) = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t s' t' : Set α<VAR>h : s ≤ᵐ[μ] t<VAR>h' : s' ≤ᵐ[μ] t'<GOAL>s ∩ s' ≤ᵐ[μ] t ∩ t'
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t s' t' : Set α<VAR>h : s ≤ᵐ[μ] t<VAR>h' : s' ≤ᵐ[μ] t'<GOAL>s ∪ s' ≤ᵐ[μ] t ∪ t'
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>s ∪ t =ᵐ[μ] t ↔ μ (s \ t) = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>s \ t =ᵐ[μ] s ↔ μ (s ∩ t) = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>ht : μ t = 0<GOAL>s \ t =ᵐ[μ] s
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>s =ᵐ[μ] t ↔ μ (s \ t) = 0 ∧ μ (t \ s) = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>μ (symmDiff s t) = 0 ↔ s =ᵐ[μ] t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>sᶜ =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>sᶜ =ᵐ[μ] t ↔ s =ᵐ[μ] tᶜ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t s' t' : Set α<VAR>h : s =ᵐ[μ] t<VAR>h' : s' =ᵐ[μ] t'<GOAL>s ∩ s' =ᵐ[μ] t ∩ t'
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t s' t' : Set α<VAR>h : s =ᵐ[μ] t<VAR>h' : s' =ᵐ[μ] t'<GOAL>s ∪ s' =ᵐ[μ] t ∪ t'
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᵐ[μ] Set.univ<GOAL>s ∪ t =ᵐ[μ] Set.univ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᵐ[μ] Set.univ<GOAL>s ∪ t =ᵐ[μ] Set.univ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᵐ[μ] ∅<GOAL>s ∪ t =ᵐ[μ] t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᵐ[μ] ∅<GOAL>s ∪ t =ᵐ[μ] s
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᵐ[μ] Set.univ<GOAL>s ∩ t =ᵐ[μ] t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᵐ[μ] Set.univ<GOAL>s ∩ t =ᵐ[μ] s
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᵐ[μ] ∅<GOAL>s ∩ t =ᵐ[μ] ∅
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᵐ[μ] ∅<GOAL>s ∩ t =ᵐ[μ] ∅
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>M : Type u_4<VAR>One M<VAR>f : α → M<VAR>s : Set α<GOAL>s.mulIndicator f =ᵐ[μ] 1 ↔ μ (s ∩ Function.mulSupport f) = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>M : Type u_4<VAR>Zero M<VAR>f : α → M<VAR>s : Set α<GOAL>s.indicator f =ᵐ[μ] 0 ↔ μ (s ∩ Function.support f) = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>H : s ≤ᵐ[μ] t<GOAL>μ s ≤ μ t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>H : s =ᵐ[μ] t<GOAL>μ s = μ t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>H : s ≤ᵐ[μ] t<VAR>ht : μ t = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᵐ[μ.restrict s] 0<GOAL>μ[f|m] =ᵐ[μ.restrict s] 0
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᵐ[μ.restrict sᶜ] 0<GOAL>μ[s.indicator f|m] =ᵐ[μ] s.indicator (μ[f|m])
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hf_int : MeasureTheory.Integrable f μ<VAR>hs : MeasurableSet s<GOAL>μ[s.indicator f|m] =ᵐ[μ] s.indicator (μ[f|m])
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hs_m : MeasurableSet s<VAR>hf_int : MeasureTheory.Integrable f μ<GOAL>μ.restrict s[f|m] =ᵐ[μ.restrict s] μ[f|m]
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>MeasureTheory.SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<GOAL>μ[f|m] =ᵐ[μ.restrict s] μ[f|m₂]
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<GOAL>∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>x : α<GOAL>∀ᶠ (a : Set α) in v.filterAt x, μ a < ⊤
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>ρ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ν<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a<GOAL>ρ s ≤ ν s
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ⟂ₘ μ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>c d : ℝ≥0<VAR>hcd : c < d<VAR>s : Set α<VAR>hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a<VAR>hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ᵐ (x : α) ∂μ, ∃ c, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p q : ℝ≥0<VAR>hpq : p < q<GOAL>∃ a b, MeasurableSet a ∧ MeasurableSet b ∧ {x | v.limRatio ρ x < ↑p} ⊆ a ∧ {x | ↑q < v.limRatio ρ x} ⊆ b ∧ μ (a ∩ b) = 0
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>AEMeasurable (v.limRatio ρ) μ
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>Measurable (v.limRatioMeas hρ)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}<GOAL>ρ s ≤ ↑p * μ s
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>q : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}<GOAL>↑q * μ s ≤ ρ s
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>μ {x | v.limRatioMeas hρ x = ⊤} = 0
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>ρ {x | v.limRatioMeas hρ x = 0} = 0
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<GOAL>ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>μ.withDensity (v.limRatioMeas hρ) = ρ
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ρ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure ρ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 (s.indicator 1 x))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>s : Set α<GOAL>∀ᵐ (x : α) ∂μ.restrict s, Filter.Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>h'f : MeasureTheory.StronglyMeasurable f<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : α → E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>x : α<VAR>f : α → E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<GOAL>∀ᶠ (a : Set α) in v.filterAt x, MeasureTheory.IntegrableOn f a μ
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : α → E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>SecondCountableTopology α<VAR>BorelSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : α → E<VAR>hf : MeasureTheory.LocallyIntegrable f μ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<GOAL>⇑0 = 0
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<GOAL>⇑(m₁ + m₂) = ⇑m₁ + ⇑m₂
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>(m₁ + m₂) s = m₁ s + m₂ s
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>c : R<VAR>m : MeasureTheory.OuterMeasure α<GOAL>⇑(c • m) = c • ⇑m
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>c : R<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>(c • m) s = c • m s
<VAR>α : Type u_1<GOAL>∀ (a : MeasureTheory.OuterMeasure α) (a_1 : Set α), MeasureTheory.OuterMeasure.coeFnAddMonoidHom a a_1 = a a_1
<VAR>α : Type u_1<GOAL>⊥ = 0
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<GOAL>m Set.univ = 0 ↔ m = 0
<VAR>α : Type u_1<VAR>ms : Set (MeasureTheory.OuterMeasure α)<VAR>s : Set α<GOAL>(sSup ms) s = ⨆ m ∈ ms, m s
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>f : ι → MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>(⨆ i, f i) s = ⨆ i, (f i) s
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>f : ι → MeasureTheory.OuterMeasure α<GOAL>⇑(⨆ i, f i) = ⨆ i, ⇑(f i)
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>(m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>ι : Sort u_4<VAR>f : ι → MeasureTheory.OuterMeasure α<VAR>c : R<GOAL>c • ⨆ i, f i = ⨆ i, c • f i
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<VAR>s₁ s₂ : Set α<VAR>hm : m₁ ≤ m₂<VAR>hs : s₁ ⊆ s₂<GOAL>m₁ s₁ ≤ m₂ s₂
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set β<GOAL>((MeasureTheory.OuterMeasure.map f) m) s = m (f ⁻¹' s)
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.map id) m = m
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β<VAR>g : β → γ<VAR>m : MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.map g) ((MeasureTheory.OuterMeasure.map f) m) = (MeasureTheory.OuterMeasure.map (g ∘ f)) m
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<GOAL>Monotone ⇑(MeasureTheory.OuterMeasure.map f)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<VAR>m m' : MeasureTheory.OuterMeasure α<GOAL>(MeasureTheory.OuterMeasure.map f) (m ⊔ m') = (MeasureTheory.OuterMeasure.map f) m ⊔ (MeasureTheory.OuterMeasure.map f) m'