ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α}, Filter.EventuallyConst s (MeasureTheory.ae μ) → MulAction.aestabilizer G μ s = ⊤
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {x_1 y : G} {s : Set α}, x_1 • s =ᵐ[μ] s → y ∈ Subgroup.zpowers x_1 → y • s =ᵐ[μ] s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] {x_1 y : G} {s : Set α}, x_1 +ᵥ s =ᵐ[μ] s → y ∈ AddSubgroup.zmultiples x_1 → y +ᵥ s =ᵐ[μ] s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {x_1 : G} {s : Set α}, x_1 • s =ᵐ[μ] s → x_1⁻¹ • s =ᵐ[μ] s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] {x_1 : G} {s : Set α}, x_1 +ᵥ s =ᵐ[μ] s → -x_1 +ᵥ s =ᵐ[μ] s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>MeasurableSMul G α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G<GOAL>MeasurableSet (a • s)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>MeasurableVAdd G α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G<GOAL>MeasurableSet (a +ᵥ s)
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>MeasurableSpace G₀<VAR>MeasurableSpace α<VAR>MeasurableSMul G₀ α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>MeasurableSet (a • s)
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Zero α<VAR>MulActionWithZero G₀ α<VAR>MeasurableSpace G₀<VAR>MeasurableSpace α<VAR>MeasurableSMul G₀ α<VAR>MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G₀<GOAL>MeasurableSet (a • s)
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableNeg G<VAR>μ.IsNegInvariant<VAR>f : G → F<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun t => f (-t)) μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableInv G<VAR>μ.IsInvInvariant<VAR>f : G → F<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun t => f t⁻¹) μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Group G<VAR>MeasurableInv G<VAR>f : G → E<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<GOAL>∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>AddGroup G<VAR>MeasurableNeg G<VAR>f : G → E<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<GOAL>∫ (x : G), f (-x) ∂μ = ∫ (x : G), f x ∂μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ.IsAddLeftInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (g + x) ∂μ = ∫ (x : G), f x ∂μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>μ.IsMulLeftInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ.IsAddRightInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (x + g) ∂μ = ∫ (x : G), f x ∂μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>μ.IsMulRightInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ.IsAddRightInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (x - g) ∂μ = ∫ (x : G), f x ∂μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>μ.IsMulRightInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (x / g) ∂μ = ∫ (x : G), f x ∂μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>f : G → E<VAR>g : G<VAR>Group G<VAR>MeasurableMul G<VAR>μ.IsMulLeftInvariant<VAR>hf' : ∀ (x : G), f (g * x) = -f x<GOAL>∫ (x : G), f x ∂μ = 0
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>f : G → E<VAR>g : G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ.IsAddLeftInvariant<VAR>hf' : ∀ (x : G), f (g + x) = -f x<GOAL>∫ (x : G), f x ∂μ = 0
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>f : G → E<VAR>g : G<VAR>Group G<VAR>MeasurableMul G<VAR>μ.IsMulRightInvariant<VAR>hf' : ∀ (x : G), f (x * g) = -f x<GOAL>∫ (x : G), f x ∂μ = 0
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure G<VAR>f : G → E<VAR>g : G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>μ.IsAddRightInvariant<VAR>hf' : ∀ (x : G), f (x + g) = -f x<GOAL>∫ (x : G), f x ∂μ = 0
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>f : G → F<VAR>μ.IsMulLeftInvariant<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (g * t)) μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>f : G → F<VAR>μ.IsAddLeftInvariant<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (g + t)) μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>f : G → F<VAR>μ.IsMulRightInvariant<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (t * g)) μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>f : G → F<VAR>μ.IsAddRightInvariant<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (t + g)) μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>f : G → F<VAR>μ.IsAddRightInvariant<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (t - g)) μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>f : G → F<VAR>μ.IsMulRightInvariant<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (t / g)) μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>MeasurableInv G<VAR>f : G → F<VAR>μ.IsInvInvariant<VAR>μ.IsMulLeftInvariant<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (g / t)) μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>f : G → F<VAR>μ.IsNegInvariant<VAR>μ.IsAddLeftInvariant<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (g - t)) μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>f : G → F<VAR>μ.IsNegInvariant<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (g - t)) μ ↔ MeasureTheory.Integrable f μ
<VAR>G : Type u_4<VAR>F : Type u_6<VAR>MeasurableSpace G<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure G<VAR>Group G<VAR>MeasurableMul G<VAR>MeasurableInv G<VAR>f : G → F<VAR>μ.IsInvInvariant<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Integrable (fun t => f (g / t)) μ ↔ MeasureTheory.Integrable f μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>AddGroup G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>f : G → E<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsNegInvariant<VAR>μ.IsAddLeftInvariant<VAR>x' : G<GOAL>∫ (x : G), f (x' - x) ∂μ = ∫ (x : G), f x ∂μ
<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Group G<VAR>MeasurableMul G<VAR>MeasurableInv G<VAR>f : G → E<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsInvInvariant<VAR>μ.IsMulLeftInvariant<VAR>x' : G<GOAL>∫ (x : G), f (x' / x) ∂μ = ∫ (x : G), f x ∂μ
<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>AddGroup G<VAR>MeasurableSpace α<VAR>AddAction G α<VAR>MeasurableVAdd G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>f : α → E<VAR>g : G<GOAL>∫ (x : α), f (g +ᵥ x) ∂μ = ∫ (x : α), f x ∂μ
<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>MeasurableSpace G<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Group G<VAR>MeasurableSpace α<VAR>MulAction G α<VAR>MeasurableSMul G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>f : α → E<VAR>g : G<GOAL>∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>SecondCountableTopology F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0<GOAL>∃ t A, (∀ (n : ℕ), IsClosed (t n)) ∧ s ⊆ ⋃ n, t n ∧ (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>SecondCountableTopology F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0<GOAL>∃ t A, Pairwise (Disjoint on t) ∧ (∀ (n : ℕ), MeasurableSet (t n)) ∧ s ⊆ ⋃ n, t n ∧ (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<GOAL>∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0, ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<GOAL>∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0, ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>δ : ℝ≥0<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hs : MeasurableSet s<VAR>f' : E → E →L[ℝ] E<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>∀ᵐ (x : E) ∂μ.restrict s, ‖f' x - A‖₊ ≤ δ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : DifferentiableOn ℝ f s<VAR>hs : μ s = 0<GOAL>μ (f '' s) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>R : ℝ<VAR>hs : s ⊆ Metric.closedBall 0 R<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<GOAL>μ (f '' s) ≤ ↑ε * μ (Metric.closedBall 0 R)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>h'f' : ∀ x ∈ s, (f' x).det = 0<GOAL>μ (f '' s) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>AEMeasurable f' (μ.restrict s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>AEMeasurable (fun x => ENNReal.ofReal |(f' x).det|) (μ.restrict s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>AEMeasurable (fun x => |(f' x).det|.toNNReal) (μ.restrict s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<GOAL>MeasurableSet (f '' s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<GOAL>MeasurableEmbedding (s.restrict f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = μ (f '' s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<VAR>h'f : Measurable f<GOAL>MeasureTheory.Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) = μ.restrict (f '' s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<GOAL>MeasureTheory.Measure.map (s.restrict f) (MeasureTheory.Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<VAR>g : E → ℝ≥0∞<GOAL>∫⁻ (x : E) in f '' s, g x ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<VAR>g : E → F<GOAL>MeasureTheory.IntegrableOn g (f '' s) μ ↔ MeasureTheory.IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<VAR>g : E → F<GOAL>∫ (x : E) in f '' s, g x ∂μ = ∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ
<VAR>𝕜 : Type u_3<VAR>NormedField 𝕜<VAR>v : 𝕜<GOAL>(ContinuousLinearMap.smulRight 1 v).det = v
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>s : Set ℝ<VAR>f f' : ℝ → ℝ<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<VAR>g : ℝ → F<GOAL>MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (fun x => |f' x| • g (f x)) s MeasureTheory.volume
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>s : Set ℝ<VAR>f f' : ℝ → ℝ<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>hf : Set.InjOn f s<VAR>g : ℝ → F<GOAL>∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, |f' x| • g (f x)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : PartialHomeomorph E E<VAR>hf' : ∀ x ∈ f.source, HasFDerivAt (↑f) (f' x) x<VAR>g : E → F<GOAL>∫ (x : E) in f.target, g x ∂μ = ∫ (x : E) in f.source, |(f' x).det| • g (↑f x) ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf : MeasurableEmbedding f<VAR>g : E → ℝ<VAR>hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x<VAR>hg_int : MeasureTheory.IntegrableOn g (f '' s) μ<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>(MeasureTheory.Measure.comap f (μ.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>f' : E → E →L[ℝ] E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>f : E ≃ᵐ E<VAR>g : E → ℝ<VAR>hg : ∀ᵐ (x : E) ∂μ, x ∈ ⇑f '' s → 0 ≤ g x<VAR>hg_int : MeasureTheory.IntegrableOn g (⇑f '' s) μ<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt (⇑f) (f' x) s x<GOAL>(MeasureTheory.Measure.map (⇑f.symm) (μ.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)
<VAR>f : ℝ → ℝ<VAR>hf : MeasurableEmbedding f<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>g : ℝ → ℝ<VAR>hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x<VAR>hg_int : MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<GOAL>(MeasureTheory.Measure.comap f (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
<VAR>f : ℝ ≃ᵐ ℝ<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>g : ℝ → ℝ<VAR>hg : ∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x<VAR>hg_int : MeasureTheory.IntegrableOn g (⇑f '' s) MeasureTheory.volume<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f) (f' x) s x<GOAL>(MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
<VAR>f : ℝ → ℝ<VAR>hf : MeasurableEmbedding f<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>g : ℝ → ℝ<VAR>hg : 0 ≤ᵐ[MeasureTheory.volume] g<VAR>hg_int : MeasureTheory.Integrable g MeasureTheory.volume<GOAL>(MeasureTheory.Measure.comap f (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))