F

Mathlib.Analysis.Complex.Hadamard

URI: https://scilib.ai/kg/mathlib#Complex.HadamardThreeLines.F

← MathLib Explorer

English

F f ε z is the product of invInterpStrip f z ε with f(z).

Русский

F f ε z есть произведение invInterpStrip f z ε на f(z).

LaTeX

$$$F(f,\varepsilon)(z) = \big( \mathrm{invInterpStrip}(f,z,\varepsilon) \big) \cdot f(z)$$$

Lean4

/-- A function useful for the proofs steps. We will aim to show that it is bounded by 1. -/
noncomputable def F [NormedSpace ℂ E] (ε : ℝ) := fun z ↦ invInterpStrip f z ε • f z

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru