ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>s : Set G<VAR>MeasurableInv G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsMulLeftInvariant<VAR>ν'.IsMulLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>∀ᵐ (x : G) ∂μ', ν' ((fun y => y * x) ⁻¹' s) < ⊤
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>s : Set G<VAR>MeasurableNeg G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsAddLeftInvariant<VAR>ν'.IsAddLeftInvariant<VAR>sm : MeasurableSet s<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<GOAL>μ' s * ∫⁻ (y : G), f (-y) / ν' ((fun x => x + -y) ⁻¹' s) ∂ν' = ∫⁻ (x : G), f x ∂μ'
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>s : Set G<VAR>MeasurableInv G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsMulLeftInvariant<VAR>ν'.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<GOAL>μ' s * ∫⁻ (y : G), f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = ∫⁻ (x : G), f x ∂μ'
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsAddLeftInvariant<VAR>ν'.IsAddLeftInvariant<VAR>s t : Set G<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>μ' s * ν' t = ν' s * μ' t
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>MeasurableInv G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsMulLeftInvariant<VAR>ν'.IsMulLeftInvariant<VAR>s t : Set G<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>μ' s * ν' t = ν' s * μ' t
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>s : Set G<VAR>MeasurableInv G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsMulLeftInvariant<VAR>ν'.IsMulLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>μ' = (μ' s / ν' s) • ν'
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>s : Set G<VAR>MeasurableNeg G<VAR>μ' ν' : MeasureTheory.Measure G<VAR>MeasureTheory.SigmaFinite μ'<VAR>MeasureTheory.SigmaFinite ν'<VAR>μ'.IsAddLeftInvariant<VAR>ν'.IsAddLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>μ' = (μ' s / ν' s) • ν'
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>ν.IsMulRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 * z.1)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>ν.IsAddRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 + z.1)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 + z.2)) (μ.prod ν) (ν.prod μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>μ.IsMulRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 * z.2)) (μ.prod ν) (ν.prod μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1 + z.2, z.2)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>μ.IsMulRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1 * z.2, z.2)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>ν.IsMulRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 / z.1)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>ν.IsAddRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 - z.1)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 / z.2)) (μ.prod ν) (ν.prod μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 - z.2)) (μ.prod ν) (ν.prod μ)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1 - z.2, z.2)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1 / z.2, z.2)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddRightInvariant<VAR>ν.IsAddRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1 + z.2, -z.1)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulRightInvariant<VAR>ν.IsMulRightInvariant<GOAL>MeasureTheory.MeasurePreserving (fun z => (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddRightInvariant<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving Neg.neg μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulRightInvariant<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving Inv.inv μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g / h) μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g - h) μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g - h) μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g / h) μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddRightInvariant<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 - p.2) (μ.prod ν) μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulRightInvariant<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 / p.2) (μ.prod ν) μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 - p.2) (μ.prod ν) μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ ν : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 / p.2) (μ.prod ν) μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun h => h + g) μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun h => h * g) μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>Group G<VAR>MeasurableMul₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableInv G<VAR>μ.IsMulRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g * h) μ μ
<VAR>G : Type u_1<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>μ : MeasureTheory.Measure G<VAR>MeasureTheory.SFinite μ<VAR>MeasurableNeg G<VAR>μ.IsAddRightInvariant<VAR>g : G<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g + h) μ μ
<VAR>E : Type u_1<VAR>p : ℝ<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hp : 0 < p<GOAL>μ (Metric.ball 0 1) = ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (↑(FiniteDimensional.finrank ℝ E) / p + 1))
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>BorelSpace E<VAR>T2Space E<VAR>ContinuousSMul ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>μ {x | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p) ∂μ) / Real.Gamma (↑(FiniteDimensional.finrank ℝ E) / p + 1))
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>BorelSpace E<VAR>T2Space E<VAR>ContinuousSMul ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>Nontrivial E<VAR>r : ℝ<GOAL>μ {x | g x ≤ r} = μ {x | g x < r}
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>MeasureTheory.volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<GOAL>MeasureTheory.volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<GOAL>MeasureTheory.volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>MeasureTheory.volume {x | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<GOAL>MeasureTheory.volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ (2 * Fintype.card ι) * ENNReal.ofReal ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<GOAL>MeasureTheory.volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * Fintype.card ι) * ENNReal.ofReal ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))
<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>Fintype ι<VAR>x : EuclideanSpace ℝ ι<VAR>r : ℝ<GOAL>MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal (√Real.pi ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / 2 + 1))
<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>Fintype ι<VAR>x : EuclideanSpace ℝ ι<VAR>r : ℝ<GOAL>MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal (√Real.pi ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / 2 + 1))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ FiniteDimensional.finrank ℝ E * ENNReal.ofReal (√Real.pi ^ FiniteDimensional.finrank ℝ E / Real.Gamma (↑(FiniteDimensional.finrank ℝ E) / 2 + 1))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ FiniteDimensional.finrank ℝ E * ENNReal.ofReal (√Real.pi ^ FiniteDimensional.finrank ℝ E / Real.Gamma (↑(FiniteDimensional.finrank ℝ E) / 2 + 1))
<VAR>a : ℂ<VAR>r : ℝ<GOAL>MeasureTheory.volume (Metric.ball a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi
<VAR>a : ℂ<VAR>r : ℝ<GOAL>MeasureTheory.volume (Metric.closedBall a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>p.radius = Filter.liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) Filter.atTop
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddCommMonoid β<GOAL>MeasureTheory.FinMeasAdditive μ 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddCommMonoid β<VAR>T T' : Set α → β<VAR>hT : MeasureTheory.FinMeasAdditive μ T<VAR>hT' : MeasureTheory.FinMeasAdditive μ T'<GOAL>MeasureTheory.FinMeasAdditive μ (T + T')
<VAR>α : Type u_1<VAR>𝕜 : Type u_6<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddCommMonoid β<VAR>T : Set α → β<VAR>Monoid 𝕜<VAR>DistribMulAction 𝕜 β<VAR>hT : MeasureTheory.FinMeasAdditive μ T<VAR>c : 𝕜<GOAL>MeasureTheory.FinMeasAdditive μ fun s => c • T s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddCommMonoid β<VAR>T : Set α → β<VAR>μ' : MeasureTheory.Measure α<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s = ⊤ → μ' s = ⊤<VAR>hT : MeasureTheory.FinMeasAdditive μ T<GOAL>MeasureTheory.FinMeasAdditive μ' T
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddCommMonoid β<VAR>T : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : MeasureTheory.FinMeasAdditive (c • μ) T<GOAL>MeasureTheory.FinMeasAdditive μ T
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddCommMonoid β<VAR>T : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_zero : c ≠ 0<VAR>hT : MeasureTheory.FinMeasAdditive μ T<GOAL>MeasureTheory.FinMeasAdditive (c • μ) T
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddCommMonoid β<VAR>T : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_zero : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<GOAL>MeasureTheory.FinMeasAdditive (c • μ) T ↔ MeasureTheory.FinMeasAdditive μ T
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>AddCancelMonoid β<VAR>T : Set α → β<VAR>hT : MeasureTheory.FinMeasAdditive μ T<GOAL>T ∅ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>AddCommMonoid β<VAR>T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<VAR>hSp : ∀ i ∈ sι, μ (S i) ≠ ⊤<VAR>h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)<GOAL>T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>SeminormedAddCommGroup β<VAR>C : ℝ<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hC : 0 ≤ C<GOAL>MeasureTheory.DominatedFinMeasAdditive μ 0 C
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>NormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs_zero : μ s = 0<GOAL>T s = 0
<VAR>α : Type u_1<VAR>β : Type u_8<VAR>NormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>m : MeasurableSpace α<VAR>hT : MeasureTheory.DominatedFinMeasAdditive 0 T C<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>T s = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<GOAL>MeasureTheory.DominatedFinMeasAdditive μ (T + T') (C + C')
<VAR>α : Type u_1<VAR>𝕜 : Type u_6<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>SeminormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 β<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>c : 𝕜<GOAL>MeasureTheory.DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>SeminormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>μ' : MeasureTheory.Measure α<VAR>h : μ ≤ μ'<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hC : 0 ≤ C<GOAL>MeasureTheory.DominatedFinMeasAdditive μ' T C
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>SeminormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<GOAL>∀ {x : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), MeasureTheory.DominatedFinMeasAdditive μ T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive (μ + ν) T C
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>SeminormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<GOAL>∀ {x : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), MeasureTheory.DominatedFinMeasAdditive ν T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive (μ + ν) T C
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>SeminormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : MeasureTheory.DominatedFinMeasAdditive (c • μ) T C<GOAL>MeasureTheory.DominatedFinMeasAdditive μ T (c.toReal * C)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>SeminormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>μ' : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>h : μ ≤ c • μ'<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hC : 0 ≤ C<GOAL>MeasureTheory.DominatedFinMeasAdditive μ' T (c.toReal * C)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α F<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc 0 f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F' : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>T : Set α → E →L[ℝ] F'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T f = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>T : Set α → F →L[ℝ] F'<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T 0 = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>T : Set α → F →L[ℝ] F'<VAR>f : MeasureTheory.SimpleFunc α F<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x ∈ Finset.filter (fun x => x ≠ 0) f.range, (T (↑f ⁻¹' {x})) x
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f : MeasureTheory.SimpleFunc α G<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.map g f) = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f g : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>hg : MeasureTheory.Integrable (↑g) μ<VAR>h : Pairwise fun x y => T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T f = MeasureTheory.SimpleFunc.setToSimpleFunc T g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f g : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>h : ↑f =ᵐ[μ] ↑g<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T f = MeasureTheory.SimpleFunc.setToSimpleFunc T g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>T T' : Set α → E →L[ℝ] F<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T f = MeasureTheory.SimpleFunc.setToSimpleFunc T' f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>T T' : Set α → F →L[ℝ] F'<VAR>f : MeasureTheory.SimpleFunc α F<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc (T + T') f = MeasureTheory.SimpleFunc.setToSimpleFunc T f + MeasureTheory.SimpleFunc.setToSimpleFunc T' f