-- Mathlib/Analysis/Matrix.lean
theorem frobenius_nnnorm_diagonal [DecidableEq n] (v : n → α) :
    ‖diagonal v‖₊ = ‖(WithLp.equiv 2 _).symm v‖₊

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ (∑ x : n × n, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2)

Tactic:
let s := (Finset.univ : Finset n).map ⟨fun i : n => (i, i), fun i j h => congr_arg Prod.fst h⟩

Result:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x : n × n, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2)

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x : n,
        ‖diagonal v ({ toFun := fun i => (i, i), inj' := ⋯ } x).1 ({ toFun := fun i => (i, i), inj' := ⋯ } x).2‖₊ ^ 2) ^
      (1 / 2) =
    (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2) ^ (1 / 2)

Tactic:
dsimp

Result:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x : n, ‖diagonal v x x‖₊ ^ 2) ^ (1 / 2) = (∑ i : n, ‖v i‖₊ ^ 2) ^ (1 / 2)

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = ‖(WithLp.equiv 2 (n → α)).symm v‖₊

Tactic:
simp_rw [frobenius_nnnorm_def, ← Finset.sum_product', Finset.univ_product_univ,
  PiLp.nnnorm_eq_of_L2]

Result:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ (∑ x : n × n, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2)

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
this : i.1 ≠ i.2
⊢ ‖diagonal v i.1 i.2‖₊ ^ 2 = 0

Tactic:
rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]

Result:
no goals

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x : n × n, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2)

Tactic:
rw [← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_]

Result:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x ∈ s, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2)

n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
⊢ ‖diagonal v i.1 i.2‖₊ ^ 2 = 0

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x ∈ s, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2)

Tactic:
rw [Finset.sum_map, NNReal.sqrt_eq_rpow]

Result:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x : n,
        ‖diagonal v ({ toFun := fun i => (i, i), inj' := ⋯ } x).1 ({ toFun := fun i => (i, i), inj' := ⋯ } x).2‖₊ ^ 2) ^
      (1 / 2) =
    (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2) ^ (1 / 2)

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
h : i.1 = i.2
⊢ False

Tactic:
exact Finset.mem_map.not.mp his ⟨i.1, Finset.mem_univ _, Prod.ext rfl h⟩

Result:
no goals

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
⊢ i.1 ≠ i.2

Tactic:
intro h

Result:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
h : i.1 = i.2
⊢ False

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
⊢ ‖diagonal v i.1 i.2‖₊ ^ 2 = 0

Tactic:
suffices i.1 ≠ i.2 by rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]

Result:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
⊢ i.1 ≠ i.2

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x : n, ‖diagonal v x x‖₊ ^ 2) ^ (1 / 2) = (∑ i : n, ‖v i‖₊ ^ 2) ^ (1 / 2)

Tactic:
simp_rw [diagonal_apply_eq, NNReal.rpow_two]

Result:
no goals