11.6. HardyZeta.FiniteDifferenceIntegral
def hardyTransform (α : ℝ) : ℝ := ∫ t : ℝ in Ioi 0, hardyWeight t * Real.cosh (α * t)theorem difference_sample_bounds {x h a : ℝ} {k : ℕ}
(hx : |x| + (k + 1 : ℕ) * |h| < a) :
(|x + h| + (k : ℝ) * |h| < a) ∧
(|x - h| + (k : ℝ) * |h| < a) ∧
(|x| + (k : ℝ) * |h| < a) := x:ℝh:ℝa:ℝk:ℕhx:|x| + ↑(k + 1) * |h| < a⊢ |x + h| + ↑k * |h| < a ∧ |x - h| + ↑k * |h| < a ∧ |x| + ↑k * |h| < a
x:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < a⊢ |x + h| + ↑k * |h| < a ∧ |x - h| + ↑k * |h| < a ∧ |x| + ↑k * |h| < a
x:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|⊢ |x + h| + ↑k * |h| < a ∧ |x - h| + ↑k * |h| < a ∧ |x| + ↑k * |h| < a
x:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|hm:|x - h| ≤ |x| + |h|⊢ |x + h| + ↑k * |h| < a ∧ |x - h| + ↑k * |h| < a ∧ |x| + ↑k * |h| < a
x:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|hm:|x - h| ≤ |x| + |h|hn:0 ≤ |h|⊢ |x + h| + ↑k * |h| < a ∧ |x - h| + ↑k * |h| < a ∧ |x| + ↑k * |h| < a
x:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|hm:|x - h| ≤ |x| + |h|hn:0 ≤ |h|⊢ |x + h| + ↑k * |h| < ax:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|hm:|x - h| ≤ |x| + |h|hn:0 ≤ |h|⊢ |x - h| + ↑k * |h| < a ∧ |x| + ↑k * |h| < a
x:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|hm:|x - h| ≤ |x| + |h|hn:0 ≤ |h|⊢ |x + h| + ↑k * |h| < a All goals completed! 🐙
x:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|hm:|x - h| ≤ |x| + |h|hn:0 ≤ |h|⊢ |x - h| + ↑k * |h| < ax:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|hm:|x - h| ≤ |x| + |h|hn:0 ≤ |h|⊢ |x| + ↑k * |h| < a x:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|hm:|x - h| ≤ |x| + |h|hn:0 ≤ |h|⊢ |x - h| + ↑k * |h| < ax:ℝh:ℝa:ℝk:ℕhx:|x| + (↑k + 1) * |h| < ahp:|x + h| ≤ |x| + |h|hm:|x - h| ≤ |x| + |h|hn:0 ≤ |h|⊢ |x| + ↑k * |h| < a All goals completed! 🐙theorem integrableOn_hardyDifference (k : ℕ) (h x : ℝ)
(hx : |x| + (k : ℝ) * |h| < Real.pi / 4) :
IntegrableOn (fun t : ℝ ↦ hardyWeight t * differenceMultiplier h t ^ k *
Real.cosh (x * t)) (Ioi 0) := k:ℕh:ℝx:ℝhx:|x| + ↑k * |h| < Real.pi / 4⊢ IntegrableOn (fun t => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)) (Ioi 0) volume
induction k generalizing x with
h:ℝx:ℝhx:|x| + ↑0 * |h| < Real.pi / 4⊢ IntegrableOn (fun t => hardyWeight t * differenceMultiplier h t ^ 0 * Real.cosh (x * t)) (Ioi 0) volume simpa using integrableOn_hardyWeight_cosh (h:ℝx:ℝhx:|x| + ↑0 * |h| < Real.pi / 4⊢ |x| < Real.pi / 4 All goals completed! 🐙)
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
IntegrableOn (fun t => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)) (Ioi 0) volumex:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4⊢ IntegrableOn (fun t => hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)) (Ioi 0) volume
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
IntegrableOn (fun t => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)) (Ioi 0) volumex:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4⊢ IntegrableOn (fun t => hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)) (Ioi 0) volume
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
IntegrableOn (fun t => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)) (Ioi 0) volumex:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4hi:Integrable (fun t => hardyWeight t * differenceMultiplier h t ^ k * differenceMultiplier h t * Real.cosh (x * t))
(volume.restrict (Ioi 0))⊢ IntegrableOn (fun t => hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)) (Ioi 0) volume
All goals completed! 🐙theorem iterate_hardyTransform_eq_integral (k : ℕ) (h x : ℝ)
(hx : |x| + (k : ℝ) * |h| < Real.pi / 4) :
(modifiedDifference h)^[k] hardyTransform x =
∫ t : ℝ in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t) := k:ℕh:ℝx:ℝhx:|x| + ↑k * |h| < Real.pi / 4⊢ (modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)
induction k generalizing x with
h:ℝx:ℝhx:|x| + ↑0 * |h| < Real.pi / 4⊢ (modifiedDifference h)^[0] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ 0 * Real.cosh (x * t) All goals completed! 🐙
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4⊢ (modifiedDifference h)^[k + 1] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4⊢ (modifiedDifference h)^[k + 1] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4⊢ modifiedDifference h ((modifiedDifference h)^[k] hardyTransform) x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
conv_lhs => h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4| (modifiedDifference h)^[k] hardyTransform (x + h) + (modifiedDifference h)^[k] hardyTransform (x - h) -
2 * Real.cos (h / 2) * (modifiedDifference h)^[k] hardyTransform x
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4⊢ ((∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((x + h) * t)) +
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((x - h) * t)) -
2 * Real.cos (h / 2) * ∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t) =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4he:modifiedDifference h
(fun y => ∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t) ∂volume) x =
∫ (t : ℝ) in Ioi 0,
modifiedDifference h (fun y => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t)) x ∂volume⊢ ((∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((x + h) * t)) +
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((x - h) * t)) -
2 * Real.cos (h / 2) * ∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t) =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4he:modifiedDifference h
(fun y => ∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t) ∂volume) x =
∫ (t : ℝ) in Ioi 0,
modifiedDifference h (fun y => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t)) x ∂volume⊢ ∫ (t : ℝ) in Ioi 0, modifiedDifference h (fun y => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t)) x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4he:modifiedDifference h
(fun y => ∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t) ∂volume) x =
∫ (t : ℝ) in Ioi 0,
modifiedDifference h (fun y => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t)) x ∂volume⊢ EqOn
(fun x_1 => modifiedDifference h (fun y => hardyWeight x_1 * differenceMultiplier h x_1 ^ k * Real.cosh (y * x_1)) x)
(fun x_1 => hardyWeight x_1 * differenceMultiplier h x_1 ^ (k + 1) * Real.cosh (x * x_1)) (Ioi 0)
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4he:modifiedDifference h
(fun y => ∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t) ∂volume) x =
∫ (t : ℝ) in Ioi 0,
modifiedDifference h (fun y => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t)) x ∂volumet:ℝa✝:t ∈ Ioi 0⊢ (fun x_1 => modifiedDifference h (fun y => hardyWeight x_1 * differenceMultiplier h x_1 ^ k * Real.cosh (y * x_1)) x)
t =
(fun x_1 => hardyWeight x_1 * differenceMultiplier h x_1 ^ (k + 1) * Real.cosh (x * x_1)) t
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4he:modifiedDifference h
(fun y => ∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t) ∂volume) x =
∫ (t : ℝ) in Ioi 0,
modifiedDifference h (fun y => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t)) x ∂volumet:ℝa✝:t ∈ Ioi 0⊢ modifiedDifference h (fun y => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t)) x =
hardyWeight t * differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
h:ℝk:ℕih:∀ (x : ℝ),
|x| + ↑k * |h| < Real.pi / 4 →
(modifiedDifference h)^[k] hardyTransform x =
∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4hp:|x + h| + ↑k * |h| < Real.pi / 4hm:|x - h| + ↑k * |h| < Real.pi / 4hc:|x| + ↑k * |h| < Real.pi / 4he:modifiedDifference h
(fun y => ∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t) ∂volume) x =
∫ (t : ℝ) in Ioi 0,
modifiedDifference h (fun y => hardyWeight t * differenceMultiplier h t ^ k * Real.cosh (y * t)) x ∂volumet:ℝa✝:t ∈ Ioi 0⊢ hardyWeight t * differenceMultiplier h t ^ k * (differenceMultiplier h t * Real.cosh (x * t)) =
hardyWeight t * (differenceMultiplier h t ^ k * differenceMultiplier h t) * Real.cosh (x * t)
All goals completed! 🐙theorem iterate_modifiedDifference_congr_strip {f g : ℝ → ℝ} {a : ℝ}
(hfg : ∀ x, |x| < a → f x = g x) (k : ℕ) (h x : ℝ)
(hx : |x| + (k : ℝ) * |h| < a) :
(modifiedDifference h)^[k] f x = (modifiedDifference h)^[k] g x := f:ℝ → ℝg:ℝ → ℝa:ℝhfg:∀ (x : ℝ), |x| < a → f x = g xk:ℕh:ℝx:ℝhx:|x| + ↑k * |h| < a⊢ (modifiedDifference h)^[k] f x = (modifiedDifference h)^[k] g x
induction k generalizing x with
f:ℝ → ℝg:ℝ → ℝa:ℝhfg:∀ (x : ℝ), |x| < a → f x = g xh:ℝx:ℝhx:|x| + ↑0 * |h| < a⊢ (modifiedDifference h)^[0] f x = (modifiedDifference h)^[0] g x exact hfg x (f:ℝ → ℝg:ℝ → ℝa:ℝhfg:∀ (x : ℝ), |x| < a → f x = g xh:ℝx:ℝhx:|x| + ↑0 * |h| < a⊢ |x| < a All goals completed! 🐙)
f:ℝ → ℝg:ℝ → ℝa:ℝhfg:∀ (x : ℝ), |x| < a → f x = g xh:ℝk:ℕih:∀ (x : ℝ), |x| + ↑k * |h| < a → (modifiedDifference h)^[k] f x = (modifiedDifference h)^[k] g xx:ℝhx:|x| + ↑(k + 1) * |h| < a⊢ (modifiedDifference h)^[k + 1] f x = (modifiedDifference h)^[k + 1] g x
f:ℝ → ℝg:ℝ → ℝa:ℝhfg:∀ (x : ℝ), |x| < a → f x = g xh:ℝk:ℕih:∀ (x : ℝ), |x| + ↑k * |h| < a → (modifiedDifference h)^[k] f x = (modifiedDifference h)^[k] g xx:ℝhx:|x| + ↑(k + 1) * |h| < ahp:|x + h| + ↑k * |h| < ahm:|x - h| + ↑k * |h| < ahc:|x| + ↑k * |h| < a⊢ (modifiedDifference h)^[k + 1] f x = (modifiedDifference h)^[k + 1] g x
f:ℝ → ℝg:ℝ → ℝa:ℝhfg:∀ (x : ℝ), |x| < a → f x = g xh:ℝk:ℕih:∀ (x : ℝ), |x| + ↑k * |h| < a → (modifiedDifference h)^[k] f x = (modifiedDifference h)^[k] g xx:ℝhx:|x| + ↑(k + 1) * |h| < ahp:|x + h| + ↑k * |h| < ahm:|x - h| + ↑k * |h| < ahc:|x| + ↑k * |h| < a⊢ modifiedDifference h ((modifiedDifference h)^[k] f) x = modifiedDifference h ((modifiedDifference h)^[k] g) x
conv_lhs => f:ℝ → ℝg:ℝ → ℝa:ℝhfg:∀ (x : ℝ), |x| < a → f x = g xh:ℝk:ℕih:∀ (x : ℝ), |x| + ↑k * |h| < a → (modifiedDifference h)^[k] f x = (modifiedDifference h)^[k] g xx:ℝhx:|x| + ↑(k + 1) * |h| < ahp:|x + h| + ↑k * |h| < ahm:|x - h| + ↑k * |h| < ahc:|x| + ↑k * |h| < a| (modifiedDifference h)^[k] f (x + h) + (modifiedDifference h)^[k] f (x - h) -
2 * Real.cos (h / 2) * (modifiedDifference h)^[k] f x
conv_rhs => f:ℝ → ℝg:ℝ → ℝa:ℝhfg:∀ (x : ℝ), |x| < a → f x = g xh:ℝk:ℕih:∀ (x : ℝ), |x| + ↑k * |h| < a → (modifiedDifference h)^[k] f x = (modifiedDifference h)^[k] g xx:ℝhx:|x| + ↑(k + 1) * |h| < ahp:|x + h| + ↑k * |h| < ahm:|x - h| + ↑k * |h| < ahc:|x| + ↑k * |h| < a| (modifiedDifference h)^[k] g (x + h) + (modifiedDifference h)^[k] g (x - h) -
2 * Real.cos (h / 2) * (modifiedDifference h)^[k] g x
All goals completed! 🐙