ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hg' : MeasureTheory.Memℒp g p μ<VAR>hui : MeasureTheory.UnifIntegrable f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hui : MeasureTheory.UnifIntegrable f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ<VAR>hf_tendsto : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop (𝓝 0)<GOAL>MeasureTheory.UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hfg : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (𝓝 0)<GOAL>MeasureTheory.UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hui : MeasureTheory.UnifIntegrable f p μ<VAR>hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.TendstoInMeasure μ f Filter.atTop g ∧ MeasureTheory.UnifIntegrable f p μ ↔ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<GOAL>MeasureTheory.UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<GOAL>MeasureTheory.UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>MeasurableSpace α<GOAL>MeasureTheory.UniformIntegrable f p 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f g : ι → α → β<VAR>hf : MeasureTheory.UniformIntegrable f p μ<VAR>hfg : ∀ (n : ι), f n =ᵐ[μ] g n<GOAL>MeasureTheory.UniformIntegrable g p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f g : ι → α → β<VAR>hfg : ∀ (n : ι), f n =ᵐ[μ] g n<GOAL>MeasureTheory.UniformIntegrable f p μ ↔ MeasureTheory.UniformIntegrable g p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>Subsingleton ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp_ne_top : p ≠ ⊤<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.UniformIntegrable (fun x => g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<GOAL>MeasureTheory.UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<GOAL>MeasureTheory.UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)<VAR>hfu : MeasureTheory.UniformIntegrable f p μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>hfu : MeasureTheory.UniformIntegrable f p μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<GOAL>MeasureTheory.UniformIntegrable f p μ ↔ (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) ∧ ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → E<VAR>hf : MeasureTheory.UniformIntegrable f p μ<GOAL>MeasureTheory.UniformIntegrable (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) p μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → ℝ<VAR>hf : MeasureTheory.UniformIntegrable f p μ<GOAL>MeasureTheory.UniformIntegrable (fun n => (∑ i ∈ Finset.range n, f i) / ↑n) p μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ.IsAddLeftInvariant<VAR>f : G → ENNReal<VAR>g : G<GOAL>∫⁻ (x : G), f (g + x) ∂μ = ∫⁻ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>μ.IsMulLeftInvariant<VAR>f : G → ENNReal<VAR>g : G<GOAL>∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>μ.IsMulRightInvariant<VAR>f : G → ENNReal<VAR>g : G<GOAL>∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ.IsAddRightInvariant<VAR>f : G → ENNReal<VAR>g : G<GOAL>∫⁻ (x : G), f (x + g) ∂μ = ∫⁻ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>μ.IsMulRightInvariant<VAR>f : G → ENNReal<VAR>g : G<GOAL>∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ.IsAddRightInvariant<VAR>f : G → ENNReal<VAR>g : G<GOAL>∫⁻ (x : G), f (x - g) ∂μ = ∫⁻ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>μ.IsMulLeftInvariant<VAR>μ.Regular<VAR>NeZero μ<VAR>f : G → ENNReal<VAR>hf : Continuous f<GOAL>∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>μ.IsAddLeftInvariant<VAR>μ.Regular<VAR>NeZero μ<VAR>f : G → ENNReal<VAR>hf : Continuous f<GOAL>∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<GOAL>μ.toFiniteAux s = ∑' (n : ℕ), (2 ^ (n + 1) * (MeasureTheory.sFiniteSeq μ n) Set.univ)⁻¹ * (MeasureTheory.sFiniteSeq μ n) s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<GOAL>μ.toFinite s = (μ.toFiniteAux Set.univ)⁻¹ * μ.toFiniteAux s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<GOAL>MeasureTheory.Measure.toFiniteAux 0 = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<GOAL>MeasureTheory.Measure.toFinite 0 = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ.toFiniteAux = 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ.toFiniteAux Set.univ ≤ 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ.toFinite = 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>n : ℕ<GOAL>(MeasureTheory.sFiniteSeq μ n).AbsolutelyContinuous μ.toFiniteAux
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ.toFiniteAux.AbsolutelyContinuous μ.toFinite
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>n : ℕ<GOAL>(MeasureTheory.sFiniteSeq μ n).AbsolutelyContinuous μ.toFinite
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ.AbsolutelyContinuous μ.toFinite
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ.toFinite.AbsolutelyContinuous μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ.densityToFinite = fun a => ∑' (n : ℕ), (MeasureTheory.sFiniteSeq μ n).rnDeriv μ.toFinite a
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>Measurable μ.densityToFinite
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ.toFinite.withDensity μ.densityToFinite = μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>∀ᵐ (x : α) ∂μ, μ.densityToFinite x < ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>∀ᵐ (x : α) ∂μ, μ.densityToFinite x ≠ ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>MeasurableSet μ.sigmaFiniteSet
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ.restrict μ.sigmaFiniteSetᶜ = ⊤ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>s : Set α<GOAL>(μ.restrict μ.sigmaFiniteSetᶜ) s = 0 ∨ (μ.restrict μ.sigmaFiniteSetᶜ) s = ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>MeasureTheory.SFinite μ<VAR>ht_subset : t ⊆ μ.sigmaFiniteSetᶜ<GOAL>μ t = 0 ∨ μ t = ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>(μ.toFinite.withDensity fun x => if μ.densityToFinite x ≠ ⊤ then μ.densityToFinite x else 1).restrict μ.sigmaFiniteSet = μ.restrict μ.sigmaFiniteSet
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>h : μ μ.sigmaFiniteSetᶜ = 0<GOAL>MeasureTheory.SigmaFinite μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>μ μ.sigmaFiniteSetᶜ = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<GOAL>μ μ.sigmaFiniteSetᶜ = 0 ↔ MeasureTheory.SigmaFinite μ
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>VAdd M α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.VAddInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>SMul M α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.SMulInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun x => c • x) ⁻¹' s) = μ s
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>SMul G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>μ ((fun x => c • x) ⁻¹' s) ≤ μ s
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>VAdd G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>μ ((fun x => c +ᵥ x) ⁻¹' s) ≤ μ s
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>VAdd G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>c : G<GOAL>Filter.Tendsto (fun x => c +ᵥ x) (MeasureTheory.ae μ) (MeasureTheory.ae μ)
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>SMul G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>c : G<GOAL>Filter.Tendsto (fun x => c • x) (MeasureTheory.ae μ) (MeasureTheory.ae μ)
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>VAdd G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>s : Set α<VAR>h : μ s = 0<VAR>c : G<GOAL>μ ((fun x => c +ᵥ x) ⁻¹' s) = 0
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>SMul G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>h : μ s = 0<VAR>c : G<GOAL>μ ((fun x => c • x) ⁻¹' s) = 0
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>VAdd G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>c : G<GOAL>μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>SMul G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>c : G<GOAL>μ ((fun x => c • x) ⁻¹' s) = μ s
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>μ ((fun x => c • x) ⁻¹' s) = μ s
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>μ (c • s) = μ s
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>μ (c +ᵥ s) = μ s
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>c : G<GOAL>μ (c • s) = 0 ↔ μ s = 0
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>s : Set α<VAR>c : G<GOAL>μ (c +ᵥ s) = 0 ↔ μ s = 0
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>s : Set α<VAR>h : μ s = 0<VAR>c : G<GOAL>μ (c +ᵥ s) = 0
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>h : μ s = 0<VAR>c : G<GOAL>μ (c • s) = 0
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>c +ᵥ s ∈ MeasureTheory.ae μ ↔ s ∈ MeasureTheory.ae μ
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>c • s ∈ MeasureTheory.ae μ ↔ s ∈ MeasureTheory.ae μ
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>c : G<GOAL>c +ᵥ MeasureTheory.ae μ = MeasureTheory.ae μ
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>c : G<GOAL>c • MeasureTheory.ae μ = MeasureTheory.ae μ
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>Filter.EventuallyConst (c +ᵥ s) (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>Filter.EventuallyConst (c • s) (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>c : G<VAR>s t : Set α<GOAL>c +ᵥ s ≤ᵐ[μ] c +ᵥ t ↔ s ≤ᵐ[μ] t
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>c : G<VAR>s t : Set α<GOAL>c • s ≤ᵐ[μ] c • t ↔ s ≤ᵐ[μ] t
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>c : G<VAR>s t : Set α<GOAL>c • s =ᵐ[μ] c • t ↔ s =ᵐ[μ] t
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>c : G<VAR>s t : Set α<GOAL>c +ᵥ s =ᵐ[μ] c +ᵥ t ↔ s =ᵐ[μ] t
<VAR>M : Type v<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>MeasurableSpace M<VAR>VAdd M α<VAR>MeasurableVAdd M α<VAR>c : M<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<GOAL>MeasureTheory.MeasurePreserving (fun x => c +ᵥ x) μ μ
<VAR>M : Type v<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>MeasurableSpace M<VAR>SMul M α<VAR>MeasurableSMul M α<VAR>c : M<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<GOAL>MeasureTheory.MeasurePreserving (fun x => c • x) μ μ
<VAR>M : Type v<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>MeasurableSpace M<VAR>VAdd M α<VAR>MeasurableVAdd M α<VAR>c : M<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<GOAL>MeasureTheory.Measure.map (fun x => c +ᵥ x) μ = μ
<VAR>M : Type v<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>MeasurableSpace M<VAR>SMul M α<VAR>MeasurableSMul M α<VAR>c : M<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<GOAL>MeasureTheory.Measure.map (fun x => c • x) μ = μ
<VAR>M : Type uM<VAR>α : Type uα<VAR>β : Type uβ<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>SMul M α<VAR>SMul M β<VAR>MeasurableSMul M β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>f : α → β<VAR>hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a<VAR>hf : Measurable f<GOAL>MeasureTheory.SMulInvariantMeasure M β (MeasureTheory.Measure.map f μ)
<VAR>M : Type uM<VAR>α : Type uα<VAR>β : Type uβ<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>VAdd M α<VAR>VAdd M β<VAR>MeasurableVAdd M β<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>f : α → β<VAR>hsmul : ∀ (m : M) (a : α), f (m +ᵥ a) = m +ᵥ f a<VAR>hf : Measurable f<GOAL>MeasureTheory.VAddInvariantMeasure M β (MeasureTheory.Measure.map f μ)
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>μ : MeasureTheory.Measure α<GOAL>[MeasureTheory.VAddInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c +ᵥ s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c +ᵥ s) = μ s, ∀ (c : G), MeasureTheory.Measure.map (fun x => c +ᵥ x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving (fun x => c +ᵥ x) μ μ].TFAE
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>μ : MeasureTheory.Measure α<GOAL>[MeasureTheory.SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), MeasureTheory.Measure.map (fun x => c • x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving (fun x => c • x) μ μ].TFAE
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>c : G<GOAL>MeasureTheory.NullMeasurableSet (c • s) μ
<VAR>G : Type u<VAR>α : Type w<VAR>m : MeasurableSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>c : G<GOAL>MeasureTheory.NullMeasurableSet (c +ᵥ s) μ