Lean4
noncomputable instance : NormedAddCommGroup (V →ᴬ[𝕜] W) :=
AddGroupNorm.toNormedAddCommGroup
{ toFun := fun f => max ‖f 0‖ ‖f.contLinear‖
map_zero' := by simp [(ContinuousAffineMap.zero_apply)]
neg' := fun f => by simp [(ContinuousAffineMap.neg_apply)]
add_le' := fun f g => by
simp only [coe_add, max_le_iff, Pi.add_apply, add_contLinear]
exact
⟨(norm_add_le _ _).trans (add_le_add (le_max_left _ _) (le_max_left _ _)),
(norm_add_le _ _).trans (add_le_add (le_max_right _ _) (le_max_right _ _))⟩
eq_zero_of_map_eq_zero' := fun f h₀ =>
by
rcases max_eq_iff.mp h₀ with (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) <;> rw [h₁] at h₂
· rw [norm_le_zero_iff, contLinear_eq_zero_iff_exists_const] at h₂
obtain ⟨q, rfl⟩ := h₂
simp only [norm_eq_zero, coe_const, Function.const_apply] at h₁
rw [h₁]
rfl
· rw [norm_eq_zero, contLinear_eq_zero_iff_exists_const] at h₁
obtain ⟨q, rfl⟩ := h₁
simp only [norm_le_zero_iff, coe_const, Function.const_apply] at h₂
rw [h₂]
rfl }
