internlm/Lean-Github huggingface dataset:
Theorem: norm_iteratedFDerivWithin_prod_le
Proof state before:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
⊢ ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
Tactic:
have hji : j ≠ i := fun h ↦ hi <| by simpa [h] using hj
Proof state after:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
hji : j ≠ i
⊢ ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
Theorem: norm_iteratedFDerivWithin_prod_le
Proof state before:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
hji : j ≠ i
⊢ ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
Tactic:
rw [Sym.count_coe_fill_of_ne hji]
Proof state after:
no goals
Theorem: norm_iteratedFDerivWithin_prod_le
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  (∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) →
    ∀ {n : ℕ},
      ↑n ≤ N →
        ‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
⊢ ∀ (i_1 : { x // x ∈ Finset.sym (insert i u) n }), i_1 ∈ Finset.univ ↔ (Finset.symInsertEquiv hi) i_1 ∈ Finset.univ
Tactic:
simp
Proof state after:
no goals
Theorem: norm_iteratedFDerivWithin_prod_le
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  (∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) →
    ∀ {n : ℕ},
      ↑n ≤ N →
        ‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
⊢ ∀ i_1 ∈ Finset.univ,
    ↑(Multiset.multinomial ↑↑i_1) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖ =
      ((fun v =>
            ↑(Multiset.multinomial v) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm)
        ((Finset.symInsertEquiv hi) i_1)
Tactic:
simp only [← comp_apply (g := Finset.symInsertEquiv hi), comp.assoc]
Proof state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  (∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) →
    ∀ {n : ℕ},
      ↑n ≤ N →
        ‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
⊢ ∀ i_1 ∈ Finset.univ,
    ↑(Multiset.multinomial ↑↑i_1) *
        ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑↑i_1) (f x_1) s x‖ =
      ((fun v =>
            ↑(Multiset.multinomial v) *
              ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 v) (f x_1) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm ∘ ⇑(Finset.symInsertEquiv hi))
        i_1
Theorem: norm_iteratedFDerivWithin_prod_le
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  (∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) →
    ∀ {n : ℕ},
      ↑n ≤ N →
        ‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
⊢ ∀ i_1 ∈ Finset.univ,
    ↑(Multiset.multinomial ↑↑i_1) *
        ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑↑i_1) (f x_1) s x‖ =
      ((fun v =>
            ↑(Multiset.multinomial v) *
              ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 v) (f x_1) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm ∘ ⇑(Finset.symInsertEquiv hi))
        i_1
Tactic:
simp
Proof state after:
no goals
Theorem: norm_iteratedFDerivWithin_prod_le
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ 0 ≤ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖
Tactic:
simp [mul_nonneg]
Proof state after:
no goals
Theorem: norm_iteratedFDerivWithin_prod_le
Proof state before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖) =
    ↑(Nat.choose n ↑m) * ↑(Multiset.multinomial ↑p) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Tactic:
ring
Proof state after:
no goals
Theorem: norm_iteratedFDerivWithin_prod_le
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
h : j = i
⊢ i ∈ u
Tactic:
simpa [h] using hj
Proof state after:
no goals
Theorem: norm_iteratedFDeriv_prod_le
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
u : Finset ι
f : ι → E → A'
N : ℕ∞
hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun x => ∏ j in u, f j x) x‖ ≤
    ∑ p in Finset.sym u n, ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDeriv 𝕜 (Multiset.count j ↑p) (f j) x‖
Tactic:
simpa [iteratedFDerivWithin_univ] using
  norm_iteratedFDerivWithin_prod_le (fun i hi ↦ (hf i hi).contDiffOn) uniqueDiffOn_univ trivial hn
Proof state after:
no goals
Theorem: fderiv_iteratedFDeriv_apply_comm
Proof state before:
ι : Type u_1
inst✝¹¹ : Fintype ι
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
F : Type u_5
G : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
α : Type u_7
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace 𝕜 α
n : ℕ
f : F → G
m : Fin n → F
x v : F
hf : ContDiff 𝕜 (↑(Nat.succ n)) f
⊢ ↑n < ↑(Nat.succ n)
Tactic:
norm_cast
Proof state after:
ι : Type u_1
inst✝¹¹ : Fintype ι
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
F : Type u_5
G : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
α : Type u_7
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace 𝕜 α
n : ℕ
f : F → G
m : Fin n → F
x v : F
hf : ContDiff 𝕜 (↑(Nat.succ n)) f
⊢ n < Nat.succ n
Theorem: fderiv_iteratedFDeriv_apply_comm
Proof state before:
ι : Type u_1
inst✝¹¹ : Fintype ι
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
F : Type u_5
G : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
α : Type u_7
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace 𝕜 α
n : ℕ
f : F → G
m : Fin n → F
x v : F
hf : ContDiff 𝕜 (↑(Nat.succ n)) f
⊢ n < Nat.succ n
Tactic:
simp
Proof state after:
no goals
Theorem: iteratedFDeriv_fderiv_apply_comm
Proof state before:
ι : Type u_1
inst✝¹¹ : Fintype ι
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
F : Type u_5
G : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
α : Type u_7
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace 𝕜 α
n : ℕ
f : F → G
x : F
m : Fin n → F
v : F
hf : ContDiff 𝕜 (↑(Nat.succ n)) f
⊢ (iteratedFDeriv 𝕜 n (fun y => (fderiv 𝕜 f y) v) x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) m) v
Tactic:
rw [contDiff_succ_iff_fderiv] at hf
Proof state after:
ι : Type u_1
inst✝¹¹ : Fintype ι
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
F : Type u_5
G : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
α : Type u_7
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace 𝕜 α
n : ℕ
f : F → G
x : F
m : Fin n → F
v : F
hf : Differentiable 𝕜 f ∧ ContDiff 𝕜 ↑n fun y => fderiv 𝕜 f y
⊢ (iteratedFDeriv 𝕜 n (fun y => (fderiv 𝕜 f y) v) x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) m) v
Theorem: iteratedFDeriv_fderiv_apply_comm
Proof state before:
ι : Type u_1
inst✝¹¹ : Fintype ι
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
F : Type u_5
G : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
α : Type u_7
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace 𝕜 α
n : ℕ
f : F → G
x : F
m : Fin n → F
v : F
hf : Differentiable 𝕜 f ∧ ContDiff 𝕜 ↑n fun y => fderiv 𝕜 f y
⊢ (iteratedFDeriv 𝕜 n (fun y => (fderiv 𝕜 f y) v) x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) m) v
Tactic:
rw [iteratedFDeriv_clm_apply_const_apply hf.right (le_refl _)]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.eq_empty
Proof state before:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
⊢ c = constOfIsEmpty 𝕜 E (c 0)
Tactic:
ext m
Proof state after:
case H
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ c m = (constOfIsEmpty 𝕜 E (c 0)) m
Theorem: ContinuousMultilinearMap.eq_empty
Proof state before:
case H
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ c m = (constOfIsEmpty 𝕜 E (c 0)) m
Tactic:
simp [Subsingleton.elim m 0]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.norm_empty
Proof state before:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ‖c x‖ = ‖c‖
Tactic:
rw [c.eq_empty]
Proof state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ‖(constOfIsEmpty 𝕜 E (c 0)) x‖ = ‖constOfIsEmpty 𝕜 E (c 0)‖
Theorem: ContinuousMultilinearMap.norm_empty
Proof state before:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ‖(constOfIsEmpty 𝕜 E (c 0)) x‖ = ‖constOfIsEmpty 𝕜 E (c 0)‖
Tactic:
rw [constOfIsEmpty_apply, norm_constOfIsEmpty]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty
Proof state before:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
⊢ Continuous fun y => constOfIsEmpty 𝕜 E y
Tactic:
rw [Metric.continuous_iff]
Proof state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
⊢ ∀ (b : G), ∀ ε > 0, ∃ δ > 0, ∀ (a : G), dist a b < δ → dist (constOfIsEmpty 𝕜 E a) (constOfIsEmpty 𝕜 E b) < ε