ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X ≃ᵢ Y<GOAL>(MeasureTheory.OuterMeasure.map ⇑f) (MeasureTheory.OuterMeasure.mkMetric m) = MeasureTheory.OuterMeasure.mkMetric m
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<GOAL>(MeasureTheory.OuterMeasure.mkMetric m).trim = MeasureTheory.OuterMeasure.mkMetric m
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>μ : MeasureTheory.OuterMeasure X<VAR>r : ℝ≥0∞<VAR>h0 : 0 < r<VAR>hr : ∀ (s : Set X), EMetric.diam s ≤ r → μ s ≤ m (EMetric.diam s)<GOAL>μ ≤ MeasureTheory.OuterMeasure.mkMetric m
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>m : Set X → ℝ≥0∞<GOAL>(MeasureTheory.Measure.mkMetric' m).toOuterMeasure = (MeasureTheory.OuterMeasure.mkMetric' m).trim
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<GOAL>(MeasureTheory.Measure.mkMetric m).toOuterMeasure = MeasureTheory.OuterMeasure.mkMetric m
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<GOAL>⇑(MeasureTheory.OuterMeasure.mkMetric m) = ⇑(MeasureTheory.Measure.mkMetric m)
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>m₁ m₂ : ℝ≥0∞ → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>h0 : c ≠ 0<VAR>hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂<GOAL>MeasureTheory.Measure.mkMetric m₁ ≤ c • MeasureTheory.Measure.mkMetric m₂
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<GOAL>(MeasureTheory.Measure.mkMetric fun x => ⊤) = ⊤
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>m₁ m₂ : ℝ≥0∞ → ℝ≥0∞<VAR>hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂<GOAL>MeasureTheory.Measure.mkMetric m₁ ≤ MeasureTheory.Measure.mkMetric m₂
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>s : Set X<GOAL>(MeasureTheory.Measure.mkMetric m) s = ⨆ r, ⨆ (_ : 0 < r), ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ⨅ (_ : ∀ (n : ℕ), EMetric.diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (EMetric.diam (t n))
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>μ : MeasureTheory.Measure X<VAR>ε : ℝ≥0∞<VAR>h₀ : 0 < ε<VAR>h : ∀ (s : Set X), EMetric.diam s ≤ ε → μ s ≤ m (EMetric.diam s)<GOAL>μ ≤ MeasureTheory.Measure.mkMetric m
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Filter.Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<GOAL>(MeasureTheory.Measure.mkMetric m) s ≤ Filter.liminf (fun n => ∑' (i : ι n), m (EMetric.diam (t n i))) l
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>hι : (n : β) → Fintype (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Filter.Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<GOAL>(MeasureTheory.Measure.mkMetric m) s ≤ Filter.liminf (fun n => ∑ i : ι n, m (EMetric.diam (t n i))) l
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>d : ℝ<VAR>μ : MeasureTheory.Measure X<VAR>ε : ℝ≥0∞<VAR>h₀ : 0 < ε<VAR>h : ∀ (s : Set X), EMetric.diam s ≤ ε → μ s ≤ EMetric.diam s ^ d<GOAL>μ ≤ μH[d]
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>d : ℝ<VAR>s : Set X<GOAL>μH[d] s = ⨆ r, ⨆ (_ : 0 < r), ⨅ t, ⨅ (_ : s ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), EMetric.diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), EMetric.diam (t n) ^ d
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>∀ (n : β), Countable (ι n)<VAR>d : ℝ<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Filter.Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<GOAL>μH[d] s ≤ Filter.liminf (fun n => ∑' (i : ι n), EMetric.diam (t n i) ^ d) l
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>(n : β) → Fintype (ι n)<VAR>d : ℝ<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Filter.Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<GOAL>μH[d] s ≤ Filter.liminf (fun n => ∑ i : ι n, EMetric.diam (t n i) ^ d) l
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ < d₂<VAR>s : Set X<GOAL>μH[d₂] s = 0 ∨ μH[d₁] s = ⊤
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h : d₁ ≤ d₂<VAR>s : Set X<GOAL>μH[d₂] s ≤ μH[d₁] s
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>d : ℝ<VAR>hd : 0 < d<GOAL>MeasureTheory.NoAtoms μH[d]
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>x : X<GOAL>μH[0] {x} = 1
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>s : Set X<VAR>h : s.Nonempty<GOAL>1 ≤ μH[0] s
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>s : Set X<VAR>hs : s.Subsingleton<VAR>d : ℝ<VAR>hd : 0 ≤ d<GOAL>μH[d] s ≤ 1
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>d : ℝ<VAR>hd : 0 ≤ d<GOAL>μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>K : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>h : LipschitzOnWith K f s<VAR>d : ℝ<VAR>hd : 0 ≤ d<GOAL>μH[d] (f '' s) ≤ ↑K ^ d * μH[d] s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>K : ℝ≥0<VAR>f : X → Y<VAR>h : LipschitzWith K f<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>s : Set X<GOAL>μH[d] (f '' s) ≤ ↑K ^ d * μH[d] s
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>r : 𝕜<VAR>hr : r ≠ 0<VAR>s : Set E<GOAL>μH[d] (r • s) = ‖r‖₊ ^ d • μH[d] s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set Y<GOAL>μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>f : X → Y<VAR>K : ℝ≥0<VAR>d : ℝ<VAR>hf : AntilipschitzWith K f<VAR>hd : 0 ≤ d<VAR>s : Set X<GOAL>μH[d] s ≤ ↑K ^ d * μH[d] (f '' s)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>f : X → Y<VAR>d : ℝ<VAR>hf : Isometry f<VAR>hd : 0 ≤ d ∨ Function.Surjective f<VAR>s : Set X<GOAL>μH[d] (f '' s) = μH[d] s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>f : X → Y<VAR>d : ℝ<VAR>hf : Isometry f<VAR>hd : 0 ≤ d ∨ Function.Surjective f<VAR>s : Set Y<GOAL>μH[d] (f ⁻¹' s) = μH[d] (s ∩ Set.range f)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>f : X → Y<VAR>d : ℝ<VAR>hf : Isometry f<VAR>hd : 0 ≤ d ∨ Function.Surjective f<GOAL>MeasureTheory.Measure.map f μH[d] = μH[d].restrict (Set.range f)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>e : X ≃ᵢ Y<VAR>d : ℝ<VAR>s : Set X<GOAL>μH[d] (⇑e '' s) = μH[d] s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>e : X ≃ᵢ Y<VAR>d : ℝ<VAR>s : Set Y<GOAL>μH[d] (⇑e ⁻¹' s) = μH[d] s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>e : X ≃ᵢ Y<VAR>d : ℝ<GOAL>MeasureTheory.Measure.map ⇑e μH[d] = μH[d]
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>e : X ≃ᵢ Y<VAR>d : ℝ<GOAL>MeasureTheory.MeasurePreserving ⇑e μH[d] μH[d]
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>α : Type u_4<VAR>SMul α X<VAR>IsometricSMul α X<VAR>d : ℝ<VAR>c : α<VAR>h : 0 ≤ d ∨ Function.Surjective fun x => c • x<VAR>s : Set X<GOAL>μH[d] (c • s) = μH[d] s
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>α : Type u_4<VAR>VAdd α X<VAR>IsometricVAdd α X<VAR>d : ℝ<VAR>c : α<VAR>h : 0 ≤ d ∨ Function.Surjective fun x => c +ᵥ x<VAR>s : Set X<GOAL>μH[d] (c +ᵥ s) = μH[d] s
<VAR>ι : Type u_4<VAR>Fintype ι<GOAL>μH[↑(Fintype.card ι)] = MeasureTheory.volume
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>Unique ι<VAR>SecondCountableTopology X<VAR>d : ℝ<GOAL>MeasureTheory.MeasurePreserving ⇑(MeasurableEquiv.funUnique ι X) μH[d] μH[d]
<VAR>α : Fin 2 → Type u_4<VAR>(i : Fin 2) → MeasurableSpace (α i)<VAR>(i : Fin 2) → EMetricSpace (α i)<VAR>∀ (i : Fin 2), BorelSpace (α i)<VAR>∀ (i : Fin 2), SecondCountableTopology (α i)<VAR>d : ℝ<GOAL>MeasureTheory.MeasurePreserving ⇑(MeasurableEquiv.piFinTwo α) μH[d] μH[d]
<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>v : E<VAR>s : Set ℝ<GOAL>μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace P<VAR>MetricSpace P<VAR>NormedAddTorsor E P<VAR>BorelSpace P<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>x : P<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>s : Set P<GOAL>μH[d] (⇑(AffineMap.homothety x c) '' s) = ‖c‖₊ ^ d • μH[d] s
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace P<VAR>MetricSpace P<VAR>NormedAddTorsor E P<VAR>BorelSpace P<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>x : P<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>s : Set P<GOAL>μH[d] (⇑(AffineMap.homothety x c) ⁻¹' s) = ‖c‖₊⁻¹ ^ d • μH[d] s
<VAR>E : Type u_5<VAR>P : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace P<VAR>MetricSpace P<VAR>NormedAddTorsor E P<VAR>BorelSpace P<VAR>x y : P<VAR>s : Set ℝ<GOAL>μH[1] (⇑(AffineMap.lineMap x y) '' s) = nndist x y • μH[1] s
<VAR>E : Type u_5<VAR>P : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace P<VAR>MetricSpace P<VAR>NormedAddTorsor E P<VAR>BorelSpace P<VAR>x y : P<GOAL>μH[1] (affineSegment ℝ x y) = edist x y
<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>x y : E<GOAL>μH[1] (segment ℝ x y) = edist x y
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>hμ : MeasureTheory.IsProbabilityMeasure μ<GOAL>↑⟨μ, hμ⟩ = μ
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<GOAL>↑ν = ↑ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<GOAL>Function.Injective MeasureTheory.ProbabilityMeasure.toMeasure
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>⇑μ = fun s => (↑μ s).toNNReal
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>hμ : MeasureTheory.IsProbabilityMeasure μ<GOAL>⇑⟨μ, hμ⟩ = fun s => (μ s).toNNReal
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>hμ : MeasureTheory.IsProbabilityMeasure μ<VAR>s : Set Ω<GOAL>⟨μ, hμ⟩ s = (μ s).toNNReal
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<GOAL>ν Set.univ = 1
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<GOAL>ν Set.univ ≠ 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>⇑μ.toFiniteMeasure = ⇑μ
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<VAR>s : Set Ω<GOAL>μ.toFiniteMeasure s = μ s
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<GOAL>↑ν.toFiniteMeasure = ↑ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<GOAL>⇑ν.toFiniteMeasure = ⇑ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<VAR>s : Set Ω<GOAL>ν.toFiniteMeasure s = ν s
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<VAR>s : Set Ω<GOAL>↑(ν s) = ↑ν s
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<VAR>s₁ s₂ : Set Ω<VAR>h : s₁ ⊆ s₂<GOAL>μ s₁ ≤ μ s₂
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<VAR>s : Set Ω<GOAL>μ s ≤ 1
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>Nonempty Ω
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ ν : MeasureTheory.ProbabilityMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ ν : MeasureTheory.ProbabilityMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>μ.toFiniteMeasure.mass = 1
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>μ.toFiniteMeasure ≠ 0
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>LipschitzWith 1 fun f => μ.toFiniteMeasure.testAgainstNN f
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<GOAL>Continuous MeasureTheory.ProbabilityMeasure.toFiniteMeasure
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>⇑μ.toWeakDualBCNN = μ.toFiniteMeasure.testAgainstNN
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>μ.toWeakDualBCNN f = (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ).toNNReal
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<GOAL>Continuous fun μ => μ.toWeakDualBCNN
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Continuous fun μ => μ.toFiniteMeasure.testAgainstNN f
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<GOAL>Embedding MeasureTheory.ProbabilityMeasure.toFiniteMeasure
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>δ : Type u_2<VAR>F : Filter δ<VAR>μs : δ → MeasureTheory.ProbabilityMeasure Ω<VAR>μ₀ : MeasureTheory.ProbabilityMeasure Ω<GOAL>Filter.Tendsto μs F (𝓝 μ₀) ↔ Filter.Tendsto (MeasureTheory.ProbabilityMeasure.toFiniteMeasure ∘ μs) F (𝓝 μ₀.toFiniteMeasure)
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.ProbabilityMeasure Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>Filter.Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Filter.Tendsto (fun i => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.ProbabilityMeasure Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>Filter.Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ), Filter.Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>s : Set Ω<GOAL>μ s = μ.mass * μ.normalize s
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<GOAL>μ = μ.mass • μ.normalize.toFiniteMeasure
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<VAR>s : Set Ω<GOAL>μ.normalize s = μ.mass⁻¹ * μ s
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<GOAL>μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<GOAL>↑μ.normalize = μ.mass⁻¹ • ↑μ
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>μ.toFiniteMeasure.normalize = μ
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>nonzero : μ ≠ 0<VAR>f : Ω → E<GOAL>MeasureTheory.average (↑μ) f = ∫ (ω : Ω), f ω ∂↑μ.normalize
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>TopologicalSpace Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>TopologicalSpace Ω<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<GOAL>μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μs_lim : Filter.Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)<VAR>mass_lim : Filter.Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Filter.Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μs_lim : Filter.Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Filter.Tendsto (fun i => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μs_lim : Filter.Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)<VAR>mass_lim : Filter.Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<GOAL>Filter.Tendsto μs F (𝓝 μ)
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>μs_lim : Filter.Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<GOAL>Filter.Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
<VAR>Ω : Type u_1<VAR>Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.FiniteMeasure Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → MeasureTheory.FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<GOAL>Filter.Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize) ∧ Filter.Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass) ↔ Filter.Tendsto μs F (𝓝 μ)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<VAR>f : Ω → Ω'<VAR>hf : AEMeasurable f ↑ν<GOAL>↑(ν.map hf) = MeasureTheory.Measure.map f ↑ν
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<VAR>f : Ω → Ω'<VAR>f_aemble : AEMeasurable f ↑ν<VAR>A : Set Ω'<VAR>A_mble : MeasurableSet A<GOAL>↑(ν.map f_aemble) A = ↑ν (f ⁻¹' A)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<VAR>f : Ω → Ω'<VAR>f_aemble : AEMeasurable f ↑ν<VAR>A : Set Ω'<VAR>A_mble : MeasurableSet A<GOAL>(ν.map f_aemble) A = ν (f ⁻¹' A)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>TopologicalSpace Ω'<VAR>BorelSpace Ω'<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>νs : ι → MeasureTheory.ProbabilityMeasure Ω<VAR>ν : MeasureTheory.ProbabilityMeasure Ω<VAR>lim : Filter.Tendsto νs L (𝓝 ν)<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>Filter.Tendsto (fun i => (νs i).map ⋯) L (𝓝 (ν.map ⋯))
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>MeasurableSpace Ω<VAR>MeasurableSpace Ω'<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>TopologicalSpace Ω'<VAR>BorelSpace Ω'<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>Continuous fun ν => ν.map ⋯
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α), ↑(AddAction.aestabilizer G μ s) = {g | g +ᵥ s =ᵐ[μ] s}
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SMulInvariantMeasure G α μ] (s : Set α), ↑(MulAction.aestabilizer G μ s) = {g | g • s =ᵐ[μ] s}
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {g : G} {s : Set α}, g ∈ MulAction.aestabilizer G μ s ↔ g • s =ᵐ[μ] s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] {g : G} {s : Set α}, g ∈ AddAction.aestabilizer G μ s ↔ g +ᵥ s =ᵐ[μ] s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] (s : Set α), MulAction.stabilizer G s ≤ MulAction.aestabilizer G μ s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α), AddAction.stabilizer G s ≤ AddAction.aestabilizer G μ s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ], AddAction.aestabilizer G μ ∅ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ], MulAction.aestabilizer G μ ∅ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ], MulAction.aestabilizer G μ Set.univ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ], AddAction.aestabilizer G μ Set.univ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] {s t : Set α}, s =ᵐ[μ] t → AddAction.aestabilizer G μ s = AddAction.aestabilizer G μ t
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {s t : Set α}, s =ᵐ[μ] t → MulAction.aestabilizer G μ s = MulAction.aestabilizer G μ t