ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Div G<VAR>m : MeasurableSpace α<VAR>f g : α → G<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableDiv₂ G<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (f / g) μ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Div G<VAR>m : MeasurableSpace α<VAR>f g : α → G<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableDiv₂ G<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => f a / g a) μ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Sub G<VAR>m : MeasurableSpace α<VAR>f g : α → G<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSub₂ G<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => f a - g a) μ
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>MeasurableSpace E<VAR>AddGroup E<VAR>MeasurableSingletonClass E<VAR>MeasurableSub₂ E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>MeasurableSet {x | f x = g x}
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>β : Type u_4<VAR>CanonicallyOrderedAddCommMonoid β<VAR>Sub β<VAR>OrderedSub β<GOAL>∀ {x : MeasurableSpace β} [inst : MeasurableSub₂ β] [inst : MeasurableSingletonClass β] {f g : α → β}, Measurable f → Measurable g → MeasurableSet {x | f x = g x}
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_4<VAR>MeasurableSpace E<VAR>AddGroup E<VAR>MeasurableSingletonClass E<VAR>MeasurableSub₂ E<VAR>f g : α → E<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>MeasureTheory.NullMeasurableSet {x | f x = g x} μ
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>MeasurableSpace E<VAR>MeasurableSingletonClass E<VAR>Countable E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>MeasurableSet {x | f x = g x}
<VAR>α : Type u_4<VAR>E : Type u_5<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace E<VAR>AddGroup E<VAR>MeasurableSingletonClass E<VAR>MeasurableSub₂ E<VAR>hm : m ≤ m0<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : f =ᵐ[μ] g<GOAL>f =ᵐ[μ.trim hm] g
<VAR>G : Type u_2<VAR>Neg G<VAR>MeasurableSpace G<VAR>self : MeasurableNeg G<GOAL>Measurable Neg.neg
<VAR>G : Type u_2<VAR>Inv G<VAR>MeasurableSpace G<VAR>self : MeasurableInv G<GOAL>Measurable Inv.inv
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>Neg G<VAR>MeasurableSpace G<VAR>MeasurableNeg G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>hf : Measurable f<GOAL>Measurable fun x => -f x
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>Inv G<VAR>MeasurableSpace G<VAR>MeasurableInv G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>hf : Measurable f<GOAL>Measurable fun x => (f x)⁻¹
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>Neg G<VAR>MeasurableSpace G<VAR>MeasurableNeg G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => -f x) μ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>Inv G<VAR>MeasurableSpace G<VAR>MeasurableInv G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (fun x => (f x)⁻¹) μ
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>G : Type u_4<VAR>Group G<VAR>MeasurableSpace G<VAR>MeasurableInv G<VAR>f : α → G<GOAL>(Measurable fun x => (f x)⁻¹) ↔ Measurable f
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>G : Type u_4<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>MeasurableNeg G<VAR>f : α → G<GOAL>(Measurable fun x => -f x) ↔ Measurable f
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G : Type u_4<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>MeasurableNeg G<VAR>f : α → G<GOAL>AEMeasurable (fun x => -f x) μ ↔ AEMeasurable f μ
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G : Type u_4<VAR>Group G<VAR>MeasurableSpace G<VAR>MeasurableInv G<VAR>f : α → G<GOAL>AEMeasurable (fun x => (f x)⁻¹) μ ↔ AEMeasurable f μ
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>G₀ : Type u_4<VAR>GroupWithZero G₀<VAR>MeasurableSpace G₀<VAR>MeasurableInv G₀<VAR>f : α → G₀<GOAL>(Measurable fun x => (f x)⁻¹) ↔ Measurable f
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G₀ : Type u_4<VAR>GroupWithZero G₀<VAR>MeasurableSpace G₀<VAR>MeasurableInv G₀<VAR>f : α → G₀<GOAL>AEMeasurable (fun x => (f x)⁻¹) μ ↔ AEMeasurable f μ
<VAR>G : Type u_2<VAR>Inv G<VAR>MeasurableSpace G<VAR>MeasurableInv G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>MeasurableSet s⁻¹
<VAR>G : Type u_2<VAR>Neg G<VAR>MeasurableSpace G<VAR>MeasurableNeg G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (-s)
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>InvolutiveInv α<VAR>MeasurableInv α<GOAL>MeasurableEmbedding Inv.inv
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>InvolutiveNeg α<VAR>MeasurableNeg α<GOAL>MeasurableEmbedding Neg.neg
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>CommGroup G<VAR>MeasurableMul₂ G<VAR>MeasurableInv G<VAR>f g : α → G<VAR>hf : Measurable f<GOAL>Measurable (f * g) ↔ Measurable g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>AddCommGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>f g : α → G<VAR>hf : Measurable f<GOAL>Measurable (f + g) ↔ Measurable g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>CommGroup G<VAR>MeasurableMul₂ G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → G<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (f * g) μ ↔ AEMeasurable g μ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>AddCommGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → G<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (f + g) μ ↔ AEMeasurable g μ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>CommGroup G<VAR>MeasurableMul₂ G<VAR>MeasurableInv G<VAR>f g : α → G<VAR>hf : Measurable f<GOAL>Measurable (g * f) ↔ Measurable g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>AddCommGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>f g : α → G<VAR>hf : Measurable f<GOAL>Measurable (g + f) ↔ Measurable g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>AddCommGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → G<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (g + f) μ ↔ AEMeasurable g μ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>CommGroup G<VAR>MeasurableMul₂ G<VAR>MeasurableInv G<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → G<VAR>hf : AEMeasurable f μ<GOAL>AEMeasurable (g * f) μ ↔ AEMeasurable g μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>VAdd M α<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>self : MeasurableVAdd M α<VAR>c : M<GOAL>Measurable fun x => c +ᵥ x
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>VAdd M α<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>self : MeasurableVAdd M α<VAR>x : α<GOAL>Measurable fun x_1 => x_1 +ᵥ x
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>SMul M α<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>self : MeasurableSMul M α<VAR>x : α<GOAL>Measurable fun x_1 => x_1 • x
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>SMul M α<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>self : MeasurableSMul M α<VAR>c : M<GOAL>Measurable fun x => c • x
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>VAdd M α<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>self : MeasurableVAdd₂ M α<GOAL>Measurable (Function.uncurry fun x x_1 => x +ᵥ x_1)
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>SMul M α<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>self : MeasurableSMul₂ M α<GOAL>Measurable (Function.uncurry fun x x_1 => x • x_1)
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>VAdd M β<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>g : α → β<VAR>MeasurableVAdd₂ M β<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun x => f x +ᵥ g x
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>SMul M β<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>g : α → β<VAR>MeasurableSMul₂ M β<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun x => f x • g x
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>VAdd M β<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>g : α → β<VAR>MeasurableVAdd₂ M β<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun x => f x +ᵥ g x) μ
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>SMul M β<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>g : α → β<VAR>MeasurableSMul₂ M β<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun x => f x • g x) μ
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>VAdd M β<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>MeasurableVAdd M β<VAR>hf : Measurable f<VAR>y : β<GOAL>Measurable fun x => f x +ᵥ y
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>SMul M β<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>MeasurableSMul M β<VAR>hf : Measurable f<VAR>y : β<GOAL>Measurable fun x => f x • y
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>VAdd M β<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>MeasurableVAdd M β<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<VAR>y : β<GOAL>AEMeasurable (fun x => f x +ᵥ y) μ
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>SMul M β<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>MeasurableSMul M β<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable f μ<VAR>y : β<GOAL>AEMeasurable (fun x => f x • y) μ
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>VAdd M β<VAR>m : MeasurableSpace α<VAR>g : α → β<VAR>MeasurableVAdd M β<VAR>hg : Measurable g<VAR>c : M<GOAL>Measurable fun x => c +ᵥ g x
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>SMul M β<VAR>m : MeasurableSpace α<VAR>g : α → β<VAR>MeasurableSMul M β<VAR>hg : Measurable g<VAR>c : M<GOAL>Measurable fun x => c • g x
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>SMul M β<VAR>m : MeasurableSpace α<VAR>g : α → β<VAR>MeasurableSMul M β<VAR>hg : Measurable g<VAR>c : M<GOAL>Measurable (c • g)
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>VAdd M β<VAR>m : MeasurableSpace α<VAR>g : α → β<VAR>MeasurableVAdd M β<VAR>hg : Measurable g<VAR>c : M<GOAL>Measurable (c +ᵥ g)
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>SMul M β<VAR>m : MeasurableSpace α<VAR>g : α → β<VAR>MeasurableSMul M β<VAR>μ : MeasureTheory.Measure α<VAR>hg : AEMeasurable g μ<VAR>c : M<GOAL>AEMeasurable (fun x => c • g x) μ
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>VAdd M β<VAR>m : MeasurableSpace α<VAR>g : α → β<VAR>MeasurableVAdd M β<VAR>μ : MeasureTheory.Measure α<VAR>hg : AEMeasurable g μ<VAR>c : M<GOAL>AEMeasurable (fun x => c +ᵥ g x) μ
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>SMul M β<VAR>m : MeasurableSpace α<VAR>g : α → β<VAR>MeasurableSMul M β<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable g μ<VAR>c : M<GOAL>AEMeasurable (c • g) μ
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>VAdd M β<VAR>m : MeasurableSpace α<VAR>g : α → β<VAR>MeasurableVAdd M β<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable g μ<VAR>c : M<GOAL>AEMeasurable (c +ᵥ g) μ
<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>G : Type u_5<VAR>Group G<VAR>MeasurableSpace G<VAR>MulAction G β<VAR>MeasurableSMul G β<VAR>c : G<GOAL>(Measurable fun x => c • f x) ↔ Measurable f
<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>G : Type u_5<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>AddAction G β<VAR>MeasurableVAdd G β<VAR>c : G<GOAL>(Measurable fun x => c +ᵥ f x) ↔ Measurable f
<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>G : Type u_5<VAR>Group G<VAR>MeasurableSpace G<VAR>MulAction G β<VAR>MeasurableSMul G β<VAR>c : G<GOAL>AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ
<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>G : Type u_5<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>AddAction G β<VAR>MeasurableVAdd G β<VAR>c : G<GOAL>AEMeasurable (fun x => c +ᵥ f x) μ ↔ AEMeasurable f μ
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>AddMonoid M<VAR>AddAction M β<VAR>MeasurableVAdd M β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>c : M<VAR>hc : IsAddUnit c<GOAL>(Measurable fun x => c +ᵥ f x) ↔ Measurable f
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>Monoid M<VAR>MulAction M β<VAR>MeasurableSMul M β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>c : M<VAR>hc : IsUnit c<GOAL>(Measurable fun x => c • f x) ↔ Measurable f
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>AddMonoid M<VAR>AddAction M β<VAR>MeasurableVAdd M β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>c : M<VAR>hc : IsAddUnit c<GOAL>AEMeasurable (fun x => c +ᵥ f x) μ ↔ AEMeasurable f μ
<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace β<VAR>Monoid M<VAR>MulAction M β<VAR>MeasurableSMul M β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>c : M<VAR>hc : IsUnit c<GOAL>AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ
<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>G₀ : Type u_6<VAR>GroupWithZero G₀<VAR>MeasurableSpace G₀<VAR>MulAction G₀ β<VAR>MeasurableSMul G₀ β<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>(Measurable fun x => c • f x) ↔ Measurable f
<VAR>β : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace α<VAR>f : α → β<VAR>μ : MeasureTheory.Measure α<VAR>G₀ : Type u_6<VAR>GroupWithZero G₀<VAR>MeasurableSpace G₀<VAR>MulAction G₀ β<VAR>MeasurableSMul G₀ β<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ
<VAR>α : Type u_2<VAR>MeasurableSpace α<GOAL>Measurable AddOpposite.op
<VAR>α : Type u_2<VAR>MeasurableSpace α<GOAL>Measurable MulOpposite.op
<VAR>α : Type u_2<VAR>MeasurableSpace α<GOAL>Measurable AddOpposite.unop
<VAR>α : Type u_2<VAR>MeasurableSpace α<GOAL>Measurable MulOpposite.unop
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, Measurable f<GOAL>Measurable l.sum
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>Monoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, Measurable f<GOAL>Measurable l.prod
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, AEMeasurable f μ<GOAL>AEMeasurable l.sum μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>Monoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, AEMeasurable f μ<GOAL>AEMeasurable l.prod μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, Measurable f<GOAL>Measurable fun x => (List.map (fun f => f x) l).sum
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>Monoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, Measurable f<GOAL>Measurable fun x => (List.map (fun f => f x) l).prod
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>Monoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, AEMeasurable f μ<GOAL>AEMeasurable (fun x => (List.map (fun f => f x) l).prod) μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>AddMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, AEMeasurable f μ<GOAL>AEMeasurable (fun x => (List.map (fun f => f x) l).sum) μ
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>CommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>l : Multiset (α → M)<VAR>hl : ∀ f ∈ l, Measurable f<GOAL>Measurable l.prod
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>AddCommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>l : Multiset (α → M)<VAR>hl : ∀ f ∈ l, Measurable f<GOAL>Measurable l.sum
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>CommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Multiset (α → M)<VAR>hl : ∀ f ∈ l, AEMeasurable f μ<GOAL>AEMeasurable l.prod μ
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>AddCommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Multiset (α → M)<VAR>hl : ∀ f ∈ l, AEMeasurable f μ<GOAL>AEMeasurable l.sum μ
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>AddCommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, Measurable f<GOAL>Measurable fun x => (Multiset.map (fun f => f x) s).sum
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>CommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, Measurable f<GOAL>Measurable fun x => (Multiset.map (fun f => f x) s).prod
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>CommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, AEMeasurable f μ<GOAL>AEMeasurable (fun x => (Multiset.map (fun f => f x) s).prod) μ
<VAR>M : Type u_2<VAR>α : Type u_4<VAR>AddCommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, AEMeasurable f μ<GOAL>AEMeasurable (fun x => (Multiset.map (fun f => f x) s).sum) μ
<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>AddCommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable (∑ i ∈ s, f i)
<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>CommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable (∏ i ∈ s, f i)
<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>CommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable fun a => ∏ i ∈ s, f i a
<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>AddCommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable fun a => ∑ i ∈ s, f i a
<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>CommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<GOAL>AEMeasurable (∏ i ∈ s, f i) μ
<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>AddCommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<GOAL>AEMeasurable (∑ i ∈ s, f i) μ
<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>CommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<GOAL>AEMeasurable (fun a => ∏ i ∈ s, f i a) μ
<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>AddCommMonoid M<VAR>MeasurableSpace M<VAR>MeasurableAdd₂ M<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<GOAL>AEMeasurable (fun a => ∑ i ∈ s, f i a) μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<GOAL>∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f) s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → ℝ≥0∞<VAR>s : Set α<GOAL>(μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>f : α → ℝ≥0∞<GOAL>MeasureTheory.Measure.withDensity 0 f = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : f =ᵐ[μ] g<GOAL>μ.withDensity f = μ.withDensity g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᵐ[μ] g<GOAL>μ.withDensity f ≤ μ.withDensity g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : α → ℝ≥0∞<GOAL>μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>hg : Measurable g<GOAL>μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>(μ + ν).withDensity f = μ.withDensity f + ν.withDensity f
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : ι → MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>(MeasureTheory.Measure.sum μ).withDensity f = MeasureTheory.Measure.sum fun n => (μ n).withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>μ.withDensity (r • f) = r • μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>μ.withDensity (r • f) = r • μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>(r • μ).withDensity f = r • μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>MeasureTheory.IsFiniteMeasure (μ.withDensity f)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>(μ.withDensity f).AbsolutelyContinuous μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.withDensity 0 = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.withDensity 1 = μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<GOAL>(μ.withDensity fun x => c) = c • μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_2<VAR>Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>μ.withDensity (∑' (n : ι), f n) = MeasureTheory.Measure.sum fun n => μ.withDensity (f n)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ≥0∞<GOAL>μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f