ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ.AbsolutelyContinuous ν<VAR>f g : α → δ<VAR>h' : f =ᵐ[ν] g<GOAL>f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<VAR>ν : MeasureTheory.Measure α<VAR>h' : ν.AbsolutelyContinuous μ<GOAL>MeasureTheory.AEDisjoint ν s t
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<VAR>ν : MeasureTheory.Measure α<VAR>h' : ν ≤ μ<GOAL>MeasureTheory.AEDisjoint ν s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>m0 : MeasurableSpace α<VAR>f : α → β<VAR>μa : autoParam (MeasureTheory.Measure α) _auto✝<VAR>μb : autoParam (MeasureTheory.Measure β) _auto✝¹<VAR>self : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<GOAL>(MeasureTheory.Measure.map f μa).AbsolutelyContinuous μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>m0 : MeasurableSpace α<VAR>f : α → β<VAR>μa : autoParam (MeasureTheory.Measure α) _auto✝<VAR>μb : autoParam (MeasureTheory.Measure β) _auto✝¹<VAR>self : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<GOAL>Measurable f
<VAR>α : Type u_1<VAR>_m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving id μ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>f : α → β<VAR>_m0 : MeasurableSpace α<VAR>hf : Measurable f<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving f μ (MeasureTheory.Measure.map f μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa μa' : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<VAR>ha : μa'.AbsolutelyContinuous μa<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving f μa' μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb μb' : MeasureTheory.Measure β<VAR>f : α → β<VAR>h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<VAR>ha : μb.AbsolutelyContinuous μb'<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving f μa μb'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa μa' : MeasureTheory.Measure α<VAR>μb μb' : MeasureTheory.Measure β<VAR>f : α → β<VAR>ha : μa'.AbsolutelyContinuous μa<VAR>hb : μb.AbsolutelyContinuous μb'<VAR>h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving f μa' μb'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>μc : MeasureTheory.Measure γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : MeasureTheory.Measure.QuasiMeasurePreserving g μb μc<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (g ∘ f) μa μc
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μa : MeasureTheory.Measure α<VAR>f : α → α<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μa<VAR>n : ℕ<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving f^[n] μa μa
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<GOAL>AEMeasurable f μa
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<GOAL>MeasureTheory.ae (MeasureTheory.Measure.map f μa) ≤ MeasureTheory.ae μb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<GOAL>Filter.Tendsto f (MeasureTheory.ae μa) (MeasureTheory.ae μb)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<VAR>p : β → Prop<VAR>hg : ∀ᵐ (x : β) ∂μb, p x<GOAL>∀ᵐ (x : α) ∂μa, p (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<VAR>g₁ g₂ : β → δ<VAR>hg : g₁ =ᵐ[μb] g₂<GOAL>g₁ ∘ f =ᵐ[μa] g₂ ∘ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<VAR>s : Set β<VAR>hs : μb s = 0<GOAL>μa (f ⁻¹' s) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>s t : Set β<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<VAR>h : s ≤ᵐ[μb] t<GOAL>f ⁻¹' s ≤ᵐ[μa] f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μa : MeasureTheory.Measure α<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>s t : Set β<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb<VAR>h : s =ᵐ[μb] t<GOAL>f ⁻¹' s =ᵐ[μa] f ⁻¹' t
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → α<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ<VAR>k : ℕ<VAR>hs : f ⁻¹' s =ᵐ[μ] s<GOAL>f^[k] ⁻¹' s =ᵐ[μ] s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>e : α ≃ α<VAR>he : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e) μ μ<VAR>he' : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) μ μ<VAR>k : ℤ<VAR>hs : ⇑e '' s =ᵐ[μ] s<GOAL>⇑(e ^ k) '' s =ᵐ[μ] s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → α<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' s =ᵐ[μ] s<GOAL>Filter.limsup (fun n => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → α<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' s =ᵐ[μ] s<GOAL>Filter.liminf (fun n => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → α<VAR>h : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s =ᵐ[μ] s<GOAL>∃ t, MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t
<VAR>G : Type u_8<VAR>α : Type u_9<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>g : G<VAR>h_qmp : MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g⁻¹ • x) μ μ<VAR>h_ae_eq : s =ᵐ[μ] t<GOAL>g • s =ᵐ[μ] g • t
<VAR>G : Type u_8<VAR>α : Type u_9<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>g : G<VAR>h_qmp : MeasureTheory.Measure.QuasiMeasurePreserving (fun x => -g +ᵥ x) μ μ<VAR>h_ae_eq : s =ᵐ[μ] t<GOAL>g +ᵥ s =ᵐ[μ] g +ᵥ t
<VAR>G : Type u_8<VAR>α : Type u_9<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ<GOAL>Pairwise (MeasureTheory.AEDisjoint μ on fun g => g • s)
<VAR>G : Type u_8<VAR>α : Type u_9<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s<VAR>h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ<GOAL>Pairwise (MeasureTheory.AEDisjoint μ on fun g => g +ᵥ s)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>s ∈ μ.cofinite ↔ μ sᶜ < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>sᶜ ∈ μ.cofinite ↔ μ s < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in μ.cofinite, p x) ↔ μ {x | ¬p x} < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>h : AEMeasurable f μ<GOAL>MeasureTheory.NullMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>s : Set β<VAR>hf : AEMeasurable f μ<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.NullMeasurableSet (f ⁻¹' s) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>t : Set β<VAR>ht : MeasureTheory.NullMeasurableSet t ν<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν<GOAL>MeasureTheory.NullMeasurableSet (f ⁻¹' t) μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet s μ<VAR>hle : ν.AbsolutelyContinuous μ<GOAL>MeasureTheory.NullMeasurableSet s ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasureTheory.NullMeasurableSet s μ<VAR>hle : ν ≤ μ<GOAL>MeasureTheory.NullMeasurableSet s ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → β<VAR>s t : Set β<VAR>ht : MeasureTheory.AEDisjoint ν s t<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν<GOAL>MeasureTheory.AEDisjoint μ (f ⁻¹' s) (f ⁻¹' t)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.ae μ = ⊥ ↔ μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>(MeasureTheory.ae μ).NeBot ↔ μ ≠ 0
<VAR>α : Type u_1<VAR>_m0 : MeasurableSpace α<GOAL>MeasureTheory.ae 0 = ⊥
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ≤ ν<GOAL>MeasureTheory.ae μ ≤ MeasureTheory.ae ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ) ↔ f ⁻¹' s ∈ MeasureTheory.ae μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<VAR>hs : s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ)<GOAL>f ⁻¹' s ∈ MeasureTheory.ae μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>p : β → Prop<VAR>hp : MeasurableSet {x | p x}<GOAL>(∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>p : β → Prop<VAR>h : ∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y<GOAL>∀ᵐ (x : α) ∂μ, p (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>m0 : MeasurableSpace α<VAR>f : α → β<VAR>hf : MeasurableSet (Set.range f)<VAR>μ : MeasureTheory.Measure α<GOAL>∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, x ∈ Set.range f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Preorder α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hst : ∀ (x : α), ∃ y ∈ s, x ≤ y<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>⨆ x ∈ s, μ (Set.Iic x) = μ Set.univ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>SemilatticeSup α<VAR>NoMaxOrder α<VAR>Filter.atTop.IsCountablyGenerated<VAR>μ : MeasureTheory.Measure α<VAR>a : α<GOAL>Filter.Tendsto (fun x => μ (Set.Ico a x)) Filter.atTop (nhds (μ (Set.Ici a)))
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>SemilatticeInf α<VAR>NoMinOrder α<VAR>Filter.atBot.IsCountablyGenerated<VAR>μ : MeasureTheory.Measure α<VAR>a : α<GOAL>Filter.Tendsto (fun x => μ (Set.Ioc x a)) Filter.atBot (nhds (μ (Set.Iic a)))
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>SemilatticeSup α<VAR>Filter.atTop.IsCountablyGenerated<VAR>μ : MeasureTheory.Measure α<GOAL>Filter.Tendsto (fun x => μ (Set.Iic x)) Filter.atTop (nhds (μ Set.univ))
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>SemilatticeInf α<VAR>h : Filter.atBot.IsCountablyGenerated<VAR>μ : MeasureTheory.Measure α<GOAL>Filter.Tendsto (fun x => μ (Set.Ici x)) Filter.atBot (nhds (μ Set.univ))
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PartialOrder α<VAR>a : α<VAR>ha : μ {a} = 0<GOAL>Set.Iio a =ᵐ[μ] Set.Iic a
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PartialOrder α<VAR>a : α<VAR>ha : μ {a} = 0<GOAL>Set.Ioi a =ᵐ[μ] Set.Ici a
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PartialOrder α<VAR>a b : α<VAR>hb : μ {b} = 0<GOAL>Set.Ioo a b =ᵐ[μ] Set.Ioc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PartialOrder α<VAR>a b : α<VAR>ha : μ {a} = 0<GOAL>Set.Ioc a b =ᵐ[μ] Set.Icc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PartialOrder α<VAR>a b : α<VAR>ha : μ {a} = 0<GOAL>Set.Ioo a b =ᵐ[μ] Set.Ico a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PartialOrder α<VAR>a b : α<VAR>ha : μ {a} = 0<VAR>hb : μ {b} = 0<GOAL>Set.Ioo a b =ᵐ[μ] Set.Icc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PartialOrder α<VAR>a b : α<VAR>hb : μ {b} = 0<GOAL>Set.Ico a b =ᵐ[μ] Set.Icc a b
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>PartialOrder α<VAR>a b : α<VAR>ha : μ {a} = 0<VAR>hb : μ {b} = 0<GOAL>Set.Ico a b =ᵐ[μ] Set.Ioc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : MeasureTheory.Measure α<VAR>s : Set β<GOAL>(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : MeasureTheory.Measure β<GOAL>MeasureTheory.Measure.comap f (μ + ν) = MeasureTheory.Measure.comap f μ + MeasureTheory.Measure.comap f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ ν : MeasureTheory.Measure α<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ.AbsolutelyContinuous ν<GOAL>(MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α ≃ᵐ β<VAR>s : Set β<GOAL>(MeasureTheory.Measure.map (⇑f) μ) s = μ (⇑f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>e : α ≃ᵐ β<GOAL>MeasureTheory.Measure.comap (⇑e.symm) μ = MeasureTheory.Measure.map (⇑e) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>e : β ≃ᵐ α<GOAL>MeasureTheory.Measure.map (⇑e.symm) μ = MeasureTheory.Measure.comap (⇑e) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>e : α ≃ᵐ β<GOAL>MeasureTheory.Measure.map (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) = μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>e : α ≃ᵐ β<GOAL>MeasureTheory.Measure.map (⇑e) (MeasureTheory.Measure.map (⇑e.symm) ν) = ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<GOAL>Function.Injective (MeasureTheory.Measure.map ⇑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>e : α ≃ᵐ β<GOAL>MeasureTheory.Measure.map (⇑e) μ = ν ↔ MeasureTheory.Measure.map (⇑e.symm) ν = μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : α ≃ᵐ β<VAR>μ : MeasureTheory.Measure α<GOAL>Filter.map (⇑f) (MeasureTheory.ae μ) = MeasureTheory.ae (MeasureTheory.Measure.map (⇑f) μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>e : α ≃ᵐ β<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasureTheory.OuterMeasure.toMeasure 0 ⋯ = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>p : Polynomial ℝ<VAR>x : ℝ<GOAL>↑(Polynomial.eval x p) = (Polynomial.aeval ↑x) p
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>RCLike K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>FiniteDimensional K E<GOAL>ProperSpace E
<VAR>K : Type u_1<VAR>RCLike K<GOAL>‖RCLike.reCLM‖ = 1
<VAR>K : Type u_1<VAR>RCLike K<GOAL>‖↑RCLike.conjCLE‖ = 1
<VAR>K : Type u_1<VAR>RCLike K<GOAL>‖RCLike.ofRealCLM‖ = 1
<VAR>K : Type u_1<VAR>RCLike K<VAR>p : Polynomial ℝ<VAR>z : K<GOAL>(Polynomial.aeval ((starRingEnd K) z)) p = (starRingEnd K) ((Polynomial.aeval z) p)
<VAR>K : Type u_1<VAR>RCLike K<VAR>p : Polynomial ℝ<VAR>x : ℝ<GOAL>(Polynomial.aeval ↑x) p = ↑(Polynomial.eval x p)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>k : Set X<VAR>hk : IsCompact k<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>μ.InnerRegularCompactLTTop<VAR>LocallyCompactSpace X<VAR>RegularSpace X<GOAL>μ k = ⨅ f, ⨅ (_ : Continuous f), ⨅ (_ : HasCompactSupport f), ⨅ (_ : Set.EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>LocallyCompactSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : G → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<GOAL>Continuous fun x => ∫ (y : G), g (-y + x) ∂μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>LocallyCompactSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : G → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<GOAL>Continuous fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>MeasureTheory.IsFiniteMeasureOnCompacts ν<VAR>μ.IsMulLeftInvariant<VAR>ν.IsMulRightInvariant<VAR>ν.IsOpenPosMeasure<VAR>f g : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>g_nonneg : 0 ≤ g<VAR>x₀ : G<VAR>g_pos : g x₀ ≠ 0<GOAL>∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>MeasureTheory.IsFiniteMeasureOnCompacts ν<VAR>μ.IsAddLeftInvariant<VAR>ν.IsAddRightInvariant<VAR>ν.IsOpenPosMeasure<VAR>f g : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>g_nonneg : 0 ≤ g<VAR>x₀ : G<VAR>g_pos : g x₀ ≠ 0<GOAL>∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (-z + y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<GOAL>∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<GOAL>∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<GOAL>∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<GOAL>∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.addHaarScalarFactor μ • μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>int_nonzero : ∫ (x : G), f x ∂μ ≠ 0<GOAL>↑(μ'.addHaarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>int_nonzero : ∫ (x : G), f x ∂μ ≠ 0<GOAL>↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<VAR>c : ℝ≥0<GOAL>(c • μ').addHaarScalarFactor μ = c • μ'.addHaarScalarFactor μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>LocallyCompactSpace G<VAR>μ' μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<VAR>c : ℝ≥0<GOAL>(c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<GOAL>μ.addHaarScalarFactor μ = 1
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<GOAL>μ.haarScalarFactor μ = 1
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ ν : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>ν.IsAddHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsAddLeftInvariant<GOAL>μ'.addHaarScalarFactor ν = μ'.addHaarScalarFactor μ * μ.addHaarScalarFactor ν
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ' μ ν : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>ν.IsHaarMeasure<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ'<VAR>μ'.IsMulLeftInvariant<GOAL>μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν