𝕜 : 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.4063834
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
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
⊢ ‖B‖ *
      ∑ i in Finset.range (n + 1),
        ↑(Nat.choose n i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ ≤
    ∑ i in Finset.range (n + 1),
      ↑(Nat.choose n i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
𝕜 : 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.4063834
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
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => ↑(↑B (f y)) (g y)) s x‖ ≤
    ∑ i in Finset.range (n + 1),
      ↑(Nat.choose n i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
apply (B.norm_iteratedFDerivWithin_le_of_bilinear hf hg hs hx hn).trans
𝕜 : 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.4063834
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
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
i : ℕ
⊢ 0 ≤ ↑(Nat.choose n i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
𝕜 : 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.4063834
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
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
⊢ ‖B‖ *
      ∑ i in Finset.range (n + 1),
        ↑(Nat.choose n i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ ≤
    ∑ i in Finset.range (n + 1),
      ↑(Nat.choose n i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
apply mul_le_of_le_one_left (Finset.sum_nonneg' fun i => ?_) hB
no goals
𝕜 : 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.4063834
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
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
i : ℕ
⊢ 0 ≤ ↑(Nat.choose n i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
positivity