internlm/Lean-Github huggingface dataset:
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
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)‖) = δ
⊢ δ ≤ δ₁
Tactic:
rw [← hδ_def]
Proof state after:
𝕜 : 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)‖) = δ
⊢ 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) ≤ δ₁
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
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)‖) = δ
⊢ 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) ≤ δ₁
Tactic:
exact le_trans inf_le_left inf_le_right
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
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δ : δ ≤ δ₁
⊢ 0 < δ
Tactic:
simp only [← hδ_def, lt_inf_iff]
Proof state after:
𝕜 : 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δ : δ ≤ δ₁
⊢ (0 < 1 ∧ 0 < δ₁) ∧ 0 < ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖)
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
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δ : δ ≤ δ₁
⊢ (0 < 1 ∧ 0 < δ₁) ∧ 0 < ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖)
Tactic:
refine And.intro (And.intro zero_lt_one hδ₁_pos) ?_
Proof state after:
𝕜 : 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δ : δ ≤ δ₁
⊢ 0 < ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖)
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
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δ : δ ≤ δ₁
⊢ 0 < ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖)
Tactic:
refine div_pos (half_pos hε_pos) ?_
Proof state after:
𝕜 : 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δ : δ ≤ δ₁
⊢ 0 < 1 + ∏ i : Fin n, ‖f (Fin.succ i)‖
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
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δ : δ ≤ δ₁
⊢ 0 < 1 + ∏ i : Fin n, ‖f (Fin.succ i)‖
Tactic:
exact add_pos_of_pos_of_nonneg zero_lt_one (Finset.prod_nonneg fun _ _ ↦ norm_nonneg _)
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
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₂
⊢ C₁ < ε / 2
Tactic:
simp only [← hC₁_def, ← hε₁_def]
Proof state after:
𝕜 : 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₂
⊢ ε / 2 / (2 + ‖f 0‖) * (δ + ‖f 0‖) < ε / 2
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
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₂
⊢ ε / 2 / (2 + ‖f 0‖) * (δ + ‖f 0‖) < ε / 2
Tactic:
rw [div_mul_eq_mul_div]
Proof state after:
𝕜 : 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₂
⊢ ε / 2 * (δ + ‖f 0‖) / (2 + ‖f 0‖) < ε / 2
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
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₂
⊢ ε / 2 * (δ + ‖f 0‖) / (2 + ‖f 0‖) < ε / 2
Tactic:
rw [div_lt_iff <| add_pos_of_pos_of_nonneg zero_lt_two (norm_nonneg _)]
Proof state after:
𝕜 : 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₂
⊢ ε / 2 * (δ + ‖f 0‖) < ε / 2 * (2 + ‖f 0‖)
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
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₂
⊢ ε / 2 * (δ + ‖f 0‖) < ε / 2 * (2 + ‖f 0‖)
Tactic:
refine mul_lt_mul_of_pos_left (add_lt_add_right ?_ _) (half_pos hε_pos)
Proof state after:
𝕜 : 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₂
⊢ δ < 2
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
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₂
⊢ δ < 2
Tactic:
rw [← hδ_def]
Proof state after:
𝕜 : 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₂
⊢ 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) < 2
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
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₂
⊢ 1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖) < 2
Tactic:
exact inf_lt_of_left_lt <| inf_lt_of_left_lt one_lt_two
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
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
⊢ C₂ < ε / 2
Tactic:
simp only [← hC₂_def, ← hε₁_def, ← hδ_def]
Proof state after:
𝕜 : 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
⊢ (1 ⊓ δ₁ ⊓ ε / 2 / (1 + ∏ i : Fin n, ‖f (Fin.succ i)‖)) * ∏ i : Fin n, ‖f (Fin.succ i)‖ < ε / 2