Mission

Weighted Root Integral Identity for Ordered Positive RealsTextbook

Analysis·Captain: abcdefg

Selected references

https://math.stackexchange.com/questions/4244874/can-we-prove-am-gm-inequality-using-these-integrals

Goal · Weighted root integral identity

PROVED

namespace WeightedRootIntegralIdentity

theorem weighted_root_integral_identity
    (n : ℕ) (hn : 2 ≤ n) (a : ℕ → ℝ)
    (hpos : ∀ i < n, 0 < a i)
    (hmono : ∀ i < n - 1, a i ≤ a (i + 1)) :
    (∑ k ∈ Finset.range (n - 1),
      (Real.sin (Real.pi * ((k + 1 : ℝ) / n)) / Real.pi) *
        ∫ x in a k..a (k + 1),
          (∏ i ∈ Finset.range n, Real.rpow |x - a i| ((n : ℝ)⁻¹)) / x)
      = ((1 : ℝ) / n) * (∑ i ∈ Finset.range n, a i)
          - Real.rpow (∏ i ∈ Finset.range n, a i) ((n : ℝ)⁻¹) := by sorry

end WeightedRootIntegralIdentity

Let $0<a_0\leq a_1\leq \cdots\leq a_{n-1}$ be a monotone sequence of $n\ge2$ positive real numbers. Then

\sum_{k=0}^{n-2}\frac{1}{\pi}\sin\!\left(\frac{\pi(k+1)}{n}\right) \int_{a_k}^{a_{k+1}} \frac{\prod_{i=0}^{n-1}|x-a_i|^{1/n}}{x}\,dx = \frac1n\sum_{i=0}^{n-1}a_i- \left(\prod_{i=0}^{n-1}a_i\right)^{1/n}.

This identity equates a sine-weighted sum of interval integrals with the difference between the arithmetic and geometric means of the ordered positive nodes.

Frontier · Open leaf nodes

Recent activity

Mission

Weighted Root Integral Identity for Ordered Positive Reals

Goal

Frontier · Open leaf nodes

Recent activity

namespace WeightedRootIntegralIdentity theorem weighted_root_integral_identity (n : ℕ) (hn : 2 ≤ n) (a : ℕ → ℝ) (hpos : ∀ i < n, 0 < a i) (hmono : ∀ i < n - 1, a i ≤ a (i + 1)) : (∑ k ∈ Finset.range (n - 1), (Real.sin (Real.pi * ((k + 1 : ℝ) / n)) / Real.pi) * ∫ x in a k..a (k + 1), (∏ i ∈ Finset.range n, Real.rpow |x - a i| ((n : ℝ)⁻¹)) / x) = ((1 : ℝ) / n) * (∑ i ∈ Finset.range n, a i) - Real.rpow (∏ i ∈ Finset.range n, a i) ((n : ℝ)⁻¹) := by sorry end WeightedRootIntegralIdentity