ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>C : ℝ<VAR>b : ι → ℝ<VAR>hC : ‖f‖ ≤ C<VAR>hm : ∀ (i : ι), ‖m i‖ ≤ b i<GOAL>‖f m‖ ≤ C * ∏ i : ι, b i
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>b : ι → ℝ<VAR>hm : ∀ (i : ι), ‖m i‖ ≤ b i<GOAL>‖f m‖ ≤ ‖f‖ * ∏ i : ι, b i
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>b : ℝ<VAR>hm : ‖m‖ ≤ b<GOAL>‖f m‖ ≤ ‖f‖ * b ^ Fintype.card ι
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ<VAR>Ei : Fin n → Type u_1<VAR>(i : Fin n) → SeminormedAddCommGroup (Ei i)<VAR>(i : Fin n) → NormedSpace 𝕜 (Ei i)<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>m : (i : Fin n) → Ei i<VAR>b : ℝ<VAR>hm : ‖m‖ ≤ b<GOAL>‖f m‖ ≤ ‖f‖ * b ^ n
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>C : ℝ<VAR>h : ‖f‖ ≤ C<GOAL>‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<GOAL>‖f m‖ / ∏ i : ι, ‖m i‖ ≤ ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>h : ‖m‖ ≤ 1<GOAL>‖f m‖ ≤ ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ M * ∏ i : ι, ‖m i‖<GOAL>‖f‖ ≤ M
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>hC : 0 ≤ C<GOAL>‖f‖ ≤ C ↔ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f g : ContinuousMultilinearMap 𝕜 E G<GOAL>‖f + g‖ ≤ ‖f‖ + ‖g‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<GOAL>‖0‖ = 0
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>𝕜' : Type u_1<VAR>NormedField 𝕜'<VAR>NormedSpace 𝕜' G<VAR>SMulCommClass 𝕜 𝕜' G<VAR>c : 𝕜'<GOAL>‖c • f‖ ≤ ‖c‖ * ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>‖-f‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<GOAL>𝓤 (ContinuousMultilinearMap 𝕜 E G) = ⨅ r, ⨅ (_ : r > 0), 𝓟 {f | ‖f.1 - f.2‖ < r}
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<GOAL>‖f m‖₊ ≤ ‖f‖₊ * ∏ i : ι, ‖m i‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>C : ℝ≥0<VAR>h : ‖f‖₊ ≤ C<GOAL>‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>C : ℝ≥0<GOAL>‖f‖₊ ≤ C ↔ ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>IsLeast {C | ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊} ‖f‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>g : ContinuousMultilinearMap 𝕜 E G'<GOAL>‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>g : ContinuousMultilinearMap 𝕜 E G'<GOAL>‖f.prod g‖ = max ‖f‖ ‖g‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E' : ι' → Type wE'<VAR>Fintype ι<VAR>Fintype ι'<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i' : ι') → SeminormedAddCommGroup (E' i')<VAR>(i' : ι') → NormedSpace 𝕜 (E' i')<VAR>f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')<GOAL>‖ContinuousMultilinearMap.pi f‖₊ = ‖f‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>ι' : Type v'<VAR>Fintype ι'<VAR>E' : ι' → Type wE'<VAR>(i' : ι') → SeminormedAddCommGroup (E' i')<VAR>(i' : ι') → NormedSpace 𝕜 (E' i')<VAR>f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')<GOAL>‖ContinuousMultilinearMap.pi f‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>Subsingleton ι<VAR>i : ι<VAR>f : G →L[𝕜] G'<GOAL>‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G' i) f‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>Subsingleton ι<VAR>i : ι<VAR>f : G →L[𝕜] G'<GOAL>‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G' i) f‖₊ = ‖f‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>Subsingleton ι<VAR>i : ι<GOAL>∀ (a : ContinuousMultilinearMap 𝕜 (fun x => G) G'), (ContinuousMultilinearMap.ofSubsingletonₗᵢ 𝕜 G i).symm a = (ContinuousMultilinearMap.ofSubsingleton 𝕜 G G' i).invFun a
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>Subsingleton ι<VAR>i : ι<GOAL>∀ (a : G →L[𝕜] G'), (ContinuousMultilinearMap.ofSubsingletonₗᵢ 𝕜 G i) a = (ContinuousMultilinearMap.ofSubsingleton 𝕜 G G' i).toFun a
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>Subsingleton ι<VAR>i : ι<GOAL>‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ ≤ 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>Subsingleton ι<VAR>i : ι<GOAL>‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖₊ ≤ 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>IsEmpty ι<VAR>x : G<GOAL>‖ContinuousMultilinearMap.constOfIsEmpty 𝕜 E x‖ = ‖x‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>IsEmpty ι<VAR>x : G<GOAL>‖ContinuousMultilinearMap.constOfIsEmpty 𝕜 E x‖₊ = ‖x‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜' 𝕜<VAR>NormedSpace 𝕜' G<VAR>IsScalarTower 𝕜' 𝕜 G<VAR>(i : ι) → NormedSpace 𝕜' (E i)<VAR>∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)<GOAL>‖ContinuousMultilinearMap.restrictScalars 𝕜' f‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜' 𝕜<VAR>NormedSpace 𝕜' G<VAR>IsScalarTower 𝕜' 𝕜 G<VAR>(i : ι) → NormedSpace 𝕜' (E i)<VAR>∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)<GOAL>Continuous (ContinuousMultilinearMap.restrictScalars 𝕜')
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>DecidableEq ι<VAR>m₁ m₂ : (i : ι) → E i<GOAL>‖f m₁ - f m₂‖ ≤ ‖f‖ * ∑ i : ι, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m₁ m₂ : (i : ι) → E i<GOAL>‖f m₁ - f m₂‖ ≤ ‖f‖ * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<GOAL>‖f.mkContinuous C H‖ ≤ C
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<GOAL>‖f.mkContinuous C H‖ ≤ max C 0
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>k n : ℕ<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>z : G<GOAL>‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra 𝕜 A<VAR>Nonempty ι<GOAL>‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra 𝕜 A<VAR>IsEmpty ι<GOAL>‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = ‖1‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>A : Type u_1<VAR>NormedCommRing A<VAR>NormedAlgebra 𝕜 A<VAR>NormOneClass A<GOAL>‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<GOAL>‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>hn : 0 < n<GOAL>‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<GOAL>‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖1‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>NormOneClass A<GOAL>‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ = 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E 𝕜<VAR>z : G<GOAL>‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E 𝕜<VAR>z : G<GOAL>‖f.smulRight z‖ = ‖f‖ * ‖z‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>z : G<GOAL>‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E 𝕜<VAR>z : G<GOAL>((ContinuousMultilinearMap.smulRightL 𝕜 E G) f) z = f.smulRight z
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<GOAL>‖ContinuousMultilinearMap.smulRightL 𝕜 E G‖ ≤ 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>g : G →L[𝕜] G'<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>‖g.compContinuousMultilinearMap f‖ ≤ ‖g‖ * ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>g : G ≃L[𝕜] G'<GOAL>(ContinuousLinearEquiv.compContinuousMultilinearMapL E g).symm = ContinuousLinearEquiv.compContinuousMultilinearMapL E g.symm
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>g : G ≃L[𝕜] G'<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>(ContinuousLinearEquiv.compContinuousMultilinearMapL E g) f = (↑g).compContinuousMultilinearMap f
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'<VAR>m : (i : ι) → E i<VAR>x : G<GOAL>(f.flipMultilinear m) x = (f x) m
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>g : G →ₗᵢ[𝕜] G'<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'<VAR>C : ℝ<VAR>H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖<GOAL>‖MultilinearMap.mkContinuousLinear f C H‖ ≤ max C 0
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>G' : Type wG'<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖<GOAL>‖MultilinearMap.mkContinuousLinear f C H‖ ≤ C
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>Fintype ι<VAR>Fintype ι'<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι') → SeminormedAddCommGroup (E' i)<VAR>(i : ι') → NormedSpace 𝕜 (E' i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)<VAR>C : ℝ<VAR>H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖<VAR>m : (i : ι) → E i<GOAL>⇑((f.mkContinuousMultilinear C H) m) = ⇑(f m)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>Fintype ι<VAR>Fintype ι'<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι') → SeminormedAddCommGroup (E' i)<VAR>(i : ι') → NormedSpace 𝕜 (E' i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)<VAR>C : ℝ<VAR>H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖<GOAL>‖f.mkContinuousMultilinear C H‖ ≤ max C 0
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>Fintype ι<VAR>Fintype ι'<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι') → SeminormedAddCommGroup (E' i)<VAR>(i : ι') → NormedSpace 𝕜 (E' i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖<GOAL>‖f.mkContinuousMultilinear C H‖ ≤ C
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i →L[𝕜] E₁ i<GOAL>‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i : ι, ‖f i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i<GOAL>‖g.compContinuousLinearMap fun i => (f i).toContinuousLinearMap‖ ≤ ‖g‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i<GOAL>‖g.compContinuousLinearMap fun i => ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }‖ = ‖g‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i →L[𝕜] E₁ i<GOAL>(ContinuousMultilinearMap.compContinuousLinearMapL f) g = g.compContinuousLinearMap f
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : (i : ι) → E i →L[𝕜] E₁ i<GOAL>‖ContinuousMultilinearMap.compContinuousLinearMapL f‖ ≤ ∏ i : ι, ‖f i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i →L[𝕜] E₁ i<GOAL>g.compContinuousLinearMapLRight f = g.compContinuousLinearMap f