internlm/Lean-Github huggingface dataset:
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case this
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
e : ContinuousMultilinearMap 𝕜 E₁ G ≃ₗᵢ[𝕜] E₁ 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E₁ (Fin.succ i)) G
he_q : ∀ (x : E₁ 0) (v : (i : Fin n) → E₁ (Fin.succ i)), ((e q) x) v = q (Fin.cons x v)
IH :
  ‖q (Fin.cons ((g 0) (x 0)) fun i => (g (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i)))‖ ≤
    ε₁ * ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖
⊢ ‖g 0‖ * ‖x 0‖ ≤ (δ + ‖f 0‖) * ‖x 0‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
Proof state after:
case this
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
e : ContinuousMultilinearMap 𝕜 E₁ G ≃ₗᵢ[𝕜] E₁ 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E₁ (Fin.succ i)) G
he_q : ∀ (x : E₁ 0) (v : (i : Fin n) → E₁ (Fin.succ i)), ((e q) x) v = q (Fin.cons x v)
IH :
  ‖q (Fin.cons ((g 0) (x 0)) fun i => (g (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i)))‖ ≤
    ε₁ * ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖
⊢ ‖g 0‖ ≤ δ + ‖f 0‖
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case this
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
e : ContinuousMultilinearMap 𝕜 E₁ G ≃ₗᵢ[𝕜] E₁ 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E₁ (Fin.succ i)) G
he_q : ∀ (x : E₁ 0) (v : (i : Fin n) → E₁ (Fin.succ i)), ((e q) x) v = q (Fin.cons x v)
IH :
  ‖q (Fin.cons ((g 0) (x 0)) fun i => (g (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i)))‖ ≤
    ε₁ * ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖
⊢ ‖g 0‖ ≤ δ + ‖f 0‖
Tactic:
refine le_trans (norm_le_norm_add_norm_sub (f 0) (g 0)) ?_
Proof state after:
case this
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
e : ContinuousMultilinearMap 𝕜 E₁ G ≃ₗᵢ[𝕜] E₁ 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E₁ (Fin.succ i)) G
he_q : ∀ (x : E₁ 0) (v : (i : Fin n) → E₁ (Fin.succ i)), ((e q) x) v = q (Fin.cons x v)
IH :
  ‖q (Fin.cons ((g 0) (x 0)) fun i => (g (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i)))‖ ≤
    ε₁ * ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖
⊢ ‖f 0‖ + ‖f 0 - g 0‖ ≤ δ + ‖f 0‖
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case this
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
e : ContinuousMultilinearMap 𝕜 E₁ G ≃ₗᵢ[𝕜] E₁ 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E₁ (Fin.succ i)) G
he_q : ∀ (x : E₁ 0) (v : (i : Fin n) → E₁ (Fin.succ i)), ((e q) x) v = q (Fin.cons x v)
IH :
  ‖q (Fin.cons ((g 0) (x 0)) fun i => (g (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i)))‖ ≤
    ε₁ * ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖
⊢ ‖f 0‖ + ‖f 0 - g 0‖ ≤ δ + ‖f 0‖
Tactic:
rw [add_comm, norm_sub_rev]
Proof state after:
case this
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
e : ContinuousMultilinearMap 𝕜 E₁ G ≃ₗᵢ[𝕜] E₁ 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E₁ (Fin.succ i)) G
he_q : ∀ (x : E₁ 0) (v : (i : Fin n) → E₁ (Fin.succ i)), ((e q) x) v = q (Fin.cons x v)
IH :
  ‖q (Fin.cons ((g 0) (x 0)) fun i => (g (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i)))‖ ≤
    ε₁ * ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖
⊢ ‖g 0 - f 0‖ + ‖f 0‖ ≤ δ + ‖f 0‖
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case this
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
e : ContinuousMultilinearMap 𝕜 E₁ G ≃ₗᵢ[𝕜] E₁ 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E₁ (Fin.succ i)) G
he_q : ∀ (x : E₁ 0) (v : (i : Fin n) → E₁ (Fin.succ i)), ((e q) x) v = q (Fin.cons x v)
IH :
  ‖q (Fin.cons ((g 0) (x 0)) fun i => (g (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i)))‖ ≤
    ε₁ * ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖
⊢ ‖g 0 - f 0‖ + ‖f 0‖ ≤ δ + ‖f 0‖
Tactic:
exact add_le_add_right hgf.1.le _
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h.refine_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
e : ContinuousMultilinearMap 𝕜 E₁ G ≃ₗᵢ[𝕜] E₁ 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E₁ (Fin.succ i)) G
he_q : ∀ (x : E₁ 0) (v : (i : Fin n) → E₁ (Fin.succ i)), ((e q) x) v = q (Fin.cons x v)
IH :
  ‖q (Fin.cons ((g 0) (x 0)) fun i => (g (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i)))‖ ≤
    ε₁ * ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖
this : ‖(e q) ((g 0) (x 0))‖ ≤ ‖q‖ * ((δ + ‖f 0‖) * ‖x 0‖)
⊢ ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖ ≤ (δ + ‖f 0‖) * (‖q‖ * (‖x 0‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖))
Tactic:
exact le_trans
  (mul_le_mul_of_nonneg_right this (Finset.prod_nonneg fun _ _ ↦ norm_nonneg _))
  (le_of_eq (by ring))
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
e : ContinuousMultilinearMap 𝕜 E₁ G ≃ₗᵢ[𝕜] E₁ 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E₁ (Fin.succ i)) G
he_q : ∀ (x : E₁ 0) (v : (i : Fin n) → E₁ (Fin.succ i)), ((e q) x) v = q (Fin.cons x v)
IH :
  ‖q (Fin.cons ((g 0) (x 0)) fun i => (g (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i)))‖ ≤
    ε₁ * ‖(e q) ((g 0) (x 0))‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖
this : ‖(e q) ((g 0) (x 0))‖ ≤ ‖q‖ * ((δ + ‖f 0‖) * ‖x 0‖)
⊢ ‖q‖ * ((δ + ‖f 0‖) * ‖x 0‖) * ∏ i : Fin n, ‖x (Fin.succ i)‖ =
    (δ + ‖f 0‖) * (‖q‖ * (‖x 0‖ * ∏ i : Fin n, ‖x (Fin.succ i)‖))
Tactic:
ring
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
IH :
  ∀ (a : (i : Fin n) → E (Fin.succ i) →L[𝕜] E₁ (Fin.succ i)),
    ‖a - fun i => f (Fin.succ i)‖ < δ₁ →
      ‖compContinuousLinearMapL a - compContinuousLinearMapL fun i => f (Fin.succ i)‖ < ε₁
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
⊢ ‖q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i))) - q fun i => (f i) (x i)‖ ≤
    C₂ * ‖q‖ * ∏ i : Fin (Nat.succ n), ‖x i‖
Tactic:
rw [← Fin.cons_self_tail (fun i ↦ (f i) (x i)), Fin.tail_def]
Proof state after:
case h.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
IH :
  ∀ (a : (i : Fin n) → E (Fin.succ i) →L[𝕜] E₁ (Fin.succ i)),
    ‖a - fun i => f (Fin.succ i)‖ < δ₁ →
      ‖compContinuousLinearMapL a - compContinuousLinearMapL fun i => f (Fin.succ i)‖ < ε₁
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
⊢ ‖q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((f 0) (x 0)) fun k => (f (Fin.succ k)) (x (Fin.succ k)))‖ ≤
    C₂ * ‖q‖ * ∏ i : Fin (Nat.succ n), ‖x i‖
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
IH :
  ∀ (a : (i : Fin n) → E (Fin.succ i) →L[𝕜] E₁ (Fin.succ i)),
    ‖a - fun i => f (Fin.succ i)‖ < δ₁ →
      ‖compContinuousLinearMapL a - compContinuousLinearMapL fun i => f (Fin.succ i)‖ < ε₁
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
⊢ ‖q (Fin.cons ((g 0) (x 0)) fun i => (f (Fin.succ i)) (x (Fin.succ i))) -
        q (Fin.cons ((f 0) (x 0)) fun k => (f (Fin.succ k)) (x (Fin.succ k)))‖ ≤
    C₂ * ‖q‖ * ∏ i : Fin (Nat.succ n), ‖x i‖
Tactic:
simp (config := {singlePass := true}) only [← Fin.update_cons_zero 0]
Proof state after:
case h.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
IH :
  ∀ (a : (i : Fin n) → E (Fin.succ i) →L[𝕜] E₁ (Fin.succ i)),
    ‖a - fun i => f (Fin.succ i)‖ < δ₁ →
      ‖compContinuousLinearMapL a - compContinuousLinearMapL fun i => f (Fin.succ i)‖ < ε₁
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
⊢ ‖q (Function.update (Fin.cons 0 fun i => (f (Fin.succ i)) (x (Fin.succ i))) 0 ((g 0) (x 0))) -
        q (Function.update (Fin.cons 0 fun i => (f (Fin.succ i)) (x (Fin.succ i))) 0 ((f 0) (x 0)))‖ ≤
    C₂ * ‖q‖ * ∏ i : Fin (Nat.succ n), ‖x i‖
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
IH :
  ∀ (a : (i : Fin n) → E (Fin.succ i) →L[𝕜] E₁ (Fin.succ i)),
    ‖a - fun i => f (Fin.succ i)‖ < δ₁ →
      ‖compContinuousLinearMapL a - compContinuousLinearMapL fun i => f (Fin.succ i)‖ < ε₁
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
⊢ ‖q (Function.update (Fin.cons 0 fun i => (f (Fin.succ i)) (x (Fin.succ i))) 0 ((g 0) (x 0))) -
        q (Function.update (Fin.cons 0 fun i => (f (Fin.succ i)) (x (Fin.succ i))) 0 ((f 0) (x 0)))‖ ≤
    C₂ * ‖q‖ * ∏ i : Fin (Nat.succ n), ‖x i‖
Tactic:
rw [← map_sub]
Proof state after:
case h.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
δ₁ : ℝ
hδ₁_pos : δ₁ > 0
IH :
  ∀ (a : (i : Fin n) → E (Fin.succ i) →L[𝕜] E₁ (Fin.succ i)),
    ‖a - fun i => f (Fin.succ i)‖ < δ₁ →
      ‖compContinuousLinearMapL a - compContinuousLinearMapL fun i => f (Fin.succ i)‖ < ε₁
δ : ℝ
hδ_def : 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) = δ
hδ : δ ≤ δ₁
hδ_pos : 0 < δ
C₁ : ℝ
hC₁_def : ε₁ * (δ + ‖f 0‖) = C₁
C₂ : ℝ
hC₂_def : δ * ∏ i : Fin n, ‖f (Fin.succ i)‖ = C₂
hC₁ : C₁ < ε / 2
hC₂ : C₂ < ε / 2
hC : C₁ + C₂ < ε
hC₁_nonneg : 0 ≤ C₁
hC₂_nonneg : 0 ≤ C₂
g : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
hgf : ‖(g - f) 0‖ < δ ∧ ‖Fin.tail (g - f)‖ < δ
q : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : Fin (Nat.succ n)) → E i
⊢ ‖q (Function.update (Fin.cons 0 fun i => (f (Fin.succ i)) (x (Fin.succ i))) 0 ((g 0) (x 0) - (f 0) (x 0)))‖ ≤
    C₂ * ‖q‖ * ∏ i : Fin (Nat.succ n), ‖x i‖