-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
/-- Controlling the norm of `f.iteratedFDeriv` when `f` is continuous multilinear. For the same
bound on the iterated derivative of `f` in the calculus sense,
see `ContinuousMultilinearMap.norm_iteratedFDeriv_le`. -/
lemma norm_iteratedFDeriv_le' (f : ContinuousMultilinearMap 𝕜 E₁ G) (k : ℕ) (x : (i : ι) → E₁ i) :
    ‖f.iteratedFDeriv k x‖
      ≤ Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Proof state:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
⊢ ∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) =
    ↑((Fintype.card ι).descFactorial k) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
simp [card_univ, mul_assoc]

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDeriv k x‖ ≤ ↑((Fintype.card ι).descFactorial k) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
calc ‖f.iteratedFDeriv k x‖
_ ≤ ∑ e : Fin k ↪ ι, ‖iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)‖ := norm_sum_le _ _
_ ≤ ∑ _ : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
  gcongr with e _
  simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x
_ = Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
  simp [card_univ, mul_assoc]

Result:
no goals

Proof state:
case h
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
e : Fin k ↪ ι
a✝ : e ∈ univ
⊢ ‖(f.iteratedFDerivComponent e.toEquivRange) fun i => x ↑i‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
⊢ ∑ e : Fin k ↪ ι, ‖(f.iteratedFDerivComponent e.toEquivRange) fun i => x ↑i‖ ≤
    ∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
gcongr with e _

Result:
case h
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
e : Fin k ↪ ι
a✝ : e ∈ univ
⊢ ‖(f.iteratedFDerivComponent e.toEquivRange) fun i => x ↑i‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Proof state:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDeriv k x‖ ≤ ↑((Fintype.card ι).descFactorial k) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
classical
calc ‖f.iteratedFDeriv k x‖
_ ≤ ∑ e : Fin k ↪ ι, ‖iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)‖ := norm_sum_le _ _
_ ≤ ∑ _ : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
  gcongr with e _
  simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x
_ = Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
  simp [card_univ, mul_assoc]

Result:
no goals