English
If a continuous multilinear map p of order n satisfies a bound of the form (p(y,...,y)) = O(||y||^{n+1}) near 0, then p vanishes on the diagonal: (p(·,...,·))(y) = 0 for all y.
Русский
Если многочлена p порядка n удовлетворяет ограничению вида p(y,...,y) = O(||y||^{n+1}) около 0, то p на диагонали равен нулю.
LaTeX
$$$\\forall y\\in E,\\ (p\\text{ на диагонали }(y,...,y))=0.$$$
Lean4
theorem continuousMultilinearMap_apply_eq_zero {n : ℕ} {p : E [×n]→L[𝕜] F}
(h : (fun y => p fun _ => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)) (y : E) : (p fun _ => y) = 0 :=
by
obtain ⟨c, c_pos, hc⟩ := h.exists_pos
obtain ⟨t, ht, t_open, z_mem⟩ := eventually_nhds_iff.mp (isBigOWith_iff.mp hc)
obtain ⟨δ, δ_pos, δε⟩ := (Metric.isOpen_iff.mp t_open) 0 z_mem
clear h hc z_mem
rcases n with - | n
·
exact
norm_eq_zero.mp
(by
simpa only [fin0_apply_norm, norm_eq_zero, norm_zero, zero_add, pow_one, mul_zero, norm_le_zero_iff] using
ht 0 (δε (Metric.mem_ball_self δ_pos)))
· refine Or.elim (Classical.em (y = 0)) (fun hy => by simpa only [hy] using p.map_zero) fun hy => ?_
replace hy := norm_pos_iff.mpr hy
refine norm_eq_zero.mp (le_antisymm (le_of_forall_pos_le_add fun ε ε_pos => ?_) (norm_nonneg _))
have h₀ := _root_.mul_pos c_pos (pow_pos hy (n.succ + 1))
obtain ⟨k, k_pos, k_norm⟩ :=
NormedField.exists_norm_lt 𝕜 (lt_min (mul_pos δ_pos (inv_pos.mpr hy)) (mul_pos ε_pos (inv_pos.mpr h₀)))
have h₁ : ‖k • y‖ < δ := by
rw [norm_smul]
exact inv_mul_cancel_right₀ hy.ne.symm δ ▸ mul_lt_mul_of_pos_right (lt_of_lt_of_le k_norm (min_le_left _ _)) hy
have h₂ :=
calc
‖p fun _ => k • y‖ ≤ c * ‖k • y‖ ^ (n.succ + 1) := by
simpa only [norm_pow, _root_.norm_norm] using ht (k • y) (δε (mem_ball_zero_iff.mpr h₁))
_ = ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) :=
by
simp only [norm_smul, mul_pow]
ring
have h₃ : ‖k‖ * (c * ‖y‖ ^ (n.succ + 1)) < ε :=
inv_mul_cancel_right₀ h₀.ne.symm ε ▸ mul_lt_mul_of_pos_right (lt_of_lt_of_le k_norm (min_le_right _ _)) h₀
calc
‖p fun _ => y‖ = ‖k⁻¹ ^ n.succ‖ * ‖p fun _ => k • y‖ := by
simpa only [inv_smul_smul₀ (norm_pos_iff.mp k_pos), norm_smul, Finset.prod_const, Finset.card_fin] using
congr_arg norm (p.map_smul_univ (fun _ : Fin n.succ => k⁻¹) fun _ : Fin n.succ => k • y)
_ ≤ ‖k⁻¹ ^ n.succ‖ * (‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))) := by gcongr
_ = ‖(k⁻¹ * k) ^ n.succ‖ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) :=
by
rw [← mul_assoc]
simp [norm_mul, mul_pow]
_ ≤ 0 + ε := by
rw [inv_mul_cancel₀ (norm_pos_iff.mp k_pos)]
simpa using h₃.le
