[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ coeff (select P x) n = ↑(aeval x.coeff) (selectPoly P n)
[PROOFSTEP]
dsimp [select, selectPoly]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ coeff (mk p fun n => if P n then coeff x n else 0) n = ↑(aeval x.coeff) (if P n then X n else 0)
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ coeff (mk p fun n => if P n then coeff x n else 0) n = ↑(aeval x.coeff) (X n)
[PROOFSTEP]
rw [aeval_X, mk]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ coeff { coeff := fun n => if P n then coeff x n else 0 } n = coeff x n
[PROOFSTEP]
simp only [hi]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ (if True then coeff x n else 0) = coeff x n
[PROOFSTEP]
rfl
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ coeff (mk p fun n => if P n then coeff x n else 0) n = ↑(aeval x.coeff) 0
[PROOFSTEP]
rw [AlgHom.map_zero, mk]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ coeff { coeff := fun n => if P n then coeff x n else 0 } n = 0
[PROOFSTEP]
simp only [hi]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ (if False then coeff x n else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ P : ℕ → Prop
⊢ IsPoly p fun x x_1 x_2 => select P x_2
[PROOFSTEP]
use selectPoly P
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ P : ℕ → Prop
⊢ ∀ ⦃R : Type ?u.31994⦄ [inst : CommRing R] (x : 𝕎 R), (select P x).coeff = fun n => ↑(aeval x.coeff) (selectPoly P n)
[PROOFSTEP]
rintro R _Rcr x
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R✝ : Type u_1
inst✝ : CommRing R✝
P✝ P : ℕ → Prop
R : Type ?u.31994
_Rcr : CommRing R
x : 𝕎 R
⊢ (select P x).coeff = fun n => ↑(aeval x.coeff) (selectPoly P n)
[PROOFSTEP]
funext i
[GOAL]
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R✝ : Type u_1
inst✝ : CommRing R✝
P✝ P : ℕ → Prop
R : Type ?u.31994
_Rcr : CommRing R
x : 𝕎 R
i : ℕ
⊢ coeff (select P x) i = ↑(aeval x.coeff) (selectPoly P i)
[PROOFSTEP]
apply coeff_select
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
⊢ ∀ (x : 𝕎 R), select P x + select (fun i => ¬P i) x = x
[PROOFSTEP]
have : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x := IsPoly₂.diag (hf := IsPoly₂.comp)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
⊢ ∀ (x : 𝕎 R), select P x + select (fun i => ¬P i) x = x
[PROOFSTEP]
ghost_calc x
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
⊢ ∀ (n : ℕ), ↑(ghostComponent n) (select P x + select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
intro n
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ↑(ghostComponent n) (select P x + select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
simp only [RingHom.map_add]
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ↑(ghostComponent n) (select P x) + ↑(ghostComponent n) (select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
suffices
  (bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
  by
  apply_fun aeval x.coeff at this
  simpa only [AlgHom.map_add, aeval_bind₁, ← coeff_select]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this✝ : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
this :
  ↑(bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + ↑(bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
⊢ ↑(ghostComponent n) (select P x) + ↑(ghostComponent n) (select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
apply_fun aeval x.coeff at this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this✝ : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
this :
  ↑(aeval x.coeff)
      (↑(bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + ↑(bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n)) =
    ↑(aeval x.coeff) (wittPolynomial p ℤ n)
⊢ ↑(ghostComponent n) (select P x) + ↑(ghostComponent n) (select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
simpa only [AlgHom.map_add, aeval_bind₁, ← coeff_select]
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ↑(bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + ↑(bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
[PROOFSTEP]
simp only [wittPolynomial_eq_sum_C_mul_X_pow, selectPoly, AlgHom.map_sum, AlgHom.map_pow, AlgHom.map_mul, bind₁_X_right,
  bind₁_C_right, ← Finset.sum_add_distrib, ← mul_add]
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ (Finset.sum (Finset.range (n + 1)) fun x =>
      ↑C (↑p ^ x) * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x))) =
    Finset.sum (Finset.range (n + 1)) fun x => ↑C (↑p ^ x) * X x ^ p ^ (n - x)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      ↑C (↑p ^ x) * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x)) =
        ↑C (↑p ^ x) * X x ^ p ^ (n - x)
[PROOFSTEP]
refine' fun m _ => mul_eq_mul_left_iff.mpr (Or.inl _)
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
⊢ (if P m then X m else 0) ^ p ^ (n - m) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
[PROOFSTEP]
rw [ite_pow, zero_pow (pow_pos hp.out.pos _)]
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
⊢ (if P m then X m ^ p ^ (n - m) else 0) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
[PROOFSTEP]
by_cases Pm : P m
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ (if P m then X m ^ p ^ (n - m) else 0) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
[PROOFSTEP]
rw [if_pos Pm, if_neg _, zero_pow, add_zero]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ 0 < p ^ (n - m)
[PROOFSTEP]
exact Fin.size_positive'
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ ¬¬P m
[PROOFSTEP]
exact not_not_intro Pm
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : ¬P m
⊢ (if P m then X m ^ p ^ (n - m) else 0) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
[PROOFSTEP]
rwa [if_neg Pm, if_pos, zero_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
let P : ℕ → Prop := fun n => y.coeff n = 0
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
haveI : DecidablePred P := Classical.decPred P
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
set z := mk p fun n => if P n then x.coeff n else y.coeff n
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
have hx : select P z = x := by
  ext1 n; rw [select, coeff_mk, coeff_mk]
  split_ifs with hn
  · rfl
  · rw [(h n).resolve_right hn]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
⊢ select P z = x
[PROOFSTEP]
ext1 n
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
n : ℕ
⊢ coeff (select P z) n = coeff x n
[PROOFSTEP]
rw [select, coeff_mk, coeff_mk]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
n : ℕ
⊢ (if P n then if P n then coeff x n else coeff y n else 0) = coeff x n
[PROOFSTEP]
split_ifs with hn
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
n : ℕ
hn : P n
⊢ coeff x n = coeff x n
[PROOFSTEP]
rfl
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
n : ℕ
hn : ¬P n
⊢ 0 = coeff x n
[PROOFSTEP]
rw [(h n).resolve_right hn]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
have hy : select (fun i => ¬P i) z = y := by
  ext1 n; rw [select, coeff_mk, coeff_mk]
  split_ifs with hn
  · exact hn.symm
  · rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
⊢ select (fun i => ¬P i) z = y
[PROOFSTEP]
ext1 n
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
n : ℕ
⊢ coeff (select (fun i => ¬P i) z) n = coeff y n
[PROOFSTEP]
rw [select, coeff_mk, coeff_mk]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
n : ℕ
⊢ (if ¬P n then if P n then coeff x n else coeff y n else 0) = coeff y n
[PROOFSTEP]
split_ifs with hn
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
n : ℕ
hn : P n
⊢ 0 = coeff y n
[PROOFSTEP]
exact hn.symm
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
n : ℕ
hn : ¬P n
⊢ coeff y n = coeff y n
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
calc
  (x + y).coeff n = z.coeff n := by rw [← hx, ← hy, select_add_select_not P z]
  _ = x.coeff n + y.coeff n := by
    simp [mk]
    split_ifs with y0
    · rw [y0, add_zero]
    · rw [h n |>.resolve_right y0, zero_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ coeff (x + y) n = coeff z n
[PROOFSTEP]
rw [← hx, ← hy, select_add_select_not P z]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ coeff z n = coeff x n + coeff y n
[PROOFSTEP]
simp [mk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ (if coeff y n = 0 then coeff x n else coeff y n) = coeff x n + coeff y n
[PROOFSTEP]
split_ifs with y0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
y0 : coeff y n = 0
⊢ coeff x n = coeff x n + coeff y n
[PROOFSTEP]
rw [y0, add_zero]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
y0 : ¬coeff y n = 0
⊢ coeff y n = coeff x n + coeff y n
[PROOFSTEP]
rw [h n |>.resolve_right y0, zero_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ init n x + tail n x = x
[PROOFSTEP]
simp only [init, tail, ← not_lt, select_add_select_not]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ init n (init n x) = init n x
[PROOFSTEP]
rw [ext_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ ∀ (n_1 : ℕ), coeff (init n (init n x)) n_1 = coeff (init n x) n_1
[PROOFSTEP]
intro i
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
⊢ coeff (init n (init n x)) i = coeff (init n x) i
[PROOFSTEP]
simp only [WittVector.init, WittVector.select, WittVector.coeff_mk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
⊢ (if i < n then if i < n then coeff x i else 0 else 0) = if i < n then coeff x i else 0
[PROOFSTEP]
by_cases hi : i < n
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
hi : i < n
⊢ (if i < n then if i < n then coeff x i else 0 else 0) = if i < n then coeff x i else 0
[PROOFSTEP]
simp [hi]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
hi : ¬i < n
⊢ (if i < n then if i < n then coeff x i else 0 else 0) = if i < n then coeff x i else 0
[PROOFSTEP]
simp [hi]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ init n (x + y) = init n (init n x + init n y)
[PROOFSTEP]
init_ring using wittAdd_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ init n (x * y) = init n (init n x * init n y)
[PROOFSTEP]
init_ring using wittMul_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ init n (-x) = init n (-init n x)
[PROOFSTEP]
init_ring using wittNeg_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ init n (x - y) = init n (init n x - init n y)
[PROOFSTEP]
init_ring using wittSub_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ init n (m • x) = init n (m • init n x)
[PROOFSTEP]
init_ring using fun p [Fact (Nat.Prime p)] n => wittNSMul_vars p m n
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℤ
x : 𝕎 R
n : ℕ
⊢ init n (m • x) = init n (m • init n x)
[PROOFSTEP]
init_ring using fun p [Fact (Nat.Prime p)] n => wittZSMul_vars p m n
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ init n (x ^ m) = init n (init n x ^ m)
[PROOFSTEP]
init_ring using fun p [Fact (Nat.Prime p)] n => wittPow_vars p m n


[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
r : ℝ
hr : 0 ≤ r
A : Matrix m n α
⊢ ‖A‖ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r
[PROOFSTEP]
simp_rw [norm_def, pi_norm_le_iff_of_nonneg hr]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
r : ℝ≥0
A : Matrix m n α
⊢ ‖A‖₊ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r
[PROOFSTEP]
simp_rw [nnnorm_def, pi_nnnorm_le_iff]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
r : ℝ
hr : 0 < r
A : Matrix m n α
⊢ ‖A‖ < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r
[PROOFSTEP]
simp_rw [norm_def, pi_norm_lt_iff hr]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
r : ℝ≥0
hr : 0 < r
A : Matrix m n α
⊢ ‖A‖₊ < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r
[PROOFSTEP]
simp_rw [nnnorm_def, pi_nnnorm_lt_iff hr]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ ‖map A f‖₊ = ‖A‖₊
[PROOFSTEP]
simp only [nnnorm_def, Pi.nnnorm_def, Matrix.map_apply, hf]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : m → α
⊢ ‖col v‖₊ = ‖v‖₊
[PROOFSTEP]
simp [nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : n → α
⊢ ‖row v‖₊ = ‖v‖₊
[PROOFSTEP]
simp [nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = ‖v‖₊
[PROOFSTEP]
simp_rw [nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
⊢ (Finset.sup Finset.univ fun b => Finset.sup Finset.univ fun b_1 => ‖diagonal v b b_1‖₊) =
    Finset.sup Finset.univ fun b => ‖v b‖₊
[PROOFSTEP]
congr 1 with i : 1
[GOAL]
case e_f.h
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i : n
⊢ (Finset.sup Finset.univ fun b => ‖diagonal v i b‖₊) = ‖v i‖₊
[PROOFSTEP]
refine' le_antisymm (Finset.sup_le fun j hj => _) _
[GOAL]
case e_f.h.refine'_1
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case e_f.h.refine'_1.inl
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i : n
hj : i ∈ Finset.univ
⊢ ‖diagonal v i i‖₊ ≤ ‖v i‖₊
[PROOFSTEP]
rw [diagonal_apply_eq]
[GOAL]
case e_f.h.refine'_1.inr
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
hij : i ≠ j
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊
[PROOFSTEP]
rw [diagonal_apply_ne _ hij, nnnorm_zero]
[GOAL]
case e_f.h.refine'_1.inr
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
hij : i ≠ j
⊢ 0 ≤ ‖v i‖₊
[PROOFSTEP]
exact zero_le _
[GOAL]
case e_f.h.refine'_2
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ ≤ Finset.sup Finset.univ fun b => ‖diagonal v i b‖₊
[PROOFSTEP]
refine' Eq.trans_le _ (Finset.le_sup (Finset.mem_univ i))
[GOAL]
case e_f.h.refine'_2
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ = ‖diagonal v i i‖₊
[PROOFSTEP]
rw [diagonal_apply_eq]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
⊢ SeminormedAddCommGroup (m → PiLp 1 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NormedAddCommGroup α
⊢ NormedAddCommGroup (m → PiLp 1 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NormedField R
inst✝¹ : SeminormedAddCommGroup α
inst✝ : NormedSpace R α
⊢ NormedSpace R (m → PiLp 1 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖ = ↑(Finset.sup Finset.univ fun i => ∑ j : n, ‖A i j‖₊)
[PROOFSTEP]
change ‖fun i => (PiLp.equiv 1 _).symm (A i)‖ = _
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖fun i => ↑(PiLp.equiv 1 fun i => α).symm (A i)‖ = ↑(Finset.sup Finset.univ fun i => ∑ j : n, ‖A i j‖₊)
[PROOFSTEP]
simp [Pi.norm_def, PiLp.nnnorm_eq_sum ENNReal.one_ne_top]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ ‖col v‖₊ = ‖v‖₊
[PROOFSTEP]
rw [linfty_op_nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (Finset.sup Finset.univ fun i => ∑ j : Unit, ‖col v i j‖₊) = Finset.sup Finset.univ fun b => ‖v b‖₊
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ‖row v‖₊ = ∑ i : n, ‖v i‖₊
[PROOFSTEP]
simp [linfty_op_nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ↑(∑ i : n, ‖v i‖₊) = ∑ i : n, ‖v i‖
[PROOFSTEP]
simp [NNReal.coe_sum]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
⊢ ‖diagonal v‖₊ = ‖v‖₊
[PROOFSTEP]
rw [linfty_op_nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
⊢ (Finset.sup Finset.univ fun i => ∑ j : m, ‖diagonal v i j‖₊) = Finset.sup Finset.univ fun b => ‖v b‖₊
[PROOFSTEP]
congr 1 with i : 1
[GOAL]
case e_f.h
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊
[PROOFSTEP]
refine' (Finset.sum_eq_single_of_mem _ (Finset.mem_univ i) fun j _hj hij => _).trans _
[GOAL]
case e_f.h.refine'_1
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i j : m
_hj : j ∈ Finset.univ
hij : j ≠ i
⊢ ‖diagonal v i j‖₊ = 0
[PROOFSTEP]
rw [diagonal_apply_ne' _ hij, nnnorm_zero]
[GOAL]
case e_f.h.refine'_2
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ‖diagonal v i i‖₊ = ‖v i‖₊
[PROOFSTEP]
rw [diagonal_apply_eq]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
[PROOFSTEP]
simp_rw [linfty_op_nnnorm_def, Matrix.mul_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.sup Finset.univ fun i => ∑ x : n, ‖∑ j : m, A i j * B j x‖₊) ≤
    (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊) * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
calc
  (Finset.univ.sup fun i => ∑ k, ‖∑ j, A i j * B j k‖₊) ≤ Finset.univ.sup fun i => ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊ :=
    Finset.sup_mono_fun fun i _hi => Finset.sum_le_sum fun k _hk => nnnorm_sum_le_of_le _ fun j _hj => nnnorm_mul_le _ _
  _ = Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊ := by simp_rw [@Finset.sum_comm _ m n, Finset.mul_sum]
  _ ≤ Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ :=
    by
    refine Finset.sup_mono_fun fun i _hi => ?_
    gcongr with j hj
    exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj
  _ ≤ (Finset.univ.sup fun i => ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ :=
    by
    simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]
    rfl
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.sup Finset.univ fun i => ∑ k : n, ∑ j : m, ‖A i j‖₊ * ‖B j k‖₊) =
    Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊
[PROOFSTEP]
simp_rw [@Finset.sum_comm _ m n, Finset.mul_sum]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊) ≤
    Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
refine Finset.sup_mono_fun fun i _hi => ?_
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
⊢ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊ ≤ ∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
gcongr with j hj
[GOAL]
case h.bc
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
j : m
hj : j ∈ Finset.univ
⊢ ∑ k : n, ‖B j k‖₊ ≤ Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊) ≤
    (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊) * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ((Finset.sup Finset.univ fun a => ∑ x : m, ‖A a x‖₊) * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊) ≤
    (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊) * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
v : m → α
⊢ ‖mulVec A v‖₊ ≤ ‖A‖₊ * ‖v‖₊
[PROOFSTEP]
rw [← linfty_op_nnnorm_col (A.mulVec v), ← linfty_op_nnnorm_col v]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
v : m → α
⊢ ‖col (mulVec A v)‖₊ ≤ ‖A‖₊ * ‖col v‖₊
[PROOFSTEP]
exact linfty_op_nnnorm_mul A (col v)
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NormedAddCommGroup α
⊢ NormedAddCommGroup (PiLp 2 fun i => PiLp 2 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NormedField R
inst✝¹ : SeminormedAddCommGroup α
inst✝ : NormedSpace R α
⊢ NormedSpace R (PiLp 2 fun i => PiLp 2 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ ‖A‖₊ = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
change ‖(PiLp.equiv 2 _).symm <| fun i => (PiLp.equiv 2 _).symm <| fun j => A i j‖₊ = _
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ ‖↑(PiLp.equiv 2 fun i => (fun x => PiLp 2 fun j => α) fun j => A i j).symm fun i =>
        ↑(PiLp.equiv 2 fun j => α).symm fun j => A i j‖₊ =
    (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp_rw [PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt, NNReal.sqrt_eq_rpow, NNReal.rpow_two, PiLp.equiv_symm_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ ↑((∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)) = (∑ i : m, ∑ j : n, ‖A i j‖ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp [NNReal.coe_sum]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ ‖map A f‖₊ = ‖A‖₊
[PROOFSTEP]
simp_rw [frobenius_nnnorm_def, Matrix.map_apply, hf]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ ‖Aᵀ‖₊ = ‖A‖₊
[PROOFSTEP]
rw [frobenius_nnnorm_def, frobenius_nnnorm_def, Finset.sum_comm]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ (∑ y : m, ∑ x : n, ‖Aᵀ x y‖₊ ^ 2) ^ (1 / 2) = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp_rw [Matrix.transpose_apply]
  -- porting note: added
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : m → α
⊢ ‖row v‖ = ‖↑(PiLp.equiv 2 fun i => α).symm v‖
[PROOFSTEP]
rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : m → α
⊢ (∑ j : m, ‖row v default j‖ ^ 2) ^ (1 / 2) = (∑ i : m, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp only [row_apply, Real.rpow_two, PiLp.equiv_symm_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : n → α
⊢ ‖col v‖ = ‖↑(PiLp.equiv 2 fun i => α).symm v‖
[PROOFSTEP]
simp_rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : n → α
⊢ (∑ x : n, ‖col v x default‖ ^ 2) ^ (1 / 2) = (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp only [col_apply, Real.rpow_two, PiLp.equiv_symm_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = ‖↑(PiLp.equiv 2 fun i => α).symm v‖₊
[PROOFSTEP]
simp_rw [frobenius_nnnorm_def, ← Finset.sum_product', Finset.univ_product_univ, PiLp.nnnorm_eq_of_L2]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
⊢ (∑ x : n × n, ‖diagonal v x.fst x.snd‖₊ ^ 2) ^ (1 / 2) =
    ↑NNReal.sqrt (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖₊ ^ 2)
[PROOFSTEP]
let s := (Finset.univ : Finset n).map ⟨fun i : n => (i, i), fun i j h => congr_arg Prod.fst h⟩
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
⊢ (∑ x : n × n, ‖diagonal v x.fst x.snd‖₊ ^ 2) ^ (1 / 2) =
    ↑NNReal.sqrt (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖₊ ^ 2)
[PROOFSTEP]
rw [← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
⊢ (∑ x in s, ‖diagonal v x.fst x.snd‖₊ ^ 2) ^ (1 / 2) =
    ↑NNReal.sqrt (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖₊ ^ 2)
[PROOFSTEP]
rw [Finset.sum_map, NNReal.sqrt_eq_rpow]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
⊢ (∑ x : n,
        ‖diagonal v
              (↑{ toFun := fun i => (i, i),
                      inj' :=
                        (_ :
                          ∀ (i j : n),
                            (fun i => (i, i)) i = (fun i => (i, i)) j →
                              ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
                  x).fst
              (↑{ toFun := fun i => (i, i),
                      inj' :=
                        (_ :
                          ∀ (i j : n),
                            (fun i => (i, i)) i = (fun i => (i, i)) j →
                              ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
                  x).snd‖₊ ^
          2) ^
      (1 / 2) =
    (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
⊢ (∑ x : n, ‖diagonal v x x‖₊ ^ 2) ^ (1 / 2) = (∑ i : n, ‖v i‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp_rw [diagonal_apply_eq, NNReal.rpow_two]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : ¬i ∈ s
⊢ ‖diagonal v i.fst i.snd‖₊ ^ 2 = 0
[PROOFSTEP]
suffices i.1 ≠ i.2 by rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : ¬i ∈ s
this : i.fst ≠ i.snd
⊢ ‖diagonal v i.fst i.snd‖₊ ^ 2 = 0
[PROOFSTEP]
rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : ¬i ∈ s
⊢ i.fst ≠ i.snd
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : ¬i ∈ s
h : i.fst = i.snd
⊢ False
[PROOFSTEP]
exact Finset.mem_map.not.mp his ⟨i.1, Finset.mem_univ _, Prod.ext rfl h⟩
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ‖1‖₊ = ↑NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
[PROOFSTEP]
refine'
  (frobenius_nnnorm_diagonal _).trans
    _
      -- porting note: change to erw, since `fun x => 1` no longer matches `Function.const`
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ‖↑(PiLp.equiv 2 fun i => α).symm fun x => 1‖₊ = ↑NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
[PROOFSTEP]
erw [PiLp.nnnorm_equiv_symm_const ENNReal.two_ne_top]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ↑(Fintype.card n) ^ ENNReal.toReal (1 / 2) * ‖1‖₊ = ↑NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
[PROOFSTEP]
simp_rw [NNReal.sqrt_eq_rpow]
  -- porting note: added `ENNReal.toReal_ofNat`
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ↑(Fintype.card n) ^ ENNReal.toReal (1 / 2) * ‖1‖₊ = ↑(Fintype.card n) ^ (1 / 2) * ‖1‖₊
[PROOFSTEP]
simp only [ENNReal.toReal_div, ENNReal.one_toReal, ENNReal.toReal_ofNat]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
[PROOFSTEP]
simp_rw [frobenius_nnnorm_def, Matrix.mul_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2) ^ (1 / 2) ≤
    (∑ i : l, ∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ i : m, ∑ j : n, ‖B i j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
rw [← NNReal.mul_rpow, @Finset.sum_comm _ n m, Finset.sum_mul_sum, Finset.sum_product]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2) ^ (1 / 2) ≤
    (∑ x : l, ∑ y : n, (∑ j : m, ‖A (x, y).fst j‖₊ ^ 2) * ∑ x_1 : m, ‖B x_1 (x, y).snd‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
refine' NNReal.rpow_le_rpow _ one_half_pos.le
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
⊢ ∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2 ≤
    ∑ x : l, ∑ y : n, (∑ j : m, ‖A (x, y).fst j‖₊ ^ 2) * ∑ x_1 : m, ‖B x_1 (x, y).snd‖₊ ^ 2
[PROOFSTEP]
refine' Finset.sum_le_sum fun i _ => Finset.sum_le_sum fun j _ => _
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
i : l
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ^ 2 ≤ (∑ j_1 : m, ‖A (i, j).fst j_1‖₊ ^ 2) * ∑ x : m, ‖B x (i, j).snd‖₊ ^ 2
[PROOFSTEP]
rw [← NNReal.rpow_le_rpow_iff one_half_pos, ← NNReal.rpow_mul, mul_div_cancel' (1 : ℝ) two_ne_zero, NNReal.rpow_one,
  NNReal.mul_rpow]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
i : l
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤
    (∑ j_1 : m, ‖A (i, j).fst j_1‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x (i, j).snd‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
i : l
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤ (∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
have :=
  @nnnorm_inner_le_nnnorm α _ _ _ _ ((PiLp.equiv 2 fun _ => α).symm fun j => star (A i j))
    ((PiLp.equiv 2 fun _ => α).symm fun k => B k j)
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
i : l
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
this :
  ‖inner (↑(PiLp.equiv 2 fun x => α).symm fun j => star (A i j)) (↑(PiLp.equiv 2 fun x => α).symm fun k => B k j)‖₊ ≤
    ‖↑(PiLp.equiv 2 fun x => α).symm fun j => star (A i j)‖₊ * ‖↑(PiLp.equiv 2 fun x => α).symm fun k => B k j‖₊
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤ (∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simpa only [PiLp.equiv_symm_apply, PiLp.inner_apply, IsROrC.inner_apply, starRingEnd_apply, Pi.nnnorm_def,
  PiLp.nnnorm_eq_of_L2, star_star, nnnorm_star, NNReal.sqrt_eq_rpow, NNReal.rpow_two] using this


[GOAL]
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
H : ∀ (x : X), ∃ U, U ∈ 𝓝 x ∧ ∃ g, ContinuousOn g U ∧ ∀ (y : X), y ∈ U → g y ∈ t y
⊢ ∃ g, ∀ (x : X), ↑g x ∈ t x
[PROOFSTEP]
choose U hU g hgc hgt using H
[GOAL]
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
⊢ ∃ g, ∀ (x : X), ↑g x ∈ t x
[PROOFSTEP]
obtain ⟨f, hf⟩ :=
  PartitionOfUnity.exists_isSubordinate isClosed_univ (fun x => interior (U x)) (fun x => isOpen_interior) fun x _ =>
    mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
[GOAL]
case intro
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X univ
hf : PartitionOfUnity.IsSubordinate f fun x => interior (U x)
⊢ ∃ g, ∀ (x : X), ↑g x ∈ t x
[PROOFSTEP]
refine'
  ⟨⟨fun x => ∑ᶠ i, f i x • g i x,
      hf.continuous_finsum_smul (fun i => isOpen_interior) fun i => (hgc i).mono interior_subset⟩,
    fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ _) (ht _)⟩
[GOAL]
case intro
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X univ
hf : PartitionOfUnity.IsSubordinate f fun x => interior (U x)
x i : X
hi : ↑(↑f i) x ≠ 0
⊢ x ∈ U i
[PROOFSTEP]
exact interior_subset (hf _ <| subset_closure hi)