ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G<GOAL>f.uncurryLeft.curryLeft = f
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<GOAL>f.curryLeft.uncurryLeft = f
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G<VAR>v : (i : Fin n.succ) → Ei i<GOAL>((continuousMultilinearCurryLeftEquiv 𝕜 Ei G) f) v = (f (v 0)) (Fin.tail v)
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>x : Ei 0<VAR>v : (i : Fin n) → Ei i.succ<GOAL>(((continuousMultilinearCurryLeftEquiv 𝕜 Ei G).symm f) x) v = f (Fin.cons x v)
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<GOAL>‖f.curryLeft‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G<GOAL>‖f.uncurryLeft‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)<VAR>m : (i : Fin n.succ) → Ei i<GOAL>f.uncurryRight m = (f (Fin.init m)) (m (Fin.last n))
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>m : (i : Fin n) → Ei i.castSucc<VAR>x : Ei (Fin.last n)<GOAL>(f.curryRight m) x = f (Fin.snoc m x)
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)<GOAL>f.uncurryRight.curryRight = f
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<GOAL>f.curryRight.uncurryRight = f
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)<VAR>v : (i : Fin n.succ) → Ei i<GOAL>((continuousMultilinearCurryRightEquiv 𝕜 Ei G) f) v = (f (Fin.init v)) (v (Fin.last n))
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>v : (i : Fin n) → Ei i.castSucc<VAR>x : Ei (Fin.last n)<GOAL>(((continuousMultilinearCurryRightEquiv 𝕜 Ei G).symm f) v) x = f (Fin.snoc v x)
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) (G →L[𝕜] G')<VAR>v : Fin (n + 1) → G<GOAL>((continuousMultilinearCurryRightEquiv' 𝕜 n G G') f) v = (f (Fin.init v)) (v (Fin.last n))
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>v : Fin n → G<VAR>x : G<GOAL>(((continuousMultilinearCurryRightEquiv' 𝕜 n G G').symm f) v) x = f (Fin.snoc v x)
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<GOAL>‖f.curryRight‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)<GOAL>‖f.uncurryRight‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>x : G'<VAR>m : Fin 0 → G<GOAL>(ContinuousMultilinearMap.curry0 𝕜 G x) m = x
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<GOAL>f.uncurry0 = f 0
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>x : Fin 0 → G<GOAL>ContinuousMultilinearMap.curry0 𝕜 G (f x) = f
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<GOAL>ContinuousMultilinearMap.curry0 𝕜 G f.uncurry0 = f
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>x : G'<GOAL>(ContinuousMultilinearMap.curry0 𝕜 G x).uncurry0 = x
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>x : G'<GOAL>‖ContinuousMultilinearMap.curry0 𝕜 G x‖ = ‖x‖
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>x : Fin 0 → G<GOAL>‖f x‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<GOAL>‖f.uncurry0‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<GOAL>(continuousMultilinearCurryFin0 𝕜 G G') f = f 0
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>x : G'<VAR>v : Fin 0 → G<GOAL>((continuousMultilinearCurryFin0 𝕜 G G').symm x) v = x
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>x : G<GOAL>((continuousMultilinearCurryFin1 𝕜 G G') f) x = f (Fin.snoc 0 x)
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] G'<VAR>v : Fin 1 → G<GOAL>((continuousMultilinearCurryFin1 𝕜 G G').symm f) v = f (v 0)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>Fintype ι'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>σ : ι ≃ ι'<VAR>f : ContinuousMultilinearMap 𝕜 (fun x => G) G'<GOAL>‖ContinuousMultilinearMap.domDomCongr σ f‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>Fintype ι'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun x => G) G'<VAR>m : ι → G<VAR>m' : ι' → G<GOAL>(f.currySum m) m' = f (Sum.elim m m')
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>Fintype ι'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun x => G) (ContinuousMultilinearMap 𝕜 (fun x => G) G')<VAR>m : ι ⊕ ι' → G<GOAL>f.uncurrySum m = (f (m ∘ Sum.inl)) (m ∘ Sum.inr)
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>k l : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>mk : Fin k → G<VAR>ml : Fin l → G<GOAL>(((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) mk) ml = f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>k l : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) (ContinuousMultilinearMap 𝕜 (fun i => G) G')<VAR>m : Fin n → G<GOAL>((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) m = (f fun i => m ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i => m ((finSumEquivOfFinset hk hl) (Sum.inr i))
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>k l : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) (ContinuousMultilinearMap 𝕜 (fun i => G) G')<VAR>x y : G<GOAL>((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) (s.piecewise (fun x_1 => x) fun x => y) = (f fun x_1 => x) fun x => y
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>k l : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) (ContinuousMultilinearMap 𝕜 (fun i => G) G')<VAR>x : G<GOAL>(((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) fun x_1 => x) = (f fun x_1 => x) fun x_1 => x
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>k l : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>x y : G<GOAL>((((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) fun x_1 => x) fun x => y) = f (s.piecewise (fun x_1 => x) fun x => y)
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>MeasurableSpace V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module 𝕜 W<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>r : ℂ<GOAL>VectorFourier.fourierIntegral e μ L (r • f) = r • VectorFourier.fourierIntegral e μ L f
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>MeasurableSpace V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module 𝕜 W<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>w : W<GOAL>‖VectorFourier.fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>MeasurableSpace V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module 𝕜 W<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>MeasurableAdd V<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>μ.IsAddRightInvariant<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>v₀ : V<GOAL>VectorFourier.fourierIntegral e μ L (f ∘ fun v => v + v₀) = fun w => e ((L v₀) w) • VectorFourier.fourierIntegral e μ L f w
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>MeasurableSpace V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module 𝕜 W<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>TopologicalSpace V<VAR>BorelSpace V<VAR>TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>w : W<GOAL>MeasureTheory.Integrable (fun v => e (-(L v) w) • f v) μ ↔ MeasureTheory.Integrable f μ
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>MeasurableSpace V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module 𝕜 W<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>TopologicalSpace V<VAR>BorelSpace V<VAR>TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f g : V → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>VectorFourier.fourierIntegral e μ L f + VectorFourier.fourierIntegral e μ L g = VectorFourier.fourierIntegral e μ L (f + g)
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>MeasurableSpace V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module 𝕜 W<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>TopologicalSpace V<VAR>BorelSpace V<VAR>TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>FirstCountableTopology W<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>Continuous (VectorFourier.fourierIntegral e μ L f)
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>MeasurableSpace V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>NormedAddCommGroup G<VAR>NormedSpace ℂ G<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>TopologicalSpace V<VAR>BorelSpace V<VAR>TopologicalSpace W<VAR>MeasurableSpace W<VAR>BorelSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>ν : MeasureTheory.Measure W<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>SecondCountableTopology V<VAR>CompleteSpace E<VAR>CompleteSpace F<VAR>f : V → E<VAR>g : W → F<VAR>M : E →L[ℂ] F →L[ℂ] G<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g ν<GOAL>∫ (ξ : W), (M (VectorFourier.fourierIntegral e μ L f ξ)) (g ξ) ∂ν = ∫ (x : V), (M (f x)) (VectorFourier.fourierIntegral e ν L.flip g x) ∂μ
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>MeasurableSpace V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module 𝕜 W<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>TopologicalSpace V<VAR>BorelSpace V<VAR>TopologicalSpace W<VAR>MeasurableSpace W<VAR>BorelSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>ν : MeasureTheory.Measure W<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>SecondCountableTopology V<VAR>CompleteSpace F<VAR>f : V → ℂ<VAR>g : W → F<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g ν<GOAL>∫ (ξ : W), VectorFourier.fourierIntegral e μ L f ξ • g ξ ∂ν = ∫ (x : V), f x • VectorFourier.fourierIntegral e ν L.flip g x ∂μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>V : Type u_5<VAR>W : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>NormedAddCommGroup W<VAR>NormedSpace 𝕜 W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>L : V →L[𝕜] W →L[𝕜] 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → F →L[ℝ] E<VAR>a : F<VAR>w : W<VAR>he : Continuous ⇑e<VAR>hf : MeasureTheory.Integrable f μ<GOAL>(VectorFourier.fourierIntegral e μ L.toLinearMap₂ f w) a = VectorFourier.fourierIntegral e μ L.toLinearMap₂ (fun x => (f x) a) w
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>V : Type u_5<VAR>W : Type u_6<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>NormedAddCommGroup W<VAR>NormedSpace 𝕜 W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure V<VAR>L : V →L[𝕜] W →L[𝕜] 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace ℝ (M i)<VAR>f : V → ContinuousMultilinearMap ℝ M E<VAR>m : (i : ι) → M i<VAR>w : W<VAR>he : Continuous ⇑e<VAR>hf : MeasureTheory.Integrable f μ<GOAL>(VectorFourier.fourierIntegral e μ L.toLinearMap₂ f w) m = VectorFourier.fourierIntegral e μ L.toLinearMap₂ (fun x => (f x) m) w
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>MeasurableSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure 𝕜<VAR>f : 𝕜 → E<VAR>w : 𝕜<GOAL>Fourier.fourierIntegral e μ f w = ∫ (v : 𝕜), e (-(v * w)) • f v ∂μ
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>MeasurableSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure 𝕜<VAR>f : 𝕜 → E<VAR>r : ℂ<GOAL>Fourier.fourierIntegral e μ (r • f) = r • Fourier.fourierIntegral e μ f
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>MeasurableSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure 𝕜<VAR>f : 𝕜 → E<VAR>w : 𝕜<GOAL>‖Fourier.fourierIntegral e μ f w‖ ≤ ∫ (x : 𝕜), ‖f x‖ ∂μ
<VAR>𝕜 : Type u_1<VAR>CommRing 𝕜<VAR>MeasurableSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>MeasurableAdd 𝕜<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : MeasureTheory.Measure 𝕜<VAR>μ.IsAddRightInvariant<VAR>f : 𝕜 → E<VAR>v₀ : 𝕜<GOAL>Fourier.fourierIntegral e μ (f ∘ fun v => v + v₀) = fun w => e (v₀ * w) • Fourier.fourierIntegral e μ f w
<VAR>x : ℝ<GOAL>↑(Real.fourierChar x) = Complex.exp (↑(2 * π * x) * Complex.I)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module ℝ V<VAR>MeasurableSpace V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module ℝ W<VAR>L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ<VAR>μ : MeasureTheory.Measure V<VAR>f : V → E<VAR>w : W<GOAL>VectorFourier.fourierIntegral Real.fourierChar μ L f w = ∫ (v : V), Complex.exp (↑(-2 * π * (L v) w) * Complex.I) • f v ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>μ : MeasureTheory.Measure V<VAR>f : V → E<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>w : W<GOAL>MeasureTheory.Integrable (fun v => Real.fourierChar (-(L v) w) • f v) μ ↔ MeasureTheory.Integrable f μ
<VAR>E : Type u_1<VAR>F : Type u_3<VAR>V : Type u_4<VAR>W : Type u_5<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>μ : MeasureTheory.Measure V<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → F →L[ℝ] E<VAR>a : F<VAR>w : W<VAR>hf : MeasureTheory.Integrable f μ<GOAL>(VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f w) a = VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ (fun x => (f x) a) w
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>V : Type u_4<VAR>W : Type u_5<VAR>Fintype ι<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>μ : MeasureTheory.Measure V<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>M : ι → Type u_6<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace ℝ (M i)<VAR>f : V → ContinuousMultilinearMap ℝ M E<VAR>m : (i : ι) → M i<VAR>w : W<VAR>hf : MeasureTheory.Integrable f μ<GOAL>(VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f w) m = VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ (fun x => (f x) m) w
<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<VAR>w : V<GOAL>Real.fourierIntegral f w = ∫ (v : V), Real.fourierChar (-⟪v, w⟫_ℝ) • 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>FiniteDimensional ℝ V<VAR>f : V → E<VAR>w : V<GOAL>Real.fourierIntegral f w = ∫ (v : 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>FiniteDimensional ℝ V<VAR>f : V → E<VAR>w : V<GOAL>Real.fourierIntegralInv f w = ∫ (v : V), Real.fourierChar ⟪v, w⟫_ℝ • 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>FiniteDimensional ℝ V<VAR>f : V → E<VAR>w : V<GOAL>Real.fourierIntegralInv f w = ∫ (v : 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>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.fourierIntegral (f ∘ ⇑A) w = Real.fourierIntegral f (A w)
<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<VAR>w : V<GOAL>Real.fourierIntegralInv f w = Real.fourierIntegral f (-w)