Skip to content

Landau–Kolmogorov inequality

4 fully proved

Landau–Kolmogorov inequality

TheoremLandau–Kolmogorov inequality#✓fully proved

Landau–Kolmogorov inequality on ℝ (case n = 2, k = 1): if f is twice continuously differentiable with |f| ≤ M₀ and |f''| ≤ M₂ everywhere, then (f' x)² ≤ 2 * M₀ * M₂ for every x.

theorem landau_inequality {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) {M₀ M₂ : ℝ}
    (hM₀ : ∀ x, |f x| ≤ M₀) (hM₂ : ∀ x, |deriv (deriv f) x| ≤ M₂) (x : ℝ) :
    (deriv f x) ^ 2 ≤ 2 * M₀ * M₂
Used by 3
Used byLandau's inequality \(M_1 \le 2\sqrt{M_0 M_2}\) · Landau–Kolmogorov inequality, square-root form · Landau–Kolmogorov inequality, complex-valued case

TheoremLandau–Kolmogorov inequality, square-root form#✓fully proved

Square-root form of the Landau–Kolmogorov inequality.

theorem landau_inequality_abs {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) {M₀ M₂ : ℝ}
    (hM₀ : ∀ x, |f x| ≤ M₀) (hM₂ : ∀ x, |deriv (deriv f) x| ≤ M₂) (x : ℝ) :
    |deriv f x| ≤ Real.sqrt (2 * M₀ * M₂)
Uses 1
Proof usesLandau–Kolmogorov inequality

TheoremLandau–Kolmogorov inequality, complex-valued case#✓fully proved

Landau–Kolmogorov inequality, complex-valued case (constant 4): if f : ℝ → ℂ is twice continuously differentiable with ‖f‖ ≤ M₀ and ‖f''‖ ≤ M₂ everywhere, then ‖f' x‖² ≤ 4 * M₀ * M₂ for every x. The constant 4 comes from applying the real inequality to the real and imaginary parts and adding.

theorem landau_inequality_complex {f : ℝ → ℂ} (hf : ContDiff ℝ 2 f) {M₀ M₂ : ℝ}
    (hM₀ : ∀ x, ‖f x‖ ≤ M₀) (hM₂ : ∀ x, ‖deriv (deriv f) x‖ ≤ M₂) (x : ℝ) :
    ‖deriv f x‖ ^ 2 ≤ 4 * M₀ * M₂
Uses 1
Proof usesLandau–Kolmogorov inequality

Landau's inequality

TheoremLandau's inequality \(M_1 \le 2\sqrt{M_0 M_2}\)#✓fully proved

For \(f \in C^2(\mathbb{R})\), let \(M_k = \sup_x |f^{(k)}(x)|\). Prove that \(M_1 \le 2\sqrt{M_0 M_2}\).

public theorem bddAbove_abs_deriv_and_iSup_le_two_mul_sqrt
    (f : ℝ → ℝ)
    (hf : ContDiff ℝ 2 f)
    (M : ℕ → ℝ)
    (hM : M = fun k => ⨆ x : ℝ, |iteratedDeriv k f x|)
    (hB0 : BddAbove (Set.range (fun x : ℝ => |iteratedDeriv 0 f x|)))
    (hB2 : BddAbove (Set.range (fun x : ℝ => |iteratedDeriv 2 f x|))) :
    BddAbove (Set.range (fun x : ℝ => |iteratedDeriv 1 f x|)) ∧
      M 1 ≤ 2 * Real.sqrt (M 0 * M 2)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Real functions; Inequalities in real analysis), problem ma_proofbench_l2_92.
Uses 1
Proof usesLandau–Kolmogorov inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.