ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>f : V → E<GOAL>Real.fourierIntegralInv f = Real.fourierIntegral fun x => f (-x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>f : V → E<GOAL>Real.fourierIntegral (Real.fourierIntegralInv f) = Real.fourierIntegralInv (Real.fourierIntegral f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>NormedAddCommGroup W<VAR>InnerProductSpace ℝ W<VAR>MeasurableSpace W<VAR>BorelSpace W<VAR>FiniteDimensional ℝ W<VAR>A : W ≃ₗᵢ[ℝ] V<VAR>f : V → E<VAR>w : W<GOAL>Real.fourierIntegralInv (f ∘ ⇑A) w = Real.fourierIntegralInv f (A w)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>w : ℝ<GOAL>Real.fourierIntegral f w = ∫ (v : ℝ), Real.fourierChar (-(v * w)) • f v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<VAR>w : ℝ<GOAL>Real.fourierIntegral f w = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>μ : MeasureTheory.Measure V<VAR>f : V → E<VAR>w : V<GOAL>MeasureTheory.Integrable (fun v => Real.fourierChar (-⟪v, w⟫_ℝ) • f v) μ ↔ MeasureTheory.Integrable f μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : V → F →L[ℝ] E<VAR>a : F<VAR>v : V<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<GOAL>(Real.fourierIntegral f v) a = Real.fourierIntegral (fun x => (f x) a) v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>ι : Type u_4<VAR>Fintype ι<VAR>M : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace ℝ (M i)<VAR>f : V → ContinuousMultilinearMap ℝ M E<VAR>m : (i : ι) → M i<VAR>v : V<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<GOAL>(Real.fourierIntegral f v) m = Real.fourierIntegral (fun x => (f x) m) v
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>MeasureTheory.volume = ENNReal.ofReal T • AddCircle.haarAddCircle
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : AddCircle T<GOAL>(fourier n) x = ↑(n • x).toCircle
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>↑(AddCircle.toCircle (n • ↑x)) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
<VAR>T : ℝ<VAR>x : AddCircle T<GOAL>↑(AddCircle.toCircle 0) = 1
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : AddCircle T<GOAL>↑(-(n • x)).toCircle = (starRingEnd ℂ) ((fourier n) x)
<VAR>T : ℝ<VAR>Fact (0 < T)<VAR>n : ℤ<GOAL>‖fourier n‖ = 1
<VAR>T : ℝ<GOAL>Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra = Submodule.span ℂ (Set.range fourier)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>fourierSubalgebra.SeparatesPoints
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>fourierSubalgebra.topologicalClosure = ⊤
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>(Submodule.span ℂ (Set.range fourier)).topologicalClosure = ⊤
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>n : ℤ<GOAL>↑↑(fourierLp p n) =ᵐ[AddCircle.haarAddCircle] ⇑(fourier n)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<GOAL>(Submodule.span ℂ (Set.range (fourierLp p))).topologicalClosure = ⊤
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : AddCircle T → E<VAR>n : ℤ<VAR>a : ℝ<GOAL>fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f ↑x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : AddCircle T → E<VAR>c : ℂ<VAR>n : ℤ<GOAL>fourierCoeff (c • f) n = c • fourierCoeff f n
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : AddCircle T → ℂ<VAR>c : ℂ<VAR>n : ℤ<GOAL>fourierCoeff (fun x => c * f x) n = c * fourierCoeff f n
<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>n : ℤ<VAR>hab : a < b<GOAL>fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>c : ℂ<VAR>n : ℤ<VAR>hab : a < b<GOAL>fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n
<VAR>a b : ℝ<VAR>f : ℝ → ℂ<VAR>c : ℂ<VAR>n : ℤ<VAR>hab : a < b<GOAL>fourierCoeffOn hab (fun x => c * f x) n = c * fourierCoeffOn hab f n
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>fourierCoeff (AddCircle.liftIoc T a f) n = fourierCoeffOn ⋯ f n
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>fourierCoeff (AddCircle.liftIco T a f) n = fourierCoeffOn ⋯ f n
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>(fun i => fourierBasis.repr.symm (lp.single 2 i 1)) = fourierLp 2
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)<VAR>i : ℤ<GOAL>↑(fourierBasis.repr f) i = fourierCoeff (↑↑f) i
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)<GOAL>HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)<GOAL>∑' (i : ℤ), ‖fourierCoeff (↑↑f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : C(AddCircle T, ℂ)<VAR>n : ℤ<GOAL>fourierCoeff (↑↑((ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f)) n = fourierCoeff (⇑f) n
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>HasDerivAt (fun y => (fourier n) ↑y) (2 * ↑π * Complex.I * ↑n / ↑T * (fourier n) ↑x) x
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>HasDerivAt (fun y => (fourier (-n)) ↑y) (-2 * ↑π * Complex.I * ↑n / ↑T * (fourier (-n)) ↑x) x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>x : ℝ<GOAL>HasDerivAt (fun y => ↑T / (-2 * ↑π * Complex.I * ↑n) * (fourier (-n)) ↑y) ((fourier (-n)) ↑x) x
<VAR>a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f (Set.uIcc a b)<VAR>hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hf' : IntervalIntegrable f' MeasureTheory.volume a b<GOAL>fourierCoeffOn hab f n = 1 / (-2 * ↑π * Complex.I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f (Set.uIcc a b)<VAR>hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x<VAR>hf' : IntervalIntegrable f' MeasureTheory.volume a b<GOAL>fourierCoeffOn hab f n = 1 / (-2 * ↑π * Complex.I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x<VAR>hf' : IntervalIntegrable f' MeasureTheory.volume a b<GOAL>fourierCoeffOn hab f n = 1 / (-2 * ↑π * Complex.I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>x₀ : E<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<GOAL>∀ᶠ (x : E) in 𝓝 x₀, ‖x - x₀‖₊ < ε
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>x₀ : E<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<GOAL>∀ᶠ (x : E) in 𝓝 x₀, ‖x - x₀‖ < ε
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring 𝕜<VAR>Ring 𝕜₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>f : E → F<VAR>h_add : ∀ (x y : E), f (x + y) = f x + f y<VAR>h_smul : ∀ (c : 𝕜) (x : E), f (c • x) = σ c • f x<VAR>C : ℝ<VAR>h_bound : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>Continuous f
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>G : Type u_5<VAR>Ring 𝕜<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup G<VAR>Module 𝕜 E<VAR>Module 𝕜 G<VAR>f : E → G<VAR>h_add : ∀ (x y : E), f (x + y) = f x + f y<VAR>h_smul : ∀ (c : 𝕜) (x : E), f (c • x) = c • f x<VAR>C : ℝ<VAR>h_bound : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>Continuous f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring 𝕜<VAR>Ring 𝕜₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>f : E →ₛₗ[σ] F<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>↑(f.mkContinuous C h) = f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring 𝕜<VAR>Ring 𝕜₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>f : E →ₛₗ[σ] F<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<VAR>x : E<GOAL>(f.mkContinuous C h) x = f x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring 𝕜<VAR>Ring 𝕜₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>f : E →ₛₗ[σ] F<VAR>h : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>↑(f.mkContinuousOfExistsBound h) = f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring 𝕜<VAR>Ring 𝕜₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>f : E →ₛₗ[σ] F<VAR>h : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<VAR>x : E<GOAL>(f.mkContinuousOfExistsBound h) x = f x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring 𝕜<VAR>Ring 𝕜₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>f : E →SL[σ] F<VAR>K : ℝ≥0<VAR>h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖<GOAL>AntilipschitzWith K ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring 𝕜<VAR>Ring 𝕜₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>f : E →SL[σ] F<VAR>K : ℝ≥0<VAR>h : AntilipschitzWith K ⇑f<VAR>x : E<GOAL>‖x‖ ≤ ↑K * ‖f x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : 𝕜 →ₗ[𝕜] E<GOAL>↑f.toContinuousLinearMap₁ = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : 𝕜 →ₗ[𝕜] E<VAR>x : 𝕜<GOAL>f.toContinuousLinearMap₁ x = f x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring 𝕜<VAR>Ring 𝕜₂<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>f : E →SL[σ] F<VAR>K : ℝ≥0<VAR>hf : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖<GOAL>UniformEmbedding ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring 𝕜<VAR>Ring 𝕜₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ σ₂₁<VAR>RingHomInvPair σ₂₁ σ<VAR>a : ℝ<VAR>ha : 0 < a<VAR>f : E ≃ₛₗ[σ] F<GOAL>(∀ (x : E), ‖f x‖ = a * ‖x‖) → ∀ (y : F), ‖f.symm y‖ = a⁻¹ * ‖y‖
<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>f : ι → ℝ<VAR>g : ι' → ℝ<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hf' : 0 ≤ f<VAR>hg' : 0 ≤ g<GOAL>Summable fun x => f x.1 * g x.2
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>NormedRing R<VAR>f : ι → R<VAR>g : ι' → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>Summable fun x => ‖f x.1 * g x.2‖
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>NormedRing R<VAR>CompleteSpace R<VAR>f : ι → R<VAR>g : ι' → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>Summable fun x => f x.1 * g x.2
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>NormedRing R<VAR>CompleteSpace R<VAR>f : ι → R<VAR>g : ι' → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>(∑' (x : ι), f x) * ∑' (y : ι'), g y = ∑' (z : ι × ι'), f z.1 * g z.2
<VAR>R : Type u_1<VAR>NormedRing R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>Summable fun n => ‖∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2‖
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2
<VAR>R : Type u_1<VAR>NormedRing R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>Summable fun n => ‖∑ k ∈ Finset.range (n + 1), f k * g (n - k)‖
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
<VAR>𝕜 : Type u_1<VAR>NonUnitalSeminormedRing 𝕜<VAR>x y : ↑(Metric.ball 0 1)<GOAL>↑(x * y) = ↑x * ↑y
<VAR>𝕜 : Type u_1<VAR>NonUnitalSeminormedRing 𝕜<VAR>x y : ↑(Metric.closedBall 0 1)<GOAL>↑(x * y) = ↑x * ↑y
<VAR>𝕜 : Type u_1<VAR>SeminormedRing 𝕜<VAR>NormOneClass 𝕜<GOAL>↑1 = 1
<VAR>𝕜 : Type u_1<VAR>SeminormedRing 𝕜<VAR>NormOneClass 𝕜<VAR>x : ↑(Metric.closedBall 0 1)<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>x : ↑(Metric.sphere 0 1)<GOAL>↑x⁻¹ = (↑x)⁻¹
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>x y : ↑(Metric.sphere 0 1)<GOAL>↑(x / y) = ↑x / ↑y
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>x : ↑(Metric.sphere 0 1)<VAR>n : ℤ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<GOAL>↑1 = 1
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>x y : ↑(Metric.sphere 0 1)<GOAL>↑(x * y) = ↑x * ↑y
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>x : ↑(Metric.sphere 0 1)<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<VAR>x : ↑(Metric.sphere 0 1)<GOAL>↑((unitSphereToUnits 𝕜) x) = ↑x
<VAR>𝕜 : Type u_1<VAR>NormedDivisionRing 𝕜<GOAL>Function.Injective ⇑(unitSphereToUnits 𝕜)
<VAR>n : ℤ<GOAL>‖n‖ = |↑n|
<VAR>n : ℕ<GOAL>‖↑n‖ = ↑n
<VAR>n : ℤ<GOAL>↑n.natAbs = ‖n‖₊
<VAR>z : ℤ<VAR>c : ℝ≥0<GOAL>|z| ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>n : ℤ<VAR>a : α<GOAL>‖n • a‖ ≤ ‖n‖ * ‖a‖
<VAR>α : Type u_1<VAR>SeminormedCommGroup α<VAR>n : ℤ<VAR>a : α<GOAL>‖a ^ n‖ ≤ ‖n‖ * ‖a‖
<VAR>α : Type u_1<VAR>SeminormedCommGroup α<VAR>n : ℤ<VAR>a : α<GOAL>‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>n : ℤ<VAR>a : α<GOAL>‖n • a‖₊ ≤ ‖n‖₊ * ‖a‖₊
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<GOAL>Filter.comap norm Filter.atTop = Bornology.cobounded E
<VAR>E : Type u_3<VAR>SeminormedGroup E<GOAL>Filter.comap norm Filter.atTop = Bornology.cobounded E
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>ι : Sort u_6<VAR>p : ι → Prop<VAR>s : ι → Set ℝ<VAR>h : Filter.atTop.HasBasis p s<GOAL>(Bornology.cobounded E).HasBasis p fun i => norm ⁻¹' s i
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>ι : Sort u_6<VAR>p : ι → Prop<VAR>s : ι → Set ℝ<VAR>h : Filter.atTop.HasBasis p s<GOAL>(Bornology.cobounded E).HasBasis p fun i => norm ⁻¹' s i
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<GOAL>(Bornology.cobounded E).HasBasis (fun x => True) fun x => {x_1 | x ≤ ‖x_1‖}
<VAR>E : Type u_3<VAR>SeminormedGroup E<GOAL>(Bornology.cobounded E).HasBasis (fun x => True) fun x => {x_1 | x ≤ ‖x_1‖}
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>f : α → E<VAR>l : Filter α<GOAL>Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded E)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>f : α → E<VAR>l : Filter α<GOAL>Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded E)
<VAR>E : Type u_3<VAR>SeminormedGroup E<GOAL>Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<GOAL>Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>a : ℝ<GOAL>∀ᶠ (x : E) in Bornology.cobounded E, a ≤ ‖x‖
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>a : ℝ<GOAL>∀ᶠ (x : E) in Bornology.cobounded E, a ≤ ‖x‖
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>ProperSpace E<GOAL>Filter.Tendsto norm (Filter.cocompact E) Filter.atTop
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>ProperSpace E<GOAL>Filter.Tendsto norm (Filter.cocompact E) Filter.atTop
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<GOAL>-Bornology.cobounded E = Bornology.cobounded E
<VAR>E : Type u_3<VAR>SeminormedGroup E<GOAL>(Bornology.cobounded E)⁻¹ = Bornology.cobounded E
<VAR>E : Type u_3<VAR>SeminormedGroup E<GOAL>Filter.Tendsto Inv.inv (Bornology.cobounded E) (Bornology.cobounded E)
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<GOAL>Filter.Tendsto Neg.neg (Bornology.cobounded E) (Bornology.cobounded E)
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>s : Set E<GOAL>Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>s : Set E<GOAL>Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<GOAL>∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<GOAL>∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<GOAL>∃ R > 0, ∀ x ∈ s, ‖x‖ < R
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<GOAL>∃ R > 0, ∀ x ∈ s, ‖x‖ < R
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>u : α → E<GOAL>CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m / u n‖ < ε
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>u : α → E<GOAL>CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m - u n‖ < ε
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → E<VAR>hf : ContinuousOn f s<GOAL>∃ C, ∀ x ∈ s, ‖f x‖ ≤ C
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → E<VAR>hf : ContinuousOn f s<GOAL>∃ C, ∀ x ∈ s, ‖f x‖ ≤ C
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>hf : HasCompactMulSupport f<VAR>h'f : Continuous f<GOAL>∃ C, ∀ (x : α), ‖f x‖ ≤ C
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>hf : HasCompactSupport f<VAR>h'f : Continuous f<GOAL>∃ C, ∀ (x : α), ‖f x‖ ≤ C
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>SeminormedAddGroup G<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l (𝓝 0)<VAR>hg : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g)<VAR>op : E → F → G<VAR>h_op : ∃ A, ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<GOAL>Filter.Tendsto (fun x => op (f x) (g x)) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>SeminormedGroup G<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l (𝓝 1)<VAR>hg : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g)<VAR>op : E → F → G<VAR>h_op : ∃ A, ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<GOAL>Filter.Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>SeminormedGroup G<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l (𝓝 1)<VAR>hg : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g)<VAR>op : E → F → G<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖<GOAL>Filter.Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>SeminormedAddGroup G<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l (𝓝 0)<VAR>hg : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g)<VAR>op : E → F → G<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖<GOAL>Filter.Tendsto (fun x => op (f x) (g x)) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>NormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>hf : Continuous f<VAR>h : HasCompactSupport f<GOAL>∃ C, ∀ (x : α), ‖f x‖ ≤ C
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>NormedAddGroup α<VAR>f : α → E<VAR>One E<VAR>hf : HasCompactMulSupport f<GOAL>∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>NormedAddGroup α<VAR>f : α → E<VAR>Zero E<VAR>hf : HasCompactSupport f<GOAL>∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 0
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommGroup α<VAR>AddCommGroup β<GOAL>0.1 = 0
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommGroup α<VAR>AddCommGroup β<GOAL>0.2 = 0
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>x y : WithLp p (α × β)<GOAL>(x + y).1 = x.1 + y.1
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>x y : WithLp p (α × β)<GOAL>(x + y).2 = x.2 + y.2
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>x y : WithLp p (α × β)<GOAL>(x - y).1 = x.1 - y.1
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>x y : WithLp p (α × β)<GOAL>(x - y).2 = x.2 - y.2
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>x : WithLp p (α × β)<GOAL>(-x).1 = -x.1
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>x : WithLp p (α × β)<GOAL>(-x).2 = -x.2
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Semiring 𝕜<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>x : WithLp p (α × β)<VAR>c : 𝕜<VAR>Module 𝕜 α<VAR>Module 𝕜 β<GOAL>(c • x).1 = c • x.1
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Semiring 𝕜<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>x : WithLp p (α × β)<VAR>c : 𝕜<VAR>Module 𝕜 α<VAR>Module 𝕜 β<GOAL>(c • x).2 = c • x.2
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x : WithLp p (α × β)<GOAL>((WithLp.equiv p (α × β)) x).1 = x.1
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x : WithLp p (α × β)<GOAL>((WithLp.equiv p (α × β)) x).2 = x.2
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x : α × β<GOAL>((WithLp.equiv p (α × β)).symm x).1 = x.1
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x : α × β<GOAL>((WithLp.equiv p (α × β)).symm x).2 = x.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>EDist α<VAR>EDist β<VAR>f g : WithLp 0 (α × β)<GOAL>edist f g = (if edist f.1 g.1 = 0 then 0 else 1) + if edist f.2 g.2 = 0 then 0 else 1
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>EDist α<VAR>EDist β<VAR>hp : 0 < p.toReal<VAR>f g : WithLp p (α × β)<GOAL>edist f g = (edist f.1 g.1 ^ p.toReal + edist f.2 g.2 ^ p.toReal) ^ (1 / p.toReal)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>EDist α<VAR>EDist β<VAR>f g : WithLp ⊤ (α × β)<GOAL>edist f g = edist f.1 g.1 ⊔ edist f.2 g.2
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : WithLp p (α × β)<GOAL>edist f f = 0
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f g : WithLp p (α × β)<GOAL>edist f g = edist g f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Dist α<VAR>Dist β<VAR>f g : WithLp 0 (α × β)<GOAL>dist f g = (if dist f.1 g.1 = 0 then 0 else 1) + if dist f.2 g.2 = 0 then 0 else 1
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Dist α<VAR>Dist β<VAR>hp : 0 < p.toReal<VAR>f g : WithLp p (α × β)<GOAL>dist f g = (dist f.1 g.1 ^ p.toReal + dist f.2 g.2 ^ p.toReal) ^ (1 / p.toReal)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Dist α<VAR>Dist β<VAR>f g : WithLp ⊤ (α × β)<GOAL>dist f g = dist f.1 g.1 ⊔ dist f.2 g.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Norm α<VAR>Norm β<VAR>f : WithLp 0 (α × β)<GOAL>‖f‖ = (if ‖f.1‖ = 0 then 0 else 1) + if ‖f.2‖ = 0 then 0 else 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Norm α<VAR>Norm β<VAR>f : WithLp ⊤ (α × β)<GOAL>‖f‖ = ‖f.1‖ ⊔ ‖f.2‖