internlm/Lean-Github huggingface dataset:
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case this.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
⊢ ∏ i : Fin n, ‖(f (Fin.succ i)) (x (Fin.succ i))‖ ≤ ∏ x_1 : Fin n, ‖f (Fin.succ x_1)‖ * ‖x (Fin.succ x_1)‖
Tactic:
exact Finset.prod_le_prod (fun _ _ ↦ norm_nonneg _) fun _ _ ↦
  ContinuousLinearMap.le_opNorm _ _
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.compContinuousLinearMapL_domDomCongr
Proof state before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ compContinuousLinearMapL f =
    ContinuousLinearMap.comp
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
      (ContinuousLinearMap.comp
        (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
        ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e)))
Tactic:
ext φ x
Proof state after:
case h.H
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((compContinuousLinearMapL f) φ) x =
    ((ContinuousLinearMap.comp
          (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
          (ContinuousLinearMap.comp
            (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
            ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e))))
        φ)
      x
Theorem: ContinuousMultilinearMap.compContinuousLinearMapL_domDomCongr
Proof state before:
case h.H
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((compContinuousLinearMapL f) φ) x =
    ((ContinuousLinearMap.comp
          (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
          (ContinuousLinearMap.comp
            (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
            ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e))))
        φ)
      x
Tactic:
suffices : (e.piCongrLeft' E₁).symm (fun i' ↦ f (e.symm i') (x (e.symm i'))) = fun i ↦ f i (x i)
Proof state after:
case h.H
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
this : ((Equiv.piCongrLeft' E₁ e).symm fun i' => (f (e.symm i')) (x (e.symm i'))) = fun i => (f i) (x i)
⊢ ((compContinuousLinearMapL f) φ) x =
    ((ContinuousLinearMap.comp
          (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
          (ContinuousLinearMap.comp
            (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
            ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e))))
        φ)
      x

case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((Equiv.piCongrLeft' E₁ e).symm fun i' => (f (e.symm i')) (x (e.symm i'))) = fun i => (f i) (x i)
Theorem: ContinuousMultilinearMap.compContinuousLinearMapL_domDomCongr
Proof state before:
case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((Equiv.piCongrLeft' E₁ e).symm fun i' => (f (e.symm i')) (x (e.symm i'))) = fun i => (f i) (x i)
Tactic:
refine funext ?_
Proof state after:
case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ∀ (x_1 : ι), (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) x_1 = (f x_1) (x x_1)
Theorem: ContinuousMultilinearMap.compContinuousLinearMapL_domDomCongr
Proof state before:
case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ∀ (x_1 : ι), (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) x_1 = (f x_1) (x x_1)
Tactic:
rw [Equiv.forall_congr_left' e]
Proof state after:
case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ∀ (y : ι'),
    (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) (e.symm y) =
      (f (e.symm y)) (x (e.symm y))
Theorem: ContinuousMultilinearMap.compContinuousLinearMapL_domDomCongr
Proof state before:
case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ∀ (y : ι'),
    (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) (e.symm y) =
      (f (e.symm y)) (x (e.symm y))
Tactic:
intro i'
Proof state after:
case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
i' : ι'
⊢ (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) (e.symm i') =
    (f (e.symm i')) (x (e.symm i'))
Theorem: ContinuousMultilinearMap.compContinuousLinearMapL_domDomCongr
Proof state before:
case this
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
i' : ι'
⊢ (Equiv.piCongrLeft' E₁ e).symm (fun i' => (f (e.symm i')) (x (e.symm i'))) (e.symm i') =
    (f (e.symm i')) (x (e.symm i'))
Tactic:
simp only [Equiv.piCongrLeft'_symm_apply_apply]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.compContinuousLinearMapL_domDomCongr
Proof state before:
case h.H
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ ι'
f : (i : ι) → E i →L[𝕜] E₁ i
φ : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
this : ((Equiv.piCongrLeft' E₁ e).symm fun i' => (f (e.symm i')) (x (e.symm i'))) = fun i => (f i) (x i)
⊢ ((compContinuousLinearMapL f) φ) x =
    ((ContinuousLinearMap.comp
          (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 E G e))))
          (ContinuousLinearMap.comp
            (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) f))
            ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 E₁ G e))))
        φ)
      x
Tactic:
simp [coe_domDomCongrₗᵢ', coe_domDomCongrₗᵢ'_symm, this, -Equiv.piCongrLeft'_symm_apply]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL
Proof state before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
⊢ Continuous fun f => compContinuousLinearMapL f
Tactic:
have e := Fintype.equivFin ι
Proof state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun f => compContinuousLinearMapL f
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL
Proof state before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun f => compContinuousLinearMapL f
Tactic:
rw [continuous_congr (compContinuousLinearMapL_domDomCongr G e)]
Proof state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun x =>
    ContinuousLinearMap.comp
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 (fun i => E i) G e))))
      (ContinuousLinearMap.comp
        (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) x))
        ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 (fun i => E₁ i) G e)))
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL
Proof state before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun x =>
    ContinuousLinearMap.comp
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm (domDomCongrₗᵢ' 𝕜 (fun i => E i) G e))))
      (ContinuousLinearMap.comp
        (compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) x))
        ↑(LinearIsometryEquiv.toContinuousLinearEquiv (domDomCongrₗᵢ' 𝕜 (fun i => E₁ i) G e)))
Tactic:
refine .clm_comp continuous_const (.clm_comp ?_ continuous_const)
Proof state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun x => compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) x)
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL
Proof state before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : ι ≃ Fin (Fintype.card ι)
⊢ Continuous fun x => compContinuousLinearMapL ((LinearIsometryEquiv.piCongrLeft' 𝕜 (fun i => E i →L[𝕜] E₁ i) e) x)
Tactic:
exact .comp (continuous_compContinuousLinearMapL_fin G) (LinearIsometryEquiv.continuous _)
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMap_right
Proof state before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : ContinuousMultilinearMap 𝕜 E₁ G
⊢ Continuous fun f => compContinuousLinearMap g f
Tactic:
simp only [← compContinuousLinearMapL_apply]
Proof state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : ContinuousMultilinearMap 𝕜 E₁ G
⊢ Continuous fun f => (compContinuousLinearMapL f) g
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMap_right
Proof state before:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁷ : Fintype ι
ι' : Type u_3
inst✝⁶ : Fintype ι'
E : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_6
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : ContinuousMultilinearMap 𝕜 E₁ G
⊢ Continuous fun f => (compContinuousLinearMapL f) g
Tactic:
exact .clm_apply (continuous_compContinuousLinearMapL G) continuous_const
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
⊢ (fderiv 𝕜 (fun f => compContinuousLinearMap g f) f) df =
    ∑ j : ι, compContinuousLinearMap g (Function.update f j (df j))
Tactic:
ext x
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
⊢ ((fderiv 𝕜 (fun f => compContinuousLinearMap g f) f) df) x =
    (∑ j : ι, compContinuousLinearMap g (Function.update f j (df j))) x
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
⊢ ((fderiv 𝕜 (fun f => compContinuousLinearMap g f) f) df) x =
    (∑ j : ι, compContinuousLinearMap g (Function.update f j (df j))) x
Tactic:
rw [← fderiv_continuousMultilinear_apply_const_apply h]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
⊢ (fderiv 𝕜 (fun y => (compContinuousLinearMap g y) x) f) df =
    (∑ j : ι, compContinuousLinearMap g (Function.update f j (df j))) x