HardyZeta.HardyDifferenceLimit

            
              11.8. HardyZeta.HardyDifferenceLimit🔗
            theorem iterate_modifiedDifference_sub (h : ℝ) (f g : ℝ → ℝ) (k : ℕ) :
    (modifiedDifference h)^[k] (fun x ↦ f x - g x) =
      fun x ↦ (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x := byh:ℝf:ℝ → ℝg:ℝ → ℝk:ℕ⊢ ((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x
  induction k with
  | zero =>zeroh:ℝf:ℝ → ℝg:ℝ → ℝ⊢ ((modifiedDifference h)^[0] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[0] f x - (modifiedDifference h)^[0] g x rflAll goals completed! 🐙
  | succ k ih =>succh:ℝf:ℝ → ℝg:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x⊢ ((modifiedDifference h)^[k + 1] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k + 1] f x - (modifiedDifference h)^[k + 1] g x
    rw [Function.iterate_succ_apply',succh:ℝf:ℝ → ℝg:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x⊢ modifiedDifference h ((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k + 1] f x - (modifiedDifference h)^[k + 1] g x ihsucch:ℝf:ℝ → ℝg:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x⊢ (modifiedDifference h fun x => (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x) = fun x =>
  (modifiedDifference h)^[k + 1] f x - (modifiedDifference h)^[k + 1] g x]succh:ℝf:ℝ → ℝg:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x⊢ (modifiedDifference h fun x => (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x) = fun x =>
  (modifiedDifference h)^[k + 1] f x - (modifiedDifference h)^[k + 1] g x
    funext xsucch:ℝf:ℝ → ℝg:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g xx:ℝ⊢ modifiedDifference h (fun x => (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x) x =
  (modifiedDifference h)^[k + 1] f x - (modifiedDifference h)^[k + 1] g x
    rw [Function.iterate_succ_apply',succh:ℝf:ℝ → ℝg:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g xx:ℝ⊢ modifiedDifference h (fun x => (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x) x =
  modifiedDifference h ((modifiedDifference h)^[k] f) x - (modifiedDifference h)^[k + 1] g x Function.iterate_succ_apply'succh:ℝf:ℝ → ℝg:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g xx:ℝ⊢ modifiedDifference h (fun x => (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x) x =
  modifiedDifference h ((modifiedDifference h)^[k] f) x - modifiedDifference h ((modifiedDifference h)^[k] g) x]succh:ℝf:ℝ → ℝg:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g xx:ℝ⊢ modifiedDifference h (fun x => (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x) x =
  modifiedDifference h ((modifiedDifference h)^[k] f) x - modifiedDifference h ((modifiedDifference h)^[k] g) x
    simp only [modifiedDifference]succh:ℝf:ℝ → ℝg:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
  (modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g xx:ℝ⊢ (modifiedDifference h)^[k] f (x + h) - (modifiedDifference h)^[k] g (x + h) +
      ((modifiedDifference h)^[k] f (x - h) - (modifiedDifference h)^[k] g (x - h)) -
    2 * Real.cos (h / 2) * ((modifiedDifference h)^[k] f x - (modifiedDifference h)^[k] g x) =
  (modifiedDifference h)^[k] f (x + h) + (modifiedDifference h)^[k] f (x - h) -
      2 * Real.cos (h / 2) * (modifiedDifference h)^[k] f x -
    ((modifiedDifference h)^[k] g (x + h) + (modifiedDifference h)^[k] g (x - h) -
      2 * Real.cos (h / 2) * (modifiedDifference h)^[k] g x)
    ringAll goals completed! 🐙theorem iterate_modifiedDifference_const_mul (h c : ℝ) (f : ℝ → ℝ) (k : ℕ) :
    (modifiedDifference h)^[k] (fun x ↦ c * f x) =
      fun x ↦ c * (modifiedDifference h)^[k] f x := byh:ℝc:ℝf:ℝ → ℝk:ℕ⊢ ((modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k] f x
  induction k with
  | zero =>zeroh:ℝc:ℝf:ℝ → ℝ⊢ ((modifiedDifference h)^[0] fun x => c * f x) = fun x => c * (modifiedDifference h)^[0] f x rflAll goals completed! 🐙
  | succ k ih =>succh:ℝc:ℝf:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k] f x⊢ ((modifiedDifference h)^[k + 1] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k + 1] f x
    rw [Function.iterate_succ_apply',succh:ℝc:ℝf:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k] f x⊢ modifiedDifference h ((modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k + 1] f x ih,succh:ℝc:ℝf:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k] f x⊢ (modifiedDifference h fun x => c * (modifiedDifference h)^[k] f x) = fun x => c * (modifiedDifference h)^[k + 1] f x modifiedDifference_const_mulsucch:ℝc:ℝf:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k] f x⊢ (fun x => c * modifiedDifference h ((modifiedDifference h)^[k] f) x) = fun x => c * (modifiedDifference h)^[k + 1] f x]succh:ℝc:ℝf:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k] f x⊢ (fun x => c * modifiedDifference h ((modifiedDifference h)^[k] f) x) = fun x => c * (modifiedDifference h)^[k + 1] f x
    funext xsucch:ℝc:ℝf:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k] f xx:ℝ⊢ c * modifiedDifference h ((modifiedDifference h)^[k] f) x = c * (modifiedDifference h)^[k + 1] f x
    rw [Function.iterate_succ_apply'succh:ℝc:ℝf:ℝ → ℝk:ℕih:((modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (modifiedDifference h)^[k] f xx:ℝ⊢ c * modifiedDifference h ((modifiedDifference h)^[k] f) x = c * modifiedDifference h ((modifiedDifference h)^[k] f) x]All goals completed! 🐙theorem iterate_modifiedDifference_cos_succ (h : ℝ) (k : ℕ) :
    (modifiedDifference h)^[k + 1] (fun x ↦ Real.cos (x / 2)) = fun _ ↦ 0 := byh:ℝk:ℕ⊢ ((modifiedDifference h)^[k + 1] fun x => Real.cos (x / 2)) = fun x => 0
  induction k with
  | zero =>zeroh:ℝ⊢ ((modifiedDifference h)^[0 + 1] fun x => Real.cos (x / 2)) = fun x => 0 funext xzeroh:ℝx:ℝ⊢ (modifiedDifference h)^[0 + 1] (fun x => Real.cos (x / 2)) x = 0; exact modifiedDifference_cos h xAll goals completed! 🐙
  | succ k ih =>succh:ℝk:ℕih:((modifiedDifference h)^[k + 1] fun x => Real.cos (x / 2)) = fun x => 0⊢ ((modifiedDifference h)^[k + 1 + 1] fun x => Real.cos (x / 2)) = fun x => 0
    rw [Function.iterate_succ_apply',succh:ℝk:ℕih:((modifiedDifference h)^[k + 1] fun x => Real.cos (x / 2)) = fun x => 0⊢ modifiedDifference h ((modifiedDifference h)^[k + 1] fun x => Real.cos (x / 2)) = fun x => 0 ihsucch:ℝk:ℕih:((modifiedDifference h)^[k + 1] fun x => Real.cos (x / 2)) = fun x => 0⊢ (modifiedDifference h fun x => 0) = fun x => 0]succh:ℝk:ℕih:((modifiedDifference h)^[k + 1] fun x => Real.cos (x / 2)) = fun x => 0⊢ (modifiedDifference h fun x => 0) = fun x => 0
    funext xsucch:ℝk:ℕih:((modifiedDifference h)^[k + 1] fun x => Real.cos (x / 2)) = fun x => 0x:ℝ⊢ modifiedDifference h (fun x => 0) x = 0
    simp [modifiedDifference]All goals completed! 🐙theorem hardyTransform_eq (x : ℝ) (hx : |x| < Real.pi / 4) :
    hardyTransform x = Real.pi * Real.cos (x / 2) -
      Real.pi * (thetaBoundaryRemainder x).re := byx:ℝhx:|x| < Real.pi / 4⊢ hardyTransform x = Real.pi * Real.cos (x / 2) - Real.pi * (thetaBoundaryRemainder x).re
  have h := congrArg Complex.re (integral_hardyWeight_cosh hx)x:ℝhx:|x| < Real.pi / 4h:(↑(∫ (t : ℝ) in Ioi 0, hardyWeight t * Real.cosh (x * t))).re =
  (↑Real.pi * ↑(Real.cos (x / 2)) - ↑Real.pi * thetaBoundaryRemainder x).re⊢ hardyTransform x = Real.pi * Real.cos (x / 2) - Real.pi * (thetaBoundaryRemainder x).re
  simpa only [hardyTransform, Complex.ofReal_re, Complex.sub_re, Complex.mul_re,
    Complex.ofReal_im, mul_zero, zero_mul, sub_zero] using hAll goals completed! 🐙theorem iterate_hardyTransform_eq_theta (k : ℕ) (h x : ℝ)
    (hx : |x| + (k + 1 : ℕ) * |h| < Real.pi / 4) :
    (modifiedDifference h)^[k + 1] hardyTransform x =
      -Real.pi * (modifiedDifference h)^[k + 1] (fun α ↦ (thetaBoundaryRemainder α).re) x := byk:ℕh:ℝx:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4⊢ (modifiedDifference h)^[k + 1] hardyTransform x =
  -Real.pi * (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) x
  rw [iterate_modifiedDifference_congr_strip hardyTransform_eq (k + 1) h x hx,k:ℕh:ℝx:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4⊢ (modifiedDifference h)^[k + 1] (fun x => Real.pi * Real.cos (x / 2) - Real.pi * (thetaBoundaryRemainder x).re) x =
  -Real.pi * (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) x
    iterate_modifiedDifference_sub,k:ℕh:ℝx:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4⊢ (fun x =>
      (modifiedDifference h)^[k + 1] (fun x => Real.pi * Real.cos (x / 2)) x -
        (modifiedDifference h)^[k + 1] (fun x => Real.pi * (thetaBoundaryRemainder x).re) x)
    x =
  -Real.pi * (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) x iterate_modifiedDifference_const_mul,k:ℕh:ℝx:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4⊢ (fun x =>
      (fun x => Real.pi * (modifiedDifference h)^[k + 1] (fun x => Real.cos (x / 2)) x) x -
        (modifiedDifference h)^[k + 1] (fun x => Real.pi * (thetaBoundaryRemainder x).re) x)
    x =
  -Real.pi * (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) x
    iterate_modifiedDifference_const_mul,k:ℕh:ℝx:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4⊢ (fun x =>
      (fun x => Real.pi * (modifiedDifference h)^[k + 1] (fun x => Real.cos (x / 2)) x) x -
        (fun x => Real.pi * (modifiedDifference h)^[k + 1] (fun x => (thetaBoundaryRemainder x).re) x) x)
    x =
  -Real.pi * (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) x iterate_modifiedDifference_cos_succk:ℕh:ℝx:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4⊢ (fun x =>
      (fun x => Real.pi * (fun x => 0) x) x -
        (fun x => Real.pi * (modifiedDifference h)^[k + 1] (fun x => (thetaBoundaryRemainder x).re) x) x)
    x =
  -Real.pi * (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) x]k:ℕh:ℝx:ℝhx:|x| + ↑(k + 1) * |h| < Real.pi / 4⊢ (fun x =>
      (fun x => Real.pi * (fun x => 0) x) x -
        (fun x => Real.pi * (modifiedDifference h)^[k + 1] (fun x => (thetaBoundaryRemainder x).re) x) x)
    x =
  -Real.pi * (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) x
  simpAll goals completed! 🐙theorem eventually_difference_center_inside {a : ℝ} (ha : 0 < a) (k : ℕ) :
    ∀ᶠ h : ℝ in 𝓝[>] 0,
      |a - ((k : ℝ) + 1) * h| + (k : ℝ) * |h| < a := bya:ℝha:0 < ak:ℕ⊢ ∀ᶠ (h : ℝ) in 𝓝[>] 0, |a - (↑k + 1) * h| + ↑k * |h| < a
  have hc : 0 < (k : ℝ) + 1 := by positivitya:ℝha:0 < ak:ℕhc:0 < ↑k + 1⊢ ∀ᶠ (h : ℝ) in 𝓝[>] 0, |a - (↑k + 1) * h| + ↑k * |h| < a
  have he : ∀ᶠ h : ℝ in 𝓝[>] 0, h < a / ((k : ℝ) + 1) :=
    nhdsWithin_le_nhds (gt_mem_nhds (div_pos ha hc))a:ℝha:0 < ak:ℕhc:0 < ↑k + 1he:∀ᶠ (h : ℝ) in 𝓝[>] 0, h < a / (↑k + 1)⊢ ∀ᶠ (h : ℝ) in 𝓝[>] 0, |a - (↑k + 1) * h| + ↑k * |h| < a
  filter_upwards [he, self_mem_nhdsWithin] with h hha:ℝha:0 < ak:ℕhc:0 < ↑k + 1he:∀ᶠ (h : ℝ) in 𝓝[>] 0, h < a / (↑k + 1)h:ℝhh:h < a / (↑k + 1)⊢ h ∈ Ioi 0 → |a - (↑k + 1) * h| + ↑k * |h| < a hpa:ℝha:0 < ak:ℕhc:0 < ↑k + 1he:∀ᶠ (h : ℝ) in 𝓝[>] 0, h < a / (↑k + 1)h:ℝhh:h < a / (↑k + 1)hp:h ∈ Ioi 0⊢ |a - (↑k + 1) * h| + ↑k * |h| < a
  have hp0 : 0 < h := hpa:ℝha:0 < ak:ℕhc:0 < ↑k + 1he:∀ᶠ (h : ℝ) in 𝓝[>] 0, h < a / (↑k + 1)h:ℝhh:h < a / (↑k + 1)hp:h ∈ Ioi 0hp0:0 < h⊢ |a - (↑k + 1) * h| + ↑k * |h| < a
  have hx : 0 ≤ a - ((k : ℝ) + 1) * h := bya:ℝha:0 < ak:ℕ⊢ ∀ᶠ (h : ℝ) in 𝓝[>] 0, |a - (↑k + 1) * h| + ↑k * |h| < a
    have := (lt_div_iff₀ hc).mp hha:ℝha:0 < ak:ℕhc:0 < ↑k + 1he:∀ᶠ (h : ℝ) in 𝓝[>] 0, h < a / (↑k + 1)h:ℝhh:h < a / (↑k + 1)hp:h ∈ Ioi 0hp0:0 < hthis:h * (↑k + 1) < a⊢ 0 ≤ a - (↑k + 1) * h
    nlinaritha:ℝha:0 < ak:ℕhc:0 < ↑k + 1he:∀ᶠ (h : ℝ) in 𝓝[>] 0, h < a / (↑k + 1)h:ℝhh:h < a / (↑k + 1)hp:h ∈ Ioi 0hp0:0 < hhx:0 ≤ a - (↑k + 1) * h⊢ |a - (↑k + 1) * h| + ↑k * |h| < a
  rw [abs_of_nonneg hx,a:ℝha:0 < ak:ℕhc:0 < ↑k + 1he:∀ᶠ (h : ℝ) in 𝓝[>] 0, h < a / (↑k + 1)h:ℝhh:h < a / (↑k + 1)hp:h ∈ Ioi 0hp0:0 < hhx:0 ≤ a - (↑k + 1) * h⊢ a - (↑k + 1) * h + ↑k * |h| < a abs_of_pos hp0a:ℝha:0 < ak:ℕhc:0 < ↑k + 1he:∀ᶠ (h : ℝ) in 𝓝[>] 0, h < a / (↑k + 1)h:ℝhh:h < a / (↑k + 1)hp:h ∈ Ioi 0hp0:0 < hhx:0 ≤ a - (↑k + 1) * h⊢ a - (↑k + 1) * h + ↑k * h < a]a:ℝha:0 < ak:ℕhc:0 < ↑k + 1he:∀ᶠ (h : ℝ) in 𝓝[>] 0, h < a / (↑k + 1)h:ℝhh:h < a / (↑k + 1)hp:h ∈ Ioi 0hp0:0 < hhx:0 ≤ a - (↑k + 1) * h⊢ a - (↑k + 1) * h + ↑k * h < a
  nlinarithAll goals completed! 🐙theorem tendsto_scaled_hardy_difference (k : ℕ) :
    Tendsto (fun h : ℝ ↦ h⁻¹ ^ (2 * (k + 1)) *
      (modifiedDifference h)^[k + 1] hardyTransform
        (Real.pi / 4 - ((k + 1 : ℕ) + 1 : ℝ) * h)) (𝓝[>] 0) (𝓝 0) := byk:ℕ⊢ Tendsto
  (fun h => h⁻¹ ^ (2 * (k + 1)) * (modifiedDifference h)^[k + 1] hardyTransform (Real.pi / 4 - (↑(k + 1) + 1) * h))
  (𝓝[>] 0) (𝓝 0)
  have hl := (tendsto_scaled_theta_difference (k + 1)).const_mul (-Real.pi)k:ℕhl:Tendsto
  (fun x =>
    -Real.pi *
      (x⁻¹ ^ (2 * (k + 1)) *
        (modifiedDifference x)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * x)))
  (𝓝[>] 0) (𝓝 (-Real.pi * 0))⊢ Tendsto
  (fun h => h⁻¹ ^ (2 * (k + 1)) * (modifiedDifference h)^[k + 1] hardyTransform (Real.pi / 4 - (↑(k + 1) + 1) * h))
  (𝓝[>] 0) (𝓝 0)
  simp only [mul_zero] at hlk:ℕhl:Tendsto
  (fun x =>
    -Real.pi *
      (x⁻¹ ^ (2 * (k + 1)) *
        (modifiedDifference x)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * x)))
  (𝓝[>] 0) (𝓝 0)⊢ Tendsto
  (fun h => h⁻¹ ^ (2 * (k + 1)) * (modifiedDifference h)^[k + 1] hardyTransform (Real.pi / 4 - (↑(k + 1) + 1) * h))
  (𝓝[>] 0) (𝓝 0)
  apply hl.congr'k:ℕhl:Tendsto
  (fun x =>
    -Real.pi *
      (x⁻¹ ^ (2 * (k + 1)) *
        (modifiedDifference x)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * x)))
  (𝓝[>] 0) (𝓝 0)⊢ (fun x =>
    -Real.pi *
      (x⁻¹ ^ (2 * (k + 1)) *
        (modifiedDifference x)^[k + 1] (fun α => (thetaBoundaryRemainder α).re)
          (Real.pi / 4 - (↑(k + 1) + 1) * x))) =ᶠ[𝓝[>] 0]
  fun h => h⁻¹ ^ (2 * (k + 1)) * (modifiedDifference h)^[k + 1] hardyTransform (Real.pi / 4 - (↑(k + 1) + 1) * h)
  filter_upwards [eventually_difference_center_inside (byk:ℕhl:Tendsto
  (fun x =>
    -Real.pi *
      (x⁻¹ ^ (2 * (k + 1)) *
        (modifiedDifference x)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * x)))
  (𝓝[>] 0) (𝓝 0)⊢ 0 < Real.pi / 4 positivityAll goals completed! 🐙 : (0 : ℝ) < Real.pi / 4)
    (k + 1)] with h hhk:ℕhl:Tendsto
  (fun x =>
    -Real.pi *
      (x⁻¹ ^ (2 * (k + 1)) *
        (modifiedDifference x)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * x)))
  (𝓝[>] 0) (𝓝 0)h:ℝhh:|Real.pi / 4 - (↑(k + 1) + 1) * h| + ↑(k + 1) * |h| < Real.pi / 4⊢ -Real.pi *
    (h⁻¹ ^ (2 * (k + 1)) *
      (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * h)) =
  h⁻¹ ^ (2 * (k + 1)) * (modifiedDifference h)^[k + 1] hardyTransform (Real.pi / 4 - (↑(k + 1) + 1) * h)
  rw [iterate_hardyTransform_eq_theta k h _ hhk:ℕhl:Tendsto
  (fun x =>
    -Real.pi *
      (x⁻¹ ^ (2 * (k + 1)) *
        (modifiedDifference x)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * x)))
  (𝓝[>] 0) (𝓝 0)h:ℝhh:|Real.pi / 4 - (↑(k + 1) + 1) * h| + ↑(k + 1) * |h| < Real.pi / 4⊢ -Real.pi *
    (h⁻¹ ^ (2 * (k + 1)) *
      (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * h)) =
  h⁻¹ ^ (2 * (k + 1)) *
    (-Real.pi *
      (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * h))]k:ℕhl:Tendsto
  (fun x =>
    -Real.pi *
      (x⁻¹ ^ (2 * (k + 1)) *
        (modifiedDifference x)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * x)))
  (𝓝[>] 0) (𝓝 0)h:ℝhh:|Real.pi / 4 - (↑(k + 1) + 1) * h| + ↑(k + 1) * |h| < Real.pi / 4⊢ -Real.pi *
    (h⁻¹ ^ (2 * (k + 1)) *
      (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * h)) =
  h⁻¹ ^ (2 * (k + 1)) *
    (-Real.pi *
      (modifiedDifference h)^[k + 1] (fun α => (thetaBoundaryRemainder α).re) (Real.pi / 4 - (↑(k + 1) + 1) * h))
  ringAll goals completed! 🐙

/-- The nonnegative kernel used to compare a compact interval with the eventual-sign tail. -/def normalizedHardyKernel (k : ℕ) (h t : ℝ) : ℝ :=
  (differenceMultiplier h t / h ^ 2) ^ k *
    Real.cosh ((Real.pi / 4 - ((k : ℝ) + 1) * h) * t)theorem normalizedHardyKernel_nonneg (k : ℕ) (h t : ℝ) :
    0 ≤ normalizedHardyKernel k h t := byk:ℕh:ℝt:ℝ⊢ 0 ≤ normalizedHardyKernel k h t
  unfold normalizedHardyKernelk:ℕh:ℝt:ℝ⊢ 0 ≤ (differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t)
  exact mul_nonneg (pow_nonneg (div_nonneg (differenceMultiplier_nonneg h t) (sq_nonneg h)) k)
    (Real.cosh_pos _).leAll goals completed! 🐙theorem normalizedHardyIntegral_eq (k : ℕ) (h : ℝ)
    (hh : |Real.pi / 4 - ((k : ℝ) + 1) * h| + (k : ℝ) * |h| < Real.pi / 4) :
    (∫ t : ℝ in Ioi 0, hardyWeight t * normalizedHardyKernel k h t) =
      h⁻¹ ^ (2 * k) * (modifiedDifference h)^[k] hardyTransform
        (Real.pi / 4 - ((k : ℝ) + 1) * h) := byk:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4⊢ ∫ (t : ℝ) in Ioi 0, hardyWeight t * normalizedHardyKernel k h t =
  h⁻¹ ^ (2 * k) * (modifiedDifference h)^[k] hardyTransform (Real.pi / 4 - (↑k + 1) * h)
  rw [iterate_hardyTransform_eq_integral k h _ hh,k:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4⊢ ∫ (t : ℝ) in Ioi 0, hardyWeight t * normalizedHardyKernel k h t =
  h⁻¹ ^ (2 * k) *
    ∫ (t : ℝ) in Ioi 0, hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t) ← integral_const_mulk:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4⊢ ∫ (t : ℝ) in Ioi 0, hardyWeight t * normalizedHardyKernel k h t =
  ∫ (a : ℝ) in Ioi 0,
    h⁻¹ ^ (2 * k) * (hardyWeight a * differenceMultiplier h a ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * a))]k:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4⊢ ∫ (t : ℝ) in Ioi 0, hardyWeight t * normalizedHardyKernel k h t =
  ∫ (a : ℝ) in Ioi 0,
    h⁻¹ ^ (2 * k) * (hardyWeight a * differenceMultiplier h a ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * a))
  apply setIntegral_congr_fun measurableSet_Ioik:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4⊢ EqOn (fun x => hardyWeight x * normalizedHardyKernel k h x)
  (fun x =>
    h⁻¹ ^ (2 * k) * (hardyWeight x * differenceMultiplier h x ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * x)))
  (Ioi 0)
  intro t _k:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4t:ℝa✝:t ∈ Ioi 0⊢ (fun x => hardyWeight x * normalizedHardyKernel k h x) t =
  (fun x =>
      h⁻¹ ^ (2 * k) * (hardyWeight x * differenceMultiplier h x ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * x)))
    t
  dsimp [normalizedHardyKernel]k:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4t:ℝa✝:t ∈ Ioi 0⊢ hardyWeight t * ((differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t)) =
  h⁻¹ ^ (2 * k) * (hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t))
  simp only [div_eq_mul_inv, mul_pow, ← pow_mul, ← inv_pow]k:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4t:ℝa✝:t ∈ Ioi 0⊢ hardyWeight t * (differenceMultiplier h t ^ k * h⁻¹ ^ (2 * k) * Real.cosh ((Real.pi * 4⁻¹ - (↑k + 1) * h) * t)) =
  h⁻¹ ^ (2 * k) * (hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((Real.pi * 4⁻¹ - (↑k + 1) * h) * t))
  ringAll goals completed! 🐙theorem tendsto_normalizedHardyIntegral (k : ℕ) :
    Tendsto (fun h : ℝ ↦ ∫ t : ℝ in Ioi 0,
      hardyWeight t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0) := byk:ℕ⊢ Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, hardyWeight t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0)
  apply (tendsto_scaled_hardy_difference k).congr'k:ℕ⊢ (fun h =>
    h⁻¹ ^ (2 * (k + 1)) * (modifiedDifference h)^[k + 1] hardyTransform (Real.pi / 4 - (↑(k + 1) + 1) * h)) =ᶠ[𝓝[>] 0]
  fun h => ∫ (t : ℝ) in Ioi 0, hardyWeight t * normalizedHardyKernel (k + 1) h t
  filter_upwards [eventually_difference_center_inside (byk:ℕ⊢ 0 < Real.pi / 4 positivityAll goals completed! 🐙 : (0 : ℝ) < Real.pi / 4)
    (k + 1)] with h hhk:ℕh:ℝhh:|Real.pi / 4 - (↑(k + 1) + 1) * h| + ↑(k + 1) * |h| < Real.pi / 4⊢ h⁻¹ ^ (2 * (k + 1)) * (modifiedDifference h)^[k + 1] hardyTransform (Real.pi / 4 - (↑(k + 1) + 1) * h) =
  ∫ (t : ℝ) in Ioi 0, hardyWeight t * normalizedHardyKernel (k + 1) h t
  exact (normalizedHardyIntegral_eq (k + 1) h hh).symmAll goals completed! 🐙theorem integrableOn_normalizedHardyKernel (k : ℕ) (h : ℝ)
    (hh : |Real.pi / 4 - ((k : ℝ) + 1) * h| + (k : ℝ) * |h| < Real.pi / 4) :
    IntegrableOn (fun t ↦ hardyWeight t * normalizedHardyKernel k h t) (Ioi 0) := byk:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4⊢ IntegrableOn (fun t => hardyWeight t * normalizedHardyKernel k h t) (Ioi 0) volume
  have hi := (integrableOn_hardyDifference k h _ hh).const_mul (h⁻¹ ^ (2 * k))k:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4hi:Integrable
  (fun x =>
    h⁻¹ ^ (2 * k) * (hardyWeight x * differenceMultiplier h x ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * x)))
  (volume.restrict (Ioi 0))⊢ IntegrableOn (fun t => hardyWeight t * normalizedHardyKernel k h t) (Ioi 0) volume
  apply hi.congrk:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4hi:Integrable
  (fun x =>
    h⁻¹ ^ (2 * k) * (hardyWeight x * differenceMultiplier h x ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * x)))
  (volume.restrict (Ioi 0))⊢ (fun x =>
    h⁻¹ ^ (2 * k) *
      (hardyWeight x * differenceMultiplier h x ^ k *
        Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * x))) =ᵐ[volume.restrict (Ioi 0)]
  fun t => hardyWeight t * normalizedHardyKernel k h t
  filter_upwards [] with tk:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4hi:Integrable
  (fun x =>
    h⁻¹ ^ (2 * k) * (hardyWeight x * differenceMultiplier h x ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * x)))
  (volume.restrict (Ioi 0))t:ℝ⊢ h⁻¹ ^ (2 * k) * (hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t)) =
  hardyWeight t * normalizedHardyKernel k h t
  dsimp [normalizedHardyKernel]k:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4hi:Integrable
  (fun x =>
    h⁻¹ ^ (2 * k) * (hardyWeight x * differenceMultiplier h x ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * x)))
  (volume.restrict (Ioi 0))t:ℝ⊢ h⁻¹ ^ (2 * k) * (hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t)) =
  hardyWeight t * ((differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t))
  simp only [div_eq_mul_inv, mul_pow, ← pow_mul, ← inv_pow]k:ℕh:ℝhh:|Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4hi:Integrable
  (fun x =>
    h⁻¹ ^ (2 * k) * (hardyWeight x * differenceMultiplier h x ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * x)))
  (volume.restrict (Ioi 0))t:ℝ⊢ h⁻¹ ^ (2 * k) * (hardyWeight t * differenceMultiplier h t ^ k * Real.cosh ((Real.pi * 4⁻¹ - (↑k + 1) * h) * t)) =
  hardyWeight t * (differenceMultiplier h t ^ k * h⁻¹ ^ (2 * k) * Real.cosh ((Real.pi * 4⁻¹ - (↑k + 1) * h) * t))
  ringAll goals completed! 🐙