internlm/Lean-Github huggingface dataset:
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case succ.intro.intro
𝕜 : 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₁
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Tactic:
have hC₂_nonneg : 0 ≤ C₂ := by
  rw [← hC₂_def]
  exact mul_nonneg hδ_pos.le <| Finset.prod_nonneg fun _ _ ↦ norm_nonneg _
Proof state after:
case succ.intro.intro
𝕜 : 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₂
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case succ.intro.intro
𝕜 : 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₂
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Tactic:
use δ
Proof state after:
case h
𝕜 : 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₂
⊢ δ > 0 ∧
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h
𝕜 : 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₂
⊢ δ > 0 ∧
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Tactic:
refine And.intro hδ_pos ?_
Proof state after:
case h
𝕜 : 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₂
⊢ ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
    ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h
𝕜 : 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₂
⊢ ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
    ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Tactic:
intro g
Proof state after:
case h
𝕜 : 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
⊢ ‖g - f‖ < δ → ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h
𝕜 : 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
⊢ ‖g - f‖ < δ → ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
Tactic:
intro hgf
Proof state after:
case h
𝕜 : 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‖ < δ
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h
𝕜 : 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‖ < δ
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
Tactic:
rw [← Fin.cons_self_tail (g - f)] at hgf
Proof state after:
case h
𝕜 : 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 : ‖Fin.cons ((g - f) 0) (Fin.tail (g - f))‖ < δ
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h
𝕜 : 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 : ‖Fin.cons ((g - f) 0) (Fin.tail (g - f))‖ < δ
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
Tactic:
rw [Fin.cons.norm, sup_lt_iff] at hgf
Proof state after:
case h
𝕜 : 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)‖ < δ
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h
𝕜 : 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)‖ < δ
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
Tactic:
refine lt_of_le_of_lt ?_ hC
Proof state after:
case h
𝕜 : 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)‖ < δ
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ ≤ C₁ + C₂
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case h
𝕜 : 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)‖ < δ
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ ≤ C₁ + C₂
Tactic:
rw [ContinuousLinearMap.opNorm_le_iff (add_nonneg hC₁_nonneg hC₂_nonneg)]
Proof state after:
case h
𝕜 : 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)‖ < δ
⊢ ∀ (x : ContinuousMultilinearMap 𝕜 E₁ G),
    ‖(compContinuousLinearMapL g - compContinuousLinearMapL f) x‖ ≤ (C₁ + C₂) * ‖x‖