Theorem: Along0.norm (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ ‖p.along0‖ ≤ ‖p‖
Tactic:
have pp : 0 ≤ ‖p‖ := by bound
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
⊢ ‖p.along0‖ ≤ ‖p‖

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
⊢ ‖p.along0‖ ≤ ‖p‖
Tactic:
apply p.along0.opNorm_le_bound pp
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
⊢ ∀ (m : Fin n → ℂ), ‖p.along0 m‖ ≤ ‖p‖ * Finset.univ.prod fun i => ‖m i‖

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
⊢ ∀ (m : Fin n → ℂ), ‖p.along0 m‖ ≤ ‖p‖ * Finset.univ.prod fun i => ‖m i‖
Tactic:
intro m
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ‖p.along0 m‖ ≤ ‖p‖ * Finset.univ.prod fun i => ‖m i‖

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ‖p.along0 m‖ ≤ ‖p‖ * Finset.univ.prod fun i => ‖m i‖
Tactic:
simp only [ContinuousMultilinearMap.along0,
  ContinuousMultilinearMap.compContinuousLinearMap_apply, Complex.norm_eq_abs]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => Complex.abs (m x)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => Complex.abs (m x)
Tactic:
have e : ∀ i : Fin n, abs (m i) = ‖idZeroLm (m i)‖ := by
  intro i
  simp only [idZeroLm, ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_id', id_eq,
    ContinuousLinearMap.zero_apply, Prod.norm_def, Complex.norm_eq_abs, norm_zero, ge_iff_le,
    apply_nonneg, max_eq_left]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
e : ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => Complex.abs (m x)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
e : ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => Complex.abs (m x)
Tactic:
simp_rw [e]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
e : ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => ‖idZeroLm (m x)‖

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
e : ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => ‖idZeroLm (m x)‖
Tactic:
exact ContinuousMultilinearMap.le_opNorm p _
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ 0 ≤ ‖p‖
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
Tactic:
intro i
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
i : Fin n
⊢ Complex.abs (m i) = ‖idZeroLm (m i)‖

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
i : Fin n
⊢ Complex.abs (m i) = ‖idZeroLm (m i)‖
Tactic:
simp only [idZeroLm, ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_id', id_eq,
  ContinuousLinearMap.zero_apply, Prod.norm_def, Complex.norm_eq_abs, norm_zero, ge_iff_le,
  apply_nonneg, max_eq_left]
State after:
no goals