ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<VAR>hi4 : IndepFun Xp Yp μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<VAR>hi4 : IndepFun Xp Yp μ<VAR>hl1 : Integrable (Xm * Ym) μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<VAR>hi4 : IndepFun Xp Yp μ<VAR>hl1 : Integrable (Xm * Ym) μ<VAR>hl2 : Integrable (Xp * Ym) μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<VAR>hi4 : IndepFun Xp Yp μ<VAR>hl1 : Integrable (Xm * Ym) μ<VAR>hl2 : Integrable (Xp * Ym) μ<VAR>hl3 : Integrable (Xm * Yp) μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<VAR>hi4 : IndepFun Xp Yp μ<VAR>hl1 : Integrable (Xm * Ym) μ<VAR>hl2 : Integrable (Xp * Ym) μ<VAR>hl3 : Integrable (Xm * Yp) μ<VAR>hl4 : Integrable (Xp * Yp) μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<VAR>hi4 : IndepFun Xp Yp μ<VAR>hl1 : Integrable (Xm * Ym) μ<VAR>hl2 : Integrable (Xp * Ym) μ<VAR>hl3 : Integrable (Xm * Yp) μ<VAR>hl4 : Integrable (Xp * Yp) μ<VAR>hl5 : Integrable (Xp * Yp - Xm * Yp) μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<VAR>hi4 : IndepFun Xp Yp μ<VAR>hl1 : Integrable (Xm * Ym) μ<VAR>hl2 : Integrable (Xp * Ym) μ<VAR>hl3 : Integrable (Xm * Yp) μ<VAR>hl4 : Integrable (Xp * Yp) μ<VAR>hl5 : Integrable (Xp * Yp - Xm * Yp) μ<VAR>hl6 : Integrable (Xp * Ym - Xm * Ym) μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<VAR>hi4 : IndepFun Xp Yp μ<VAR>hl1 : Integrable (Xm * Ym) μ<VAR>hl2 : Integrable (Xp * Ym) μ<VAR>hl3 : Integrable (Xm * Yp) μ<VAR>hl4 : Integrable (Xp * Yp) μ<VAR>hl5 : Integrable (Xp * Yp - Xm * Yp) μ<VAR>hl6 : Integrable (Xp * Ym - Xm * Ym) μ<GOAL>integral μ (Xp * Yp - Xm * Yp - (Xp * Ym - Xm * Ym)) = integral μ (Xp - Xm) * integral μ (Yp - Ym)
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<VAR>hp4 : 0 ≤ Yp<VAR>hm1 : AEMeasurable Xm μ<VAR>hm2 : AEMeasurable Xp μ<VAR>hm3 : AEMeasurable Ym μ<VAR>hm4 : AEMeasurable Yp μ<VAR>hv1 : Integrable Xm μ<VAR>hv2 : Integrable Xp μ<VAR>hv3 : Integrable Ym μ<VAR>hv4 : Integrable Yp μ<VAR>hi1 : IndepFun Xm Ym μ<VAR>hi2 : IndepFun Xp Ym μ<VAR>hi3 : IndepFun Xm Yp μ<VAR>hi4 : IndepFun Xp Yp μ<VAR>hl1 : Integrable (Xm * Ym) μ<VAR>hl2 : Integrable (Xp * Ym) μ<VAR>hl3 : Integrable (Xm * Yp) μ<VAR>hl4 : Integrable (Xp * Yp) μ<VAR>hl5 : Integrable (Xp * Yp - Xm * Yp) μ<VAR>hl6 : Integrable (Xp * Ym - Xm * Ym) μ<GOAL>integral μ Xp * integral μ Yp - integral μ Xm * integral μ Yp - (integral μ Xp * integral μ Ym - integral μ Xm * integral μ Ym) = (∫ (a : Ω), Xp a ∂μ - ∫ (a : Ω), Xm a ∂μ) * (∫ (a : Ω), Yp a ∂μ - ∫ (a : Ω), Ym a ∂μ)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>x✝ : NormalWord d<GOAL>unitsSMul φ (-1) (unitsSMul φ 1 x✝) = x✝
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>w : NormalWord d<GOAL>unitsSMul φ 1 (unitsSMul φ (-1) w) = w
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>w : NormalWord d<GOAL>1 = - -1
<VAR>x y : ℝ<GOAL>sin (3 * x) = 3 * sin x - 4 * sin x ^ 3
<VAR>x y : ℝ<GOAL>↑(sin (3 * x)) = ↑(3 * sin x - 4 * sin x ^ 3)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>b : β<GOAL>dist (f b) (g b) ≤ dist f g
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>(fun x => rexp (-llr μ ν x)) =ᶠ[ae μ] fun x => (ν.rnDeriv μ x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>x : α<VAR>hx : (-llr μ ν) x = llr ν μ x<VAR>hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal<GOAL>rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>x : α<VAR>hx : -llr μ ν x = llr ν μ x<VAR>hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal<GOAL>rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>n : ℕ<GOAL>(p ^ n).degrees ≤ n • p.degrees
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X : Type w'<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : (Z B : C) → (π : Z ⟶ B) → [inst : EffectiveEpi π] → PreservesLimit (cospan π π) G<VAR>hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], QuotientMap ⇑(G.map π)<GOAL>EqualizerCondition (yonedaPresheaf G X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X : Type w'<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : (Z B : C) → (π : Z ⟶ B) → [inst : EffectiveEpi π] → PreservesLimit (cospan π π) G<VAR>hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : EffectiveEpi π], QuotientMap ⇑(G.map π)<GOAL>∀ (X_1 B : C) (π : X_1 ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π], Function.Bijective (MapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : Ring S<VAR>inst✝¹³ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra K E<VAR>A₁ : Type u_8<VAR>B₁ : Type u_9<VAR>A₂ : Type u_10<VAR>B₂ : Type u_11<VAR>inst✝⁵ : CommRing A₁<VAR>inst✝⁴ : Ring B₁<VAR>inst✝³ : CommRing A₂<VAR>inst✝² : Ring B₂<VAR>inst✝¹ : Algebra A₁ B₁<VAR>inst✝ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>x✝ : B₁<VAR>c : A₁<VAR>x : B₂<GOAL>((↑e₂).comp (algebraMap A₁ B₁)) c * x = x * ((↑e₂).comp (algebraMap A₁ B₁)) c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : Ring S<VAR>inst✝¹³ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra K E<VAR>A₁ : Type u_8<VAR>B₁ : Type u_9<VAR>A₂ : Type u_10<VAR>B₂ : Type u_11<VAR>inst✝⁵ : CommRing A₁<VAR>inst✝⁴ : Ring B₁<VAR>inst✝³ : CommRing A₂<VAR>inst✝² : Ring B₂<VAR>inst✝¹ : Algebra A₁ B₁<VAR>inst✝ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>x✝ : B₁<VAR>c : A₁<VAR>x : B₂<GOAL>e₂.symm (((↑e₂).comp (algebraMap A₁ B₁)) c * x) = e₂.symm (x * ((↑e₂).comp (algebraMap A₁ B₁)) c)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝² : IsTrans α r<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Nonempty γ<VAR>f : γ → α<VAR>inst✝ : Finite β<VAR>D : Directed r f<VAR>g : β → γ<GOAL>∃ z, ∀ (i : β), r (f (g i)) (f z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>f✝ g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝ : Archimedean α<VAR>f : ℕ → β<VAR>n : ℕ<VAR>r : α<VAR>hr0 : 0 ≤ r<VAR>hr1 : r < 1<VAR>h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)<GOAL>IsCauSeq abv fun m => ∑ n ∈ range m, f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>f✝ g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝ : Archimedean α<VAR>f : ℕ → β<VAR>n : ℕ<VAR>r : α<VAR>hr0 : 0 ≤ r<VAR>hr1 : r < 1<VAR>h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)<VAR>har1 : |r| < 1<GOAL>IsCauSeq abv fun m => ∑ n ∈ range m, f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>f✝ g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝ : Archimedean α<VAR>f : ℕ → β<VAR>n : ℕ<VAR>r : α<VAR>hr0 : 0 ≤ r<VAR>hr1 : r < 1<VAR>h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)<VAR>har1 : |r| < 1<VAR>m : ℕ<VAR>hmn : n.succ ≤ m<GOAL>abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m