integral_pow_mul_iteratedFDeriv_le

English

A repeated-right recursion identity for iteratedPDeriv, mirroring the succ_right relation.

Русский

Повторяющееся правое сопряжение для iteratedPDeriv, отражающее relation succ_right.

LaTeX

$$$iteratedPDeriv\ 𝕜\, m\ f = iteratedPDeriv\ 𝕜\, (Fin.init\, m)\ (pderivCLM\ 𝕜\ (m\ (Fin.last\, n))\ f)$$$

Lean4

theorem integral_pow_mul_iteratedFDeriv_le (f : 𝓢(D, V)) (k n : ℕ) :
    ∫ x, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ∂μ ≤
      2 ^ μ.integrablePower * (∫ x, (1 + ‖x‖) ^ (-(μ.integrablePower : ℝ)) ∂μ) *
        (SchwartzMap.seminorm 𝕜 0 n f + SchwartzMap.seminorm 𝕜 (k + μ.integrablePower) n f) :=
  integral_pow_mul_le_of_le_of_pow_mul_le (norm_iteratedFDeriv_le_seminorm ℝ _ _) (le_seminorm ℝ _ _ _)

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