𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁵ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁴ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H : ∀ (x : G) (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ ‖LinearMap.mkContinuous
        {
          toAddHom :=
            {
              toFun := fun x =>
                mkContinuous (↑f x) (C * ‖x‖) (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
              map_add' :=
                (_ :
                  ∀ (x y : G),
                    (fun x =>
                          mkContinuous (↑f x) (C * ‖x‖)
                            (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                        (x + y) =
                      (fun x =>
                            mkContinuous (↑f x) (C * ‖x‖)
                              (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                          x +
                        (fun x =>
                            mkContinuous (↑f x) (C * ‖x‖)
                              (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                          y) },
          map_smul' :=
            (_ :
              ∀ (c : 𝕜) (x : G),
                AddHom.toFun
                    {
                      toFun := fun x =>
                        mkContinuous (↑f x) (C * ‖x‖)
                          (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                      map_add' :=
                        (_ :
                          ∀ (x y : G),
                            (fun x =>
                                  mkContinuous (↑f x) (C * ‖x‖)
                                    (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                (x + y) =
                              (fun x =>
                                    mkContinuous (↑f x) (C * ‖x‖)
                                      (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                  x +
                                (fun x =>
                                    mkContinuous (↑f x) (C * ‖x‖)
                                      (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                  y) }
                    (c • x) =
                  ↑(RingHom.id 𝕜) c •
                    AddHom.toFun
                      {
                        toFun := fun x =>
                          mkContinuous (↑f x) (C * ‖x‖)
                            (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                        map_add' :=
                          (_ :
                            ∀ (x y : G),
                              (fun x =>
                                    mkContinuous (↑f x) (C * ‖x‖)
                                      (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                  (x + y) =
                                (fun x =>
                                      mkContinuous (↑f x) (C * ‖x‖)
                                        (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                    x +
                                  (fun x =>
                                      mkContinuous (↑f x) (C * ‖x‖)
                                        (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                    y) }
                      x) }
        (max C 0)
        (_ :
          ∀ (x : G),
            ‖↑{
                      toAddHom :=
                        {
                          toFun := fun x =>
                            mkContinuous (↑f x) (C * ‖x‖)
                              (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                          map_add' :=
                            (_ :
                              ∀ (x y : G),
                                (fun x =>
                                      mkContinuous (↑f x) (C * ‖x‖)
                                        (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                    (x + y) =
                                  (fun x =>
                                        mkContinuous (↑f x) (C * ‖x‖)
                                          (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                      x +
                                    (fun x =>
                                        mkContinuous (↑f x) (C * ‖x‖)
                                          (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                      y) },
                      map_smul' :=
                        (_ :
                          ∀ (c : 𝕜) (x : G),
                            AddHom.toFun
                                {
                                  toFun := fun x =>
                                    mkContinuous (↑f x) (C * ‖x‖)
                                      (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : G),
                                        (fun x =>
                                              mkContinuous (↑f x) (C * ‖x‖)
                                                (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                            (x + y) =
                                          (fun x =>
                                                mkContinuous (↑f x) (C * ‖x‖)
                                                  (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                              x +
                                            (fun x =>
                                                mkContinuous (↑f x) (C * ‖x‖)
                                                  (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                              y) }
                                (c • x) =
                              ↑(RingHom.id 𝕜) c •
                                AddHom.toFun
                                  {
                                    toFun := fun x =>
                                      mkContinuous (↑f x) (C * ‖x‖)
                                        (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : G),
                                          (fun x =>
                                                mkContinuous (↑f x) (C * ‖x‖)
                                                  (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                              (x + y) =
                                            (fun x =>
                                                  mkContinuous (↑f x) (C * ‖x‖)
                                                    (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                                x +
                                              (fun x =>
                                                  mkContinuous (↑f x) (C * ‖x‖)
                                                    (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                                y) }
                                  x) }
                  x‖ ≤
              max C 0 * ‖x‖)‖ ≤
    max C 0
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁵ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁴ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H : ∀ (x : G) (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ ‖mkContinuousLinear f C H‖ ≤ max C 0
dsimp only [mkContinuousLinear]
no goals
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁵ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁴ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H : ∀ (x : G) (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ ‖LinearMap.mkContinuous
        {
          toAddHom :=
            {
              toFun := fun x =>
                mkContinuous (↑f x) (C * ‖x‖) (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
              map_add' :=
                (_ :
                  ∀ (x y : G),
                    (fun x =>
                          mkContinuous (↑f x) (C * ‖x‖)
                            (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                        (x + y) =
                      (fun x =>
                            mkContinuous (↑f x) (C * ‖x‖)
                              (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                          x +
                        (fun x =>
                            mkContinuous (↑f x) (C * ‖x‖)
                              (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                          y) },
          map_smul' :=
            (_ :
              ∀ (c : 𝕜) (x : G),
                AddHom.toFun
                    {
                      toFun := fun x =>
                        mkContinuous (↑f x) (C * ‖x‖)
                          (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                      map_add' :=
                        (_ :
                          ∀ (x y : G),
                            (fun x =>
                                  mkContinuous (↑f x) (C * ‖x‖)
                                    (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                (x + y) =
                              (fun x =>
                                    mkContinuous (↑f x) (C * ‖x‖)
                                      (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                  x +
                                (fun x =>
                                    mkContinuous (↑f x) (C * ‖x‖)
                                      (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                  y) }
                    (c • x) =
                  ↑(RingHom.id 𝕜) c •
                    AddHom.toFun
                      {
                        toFun := fun x =>
                          mkContinuous (↑f x) (C * ‖x‖)
                            (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                        map_add' :=
                          (_ :
                            ∀ (x y : G),
                              (fun x =>
                                    mkContinuous (↑f x) (C * ‖x‖)
                                      (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                  (x + y) =
                                (fun x =>
                                      mkContinuous (↑f x) (C * ‖x‖)
                                        (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                    x +
                                  (fun x =>
                                      mkContinuous (↑f x) (C * ‖x‖)
                                        (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                    y) }
                      x) }
        (max C 0)
        (_ :
          ∀ (x : G),
            ‖↑{
                      toAddHom :=
                        {
                          toFun := fun x =>
                            mkContinuous (↑f x) (C * ‖x‖)
                              (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                          map_add' :=
                            (_ :
                              ∀ (x y : G),
                                (fun x =>
                                      mkContinuous (↑f x) (C * ‖x‖)
                                        (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                    (x + y) =
                                  (fun x =>
                                        mkContinuous (↑f x) (C * ‖x‖)
                                          (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                      x +
                                    (fun x =>
                                        mkContinuous (↑f x) (C * ‖x‖)
                                          (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                      y) },
                      map_smul' :=
                        (_ :
                          ∀ (c : 𝕜) (x : G),
                            AddHom.toFun
                                {
                                  toFun := fun x =>
                                    mkContinuous (↑f x) (C * ‖x‖)
                                      (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : G),
                                        (fun x =>
                                              mkContinuous (↑f x) (C * ‖x‖)
                                                (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                            (x + y) =
                                          (fun x =>
                                                mkContinuous (↑f x) (C * ‖x‖)
                                                  (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                              x +
                                            (fun x =>
                                                mkContinuous (↑f x) (C * ‖x‖)
                                                  (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                              y) }
                                (c • x) =
                              ↑(RingHom.id 𝕜) c •
                                AddHom.toFun
                                  {
                                    toFun := fun x =>
                                      mkContinuous (↑f x) (C * ‖x‖)
                                        (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖),
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : G),
                                          (fun x =>
                                                mkContinuous (↑f x) (C * ‖x‖)
                                                  (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                              (x + y) =
                                            (fun x =>
                                                  mkContinuous (↑f x) (C * ‖x‖)
                                                    (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                                x +
                                              (fun x =>
                                                  mkContinuous (↑f x) (C * ‖x‖)
                                                    (_ : ∀ (m : (i : ι) → E i), ‖↑(↑f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖))
                                                y) }
                                  x) }
                  x‖ ≤
              max C 0 * ‖x‖)‖ ≤
    max C 0
exact LinearMap.mkContinuous_norm_le _ (le_max_right _ _) _