11.10. HardyZeta.MomentAlgebra🔗

theorem integral_shifted_even_power {w : ℝ → ℝ} {μ : Measure ℝ} {a C : ℝ}
    (hi : ∀ n : ℕ, Integrable (fun t ↦ t ^ (2 * n) * w t) μ)
    (hm : ∀ n : ℕ, (∫ t, t ^ (2 * n) * w t ∂μ) = C * (-a) ^ n)
    (k : ℕ) :
    (∫ t, (t ^ 2 + a) ^ k * w t ∂μ) = C * ((-a) + a) ^ k := byw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕ⊢ ∫ (t : ℝ), (t ^ 2 + a) ^ k * w t ∂μ = C * (-a + a) ^ k
  have hexp (t : ℝ) : (t ^ 2 + a) ^ k * w t =
      ∑ j ∈ Finset.range (k + 1),
        (a ^ (k - j) * (k.choose j : ℝ)) * (t ^ (2 * j) * w t) := by
    rw [add_pow,w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕt:ℝ⊢ (∑ m ∈ Finset.range (k + 1), (t ^ 2) ^ m * a ^ (k - m) * ↑(k.choose m)) * w t =
  ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t) Finset.sum_mulw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕt:ℝ⊢ ∑ i ∈ Finset.range (k + 1), (t ^ 2) ^ i * a ^ (k - i) * ↑(k.choose i) * w t =
  ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)]w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕt:ℝ⊢ ∑ i ∈ Finset.range (k + 1), (t ^ 2) ^ i * a ^ (k - i) * ↑(k.choose i) * w t =
  ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)
    apply Finset.sum_congr rflw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕt:ℝ⊢ ∀ x ∈ Finset.range (k + 1),
  (t ^ 2) ^ x * a ^ (k - x) * ↑(k.choose x) * w t = a ^ (k - x) * ↑(k.choose x) * (t ^ (2 * x) * w t)
    intro j _w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕt:ℝj:ℕa✝:j ∈ Finset.range (k + 1)⊢ (t ^ 2) ^ j * a ^ (k - j) * ↑(k.choose j) * w t = a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)
    rw [← pow_mulw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕt:ℝj:ℕa✝:j ∈ Finset.range (k + 1)⊢ t ^ (2 * j) * a ^ (k - j) * ↑(k.choose j) * w t = a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)]w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕt:ℝj:ℕa✝:j ∈ Finset.range (k + 1)⊢ t ^ (2 * j) * a ^ (k - j) * ↑(k.choose j) * w t = a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)
    ringw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∫ (t : ℝ), (t ^ 2 + a) ^ k * w t ∂μ = C * (-a + a) ^ k
  simp_rw [w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∫ (t : ℝ), (t ^ 2 + a) ^ k * w t ∂μ = C * (-a + a) ^ khexpw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∫ (t : ℝ), ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t) ∂μ = C * (-a + a) ^ k]
  rw [integral_finsetSum _ (fun j _ ↦ (hi j).const_mul _)w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∑ i ∈ Finset.range (k + 1), ∫ (a_1 : ℝ), a ^ (k - i) * ↑(k.choose i) * (a_1 ^ (2 * i) * w a_1) ∂μ = C * (-a + a) ^ k]w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∑ i ∈ Finset.range (k + 1), ∫ (a_1 : ℝ), a ^ (k - i) * ↑(k.choose i) * (a_1 ^ (2 * i) * w a_1) ∂μ = C * (-a + a) ^ k
  simp_rw [w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∑ i ∈ Finset.range (k + 1), ∫ (a_1 : ℝ), a ^ (k - i) * ↑(k.choose i) * (a_1 ^ (2 * i) * w a_1) ∂μ = C * (-a + a) ^ kintegral_const_mul,w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∑ x ∈ Finset.range (k + 1), a ^ (k - x) * ↑(k.choose x) * ∫ (a : ℝ), a ^ (2 * x) * w a ∂μ = C * (-a + a) ^ k hmw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∑ x ∈ Finset.range (k + 1), a ^ (k - x) * ↑(k.choose x) * (C * (-a) ^ x) = C * (-a + a) ^ k]
  rw [add_pow,w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∑ x ∈ Finset.range (k + 1), a ^ (k - x) * ↑(k.choose x) * (C * (-a) ^ x) =
  C * ∑ m ∈ Finset.range (k + 1), (-a) ^ m * a ^ (k - m) * ↑(k.choose m) Finset.mul_sumw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∑ x ∈ Finset.range (k + 1), a ^ (k - x) * ↑(k.choose x) * (C * (-a) ^ x) =
  ∑ i ∈ Finset.range (k + 1), C * ((-a) ^ i * a ^ (k - i) * ↑(k.choose i))]w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∑ x ∈ Finset.range (k + 1), a ^ (k - x) * ↑(k.choose x) * (C * (-a) ^ x) =
  ∑ i ∈ Finset.range (k + 1), C * ((-a) ^ i * a ^ (k - i) * ↑(k.choose i))
  apply Finset.sum_congr rflw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)⊢ ∀ x ∈ Finset.range (k + 1), a ^ (k - x) * ↑(k.choose x) * (C * (-a) ^ x) = C * ((-a) ^ x * a ^ (k - x) * ↑(k.choose x))
  intro j _w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhexp:∀ (t : ℝ), (t ^ 2 + a) ^ k * w t = ∑ j ∈ Finset.range (k + 1), a ^ (k - j) * ↑(k.choose j) * (t ^ (2 * j) * w t)j:ℕa✝:j ∈ Finset.range (k + 1)⊢ a ^ (k - j) * ↑(k.choose j) * (C * (-a) ^ j) = C * ((-a) ^ j * a ^ (k - j) * ↑(k.choose j))
  ringAll goals completed! 🐙

theorem integral_shifted_even_power_eq_zero {w : ℝ → ℝ} {μ : Measure ℝ} {a C : ℝ}
    (hi : ∀ n : ℕ, Integrable (fun t ↦ t ^ (2 * n) * w t) μ)
    (hm : ∀ n : ℕ, (∫ t, t ^ (2 * n) * w t ∂μ) = C * (-a) ^ n)
    {k : ℕ} (hk : k ≠ 0) : (∫ t, (t ^ 2 + a) ^ k * w t ∂μ) = 0 := byw:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhk:k ≠ 0⊢ ∫ (t : ℝ), (t ^ 2 + a) ^ k * w t ∂μ = 0
  rw [integral_shifted_even_power hi hm,w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhk:k ≠ 0⊢ C * (-a + a) ^ k = 0 neg_add_cancel,w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhk:k ≠ 0⊢ C * 0 ^ k = 0 zero_pow hk,w:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhk:k ≠ 0⊢ C * 0 = 0 mul_zerow:ℝ → ℝμ:Measure ℝa:ℝC:ℝhi:∀ (n : ℕ), Integrable (fun t => t ^ (2 * n) * w t) μhm:∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ nk:ℕhk:k ≠ 0⊢ 0 = 0]All goals completed! 🐙

/-- The growing tail cannot be bounded by the smaller compact-interval scale. -/

theorem not_geometric_domination {m R A B : ℝ} (hm : 0 < m) (hA : 0 < A)
    (hAB : A < B) : ¬ (∀ k : ℕ, m * B ^ k ≤ R * A ^ k) := bym:ℝR:ℝA:ℝB:ℝhm:0 < mhA:0 < AhAB:A < B⊢ ¬∀ (k : ℕ), m * B ^ k ≤ R * A ^ k
  intro hm:ℝR:ℝA:ℝB:ℝhm:0 < mhA:0 < AhAB:A < Bh:∀ (k : ℕ), m * B ^ k ≤ R * A ^ k⊢ False
  obtain ⟨k, hk⟩ := pow_unbounded_of_one_lt (R / m) ((one_lt_div hA).mpr hAB)m:ℝR:ℝA:ℝB:ℝhm:0 < mhA:0 < AhAB:A < Bh:∀ (k : ℕ), m * B ^ k ≤ R * A ^ kk:ℕhk:R / m < (B / A) ^ k⊢ False
  have hpow : 0 < A ^ k := pow_pos hA km:ℝR:ℝA:ℝB:ℝhm:0 < mhA:0 < AhAB:A < Bh:∀ (k : ℕ), m * B ^ k ≤ R * A ^ kk:ℕhk:R / m < (B / A) ^ khpow:0 < A ^ k⊢ False
  have hbound : (B / A) ^ k ≤ R / m := bym:ℝR:ℝA:ℝB:ℝhm:0 < mhA:0 < AhAB:A < B⊢ ¬∀ (k : ℕ), m * B ^ k ≤ R * A ^ k
    rw [div_pow,m:ℝR:ℝA:ℝB:ℝhm:0 < mhA:0 < AhAB:A < Bh:∀ (k : ℕ), m * B ^ k ≤ R * A ^ kk:ℕhk:R / m < (B / A) ^ khpow:0 < A ^ k⊢ B ^ k / A ^ k ≤ R / m div_le_div_iff₀ hpow hmm:ℝR:ℝA:ℝB:ℝhm:0 < mhA:0 < AhAB:A < Bh:∀ (k : ℕ), m * B ^ k ≤ R * A ^ kk:ℕhk:R / m < (B / A) ^ khpow:0 < A ^ k⊢ B ^ k * m ≤ R * A ^ k]m:ℝR:ℝA:ℝB:ℝhm:0 < mhA:0 < AhAB:A < Bh:∀ (k : ℕ), m * B ^ k ≤ R * A ^ kk:ℕhk:R / m < (B / A) ^ khpow:0 < A ^ k⊢ B ^ k * m ≤ R * A ^ k
    simpa [mul_comm] using h km:ℝR:ℝA:ℝB:ℝhm:0 < mhA:0 < AhAB:A < Bh:∀ (k : ℕ), m * B ^ k ≤ R * A ^ kk:ℕhk:R / m < (B / A) ^ khpow:0 < A ^ khbound:(B / A) ^ k ≤ R / m⊢ False
  exact (not_lt_of_ge hbound) hkAll goals completed! 🐙

end HardyZeta