ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s✝<VAR>hs₂ : IsOpen s✝<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s✝ t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s✝<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>f : E →L[ℝ] ℝ<VAR>s : ℝ<VAR>hf₁ : ∀ a ∈ s✝, f a < s<VAR>hf₂ : ∀ b ∈ t, s ≤ f b<GOAL>∃ f u, (∀ a ∈ s✝, f a < u) ∧ ∀ b ∈ t, u < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s✝<VAR>hs₂ : IsOpen s✝<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s✝ t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s✝<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>f : E →L[ℝ] ℝ<VAR>s : ℝ<VAR>hf₁ : ∀ a ∈ s✝, f a < s<VAR>hf₂ : ∀ b ∈ t, s ≤ f b<VAR>hf : IsOpenMap ⇑f<GOAL>∃ f u, (∀ a ∈ s✝, f a < u) ∧ ∀ b ∈ t, u < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s✝<VAR>hs₂ : IsOpen s✝<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s✝ t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s✝<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>f : E →L[ℝ] ℝ<VAR>s : ℝ<VAR>hf₁ : ∀ a ∈ s✝, f a < s<VAR>hf₂ : ∀ b ∈ t, s ≤ f b<VAR>hf : IsOpenMap ⇑f<GOAL>⇑f '' t ⊆ Ioi s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s✝<VAR>hs₂ : IsOpen s✝<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s✝ t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s✝<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>f : E →L[ℝ] ℝ<VAR>s : ℝ<VAR>hf₁ : ∀ a ∈ s✝, f a < s<VAR>hf₂ : ∀ b ∈ t, s ≤ f b<VAR>hf : IsOpenMap ⇑f<GOAL>⇑f '' t ⊆ interior (Ici s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s✝<VAR>hs₂ : IsOpen s✝<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s✝ t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s✝<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>f : E →L[ℝ] ℝ<VAR>s : ℝ<VAR>hf₁ : ∀ a ∈ s✝, f a < s<VAR>hf₂ : ∀ b ∈ t, s ≤ f b<VAR>hf : IsOpenMap ⇑f<GOAL>f ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s✝<VAR>hs₂ : IsOpen s✝<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s✝ t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s✝<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>s : ℝ<VAR>hf₁ : ∀ a ∈ s✝, 0 a < s<VAR>hf₂ : ∀ b ∈ t, s ≤ 0 b<VAR>hf : IsOpenMap ⇑0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s✝<VAR>hs₂ : IsOpen s✝<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s✝ t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s✝<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>s : ℝ<VAR>hf₁ : ∀ a ∈ s✝, 0 < s<VAR>hf₂ : ∀ b ∈ t, s ≤ 0<VAR>hf : IsOpenMap ⇑0<GOAL>False
<VAR>α : Type u<VAR>n : ℕ<GOAL>finRange n.succ = 0 :: map Fin.succ (finRange n)
<VAR>α : Type u<VAR>n : ℕ<GOAL>map Fin.val (finRange n.succ) = map Fin.val (0 :: map Fin.succ (finRange n))
<VAR>α : Type u<VAR>n : ℕ<GOAL>0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map (Fin.val ∘ Fin.succ) (finRange n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>inst✝ : DecidableEq β<VAR>b : β<VAR>h : b ∉ s<GOAL>(insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>MulOpposite.op ((∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = MulOpposite.op (x ^ n - y ^ (n - m) * x ^ m)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(MulOpposite.op x - MulOpposite.op y) * ∑ x_1 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 = MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>this : ∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)<GOAL>(MulOpposite.op x - MulOpposite.op y) * ∑ x_1 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 = MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>this : ∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)<GOAL>(MulOpposite.op x - MulOpposite.op y) * ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) = MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>s : Set R<GOAL>↑(closure s) = ↑(AddSubmonoid.closure ↑(Subsemigroup.closure s))
<VAR>S : ShortComplex Ab<GOAL>S.Exact ↔ Function.Surjective ⇑S.abToCycles
<VAR>S : ShortComplex Ab<GOAL>Function.Surjective ⇑S.abToCycles ↔ Function.Surjective ⇑S.abToCycles
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝² : OrderedCancelAddCommMonoid Γ✝<VAR>Γ : Type u_5<VAR>inst✝¹ : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hxy : ¬x * y = 0<GOAL>x.orderTop + y.orderTop ≤ (x * y).orderTop
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝² : OrderedCancelAddCommMonoid Γ✝<VAR>Γ : Type u_5<VAR>inst✝¹ : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hxy : ¬x * y = 0<GOAL>⋯.min ⋯ ≤ ⋯.min ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>J : Ideal A<VAR>hJ : J ≠ ⊤<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hjf : f j ≠ 0<VAR>I : FractionalIdeal A⁰ K := spanFinset A s f<GOAL>∃ a, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>J : Ideal A<VAR>hJ : J ≠ ⊤<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hjf : f j ≠ 0<VAR>I : FractionalIdeal A⁰ K := spanFinset A s f<VAR>hI0 : I ≠ 0<GOAL>∃ a, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>J : Ideal A<VAR>hJ : J ≠ ⊤<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hjf : f j ≠ 0<VAR>I : FractionalIdeal A⁰ K := spanFinset A s f<VAR>hI0 : I ≠ 0<GOAL>↑J / I < I⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>J : Ideal A<VAR>hJ : J ≠ ⊤<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hjf : f j ≠ 0<VAR>I : FractionalIdeal A⁰ K := spanFinset A s f<VAR>hI0 : I ≠ 0<GOAL>↑J < 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>J : Ideal A<VAR>hJ : J ≠ ⊤<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hjf : f j ≠ 0<VAR>I : FractionalIdeal A⁰ K := spanFinset A s f<VAR>hI0 : I ≠ 0<GOAL>↑J < ↑⊤
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p : P<VAR>h : p₁ -ᵥ p = p₂ -ᵥ p<GOAL>p₁ = p₂
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>a : α<VAR>inst✝ : Invertible a<GOAL>0 < a * ⅟a
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ i : ι, ‖x i‖ ^ (ENNReal.ofReal p).toReal) ^ (1 / (ENNReal.ofReal p).toReal)<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℝ), ‖x‖ = 0 ↔ x = 0<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℝ), ‖x‖ = 0 ↔ x = 0<VAR>nm_neg : ∀ (x : ι → ℝ), ‖-x‖ = ‖x‖<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℝ), ‖x‖ = 0 ↔ x = 0<VAR>nm_neg : ∀ (x : ι → ℝ), ‖-x‖ = ‖x‖<VAR>nm_add : ∀ (x y : ι → ℝ), ‖x + y‖ ≤ ‖x‖ + ‖y‖<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℝ), (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℝ), (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℝ), ‖r • x‖ ≤ ‖r‖ * ‖x‖<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℝ), (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℝ), (∑ x_1 : ι, |(r • x) x_1| ^ p) ^ (1 / p) ≤ |r| * (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>H : Subgroup G<VAR>hH : IsCompact ↑H<VAR>t : Set G<VAR>ht : IsClosed t<GOAL>IsClosed (mk '' t)
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>H : Subgroup G<VAR>hH : IsCompact ↑H<VAR>t : Set G<VAR>ht : IsClosed t<GOAL>IsClosed (Quotient.mk' ⁻¹' (mk '' t))
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>H : Subgroup G<VAR>hH : IsCompact ↑H<VAR>t : Set G<VAR>ht : IsClosed t<GOAL>Quotient.mk' ⁻¹' (mk '' t) = t * ↑H
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>H : Subgroup G<VAR>hH : IsCompact ↑H<VAR>t : Set G<VAR>ht : IsClosed t<GOAL>⋃ x, (fun x_1 => x_1 * ↑x) '' t = t * ↑H
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>H : Subgroup G<VAR>hH : IsCompact ↑H<VAR>t : Set G<VAR>ht : IsClosed t<GOAL>⋃ x, ⋃ (hx : x ∈ H), (fun x_1 => x_1 * ↑⟨x, hx⟩) '' t = ⋃ a ∈ ↑H, (fun x => x * a) '' t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>↑↑↑((condexpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) =ᶠ[ae μ] ↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>(fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ] ↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>h_comp : ∀ᵐ (a : α) ∂μ, ↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) a = (toSpanSingleton ℝ x) (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)<GOAL>(fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ] ↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>h_comp : ↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] fun a => (toSpanSingleton ℝ x) (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)<GOAL>(fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ] ↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>h_comp : ↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] fun a => (toSpanSingleton ℝ x) (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)<GOAL>(fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ] fun a => (toSpanSingleton ℝ x) (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ✝ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f : α × β → γ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>τ : Measure γ<VAR>hf : Measurable f<VAR>inst✝ : SFinite ν<VAR>h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun y => f (x, y)) ν τ<GOAL>map f (μ.prod ν) ≪ τ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ✝ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f : α × β → γ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>τ : Measure γ<VAR>hf : Measurable f<VAR>inst✝ : SFinite ν<VAR>h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun y => f (x, y)) ν τ<VAR>s : Set γ<VAR>hs : MeasurableSet s<VAR>h2s : τ s = 0<GOAL>(map f (μ.prod ν)) s = 0