HardyZeta.TailComparison

            
              11.13. HardyZeta.TailComparison🔗
            theorem compact_tail_le_total_add_initial {q : ℝ → ℝ} (hq : Continuous q)
    (hi : IntegrableOn q (Ioi 0)) {T : ℝ} (hT : 0 < T)
    (hpos : ∀ t > T, 0 ≤ q t) :
    (∫ t in Icc (2 * T) (2 * T + 1), q t) ≤
      (∫ t in Ioi 0, q t) + ∫ t in Icc 0 T, |q t| := byq:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q t⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|
  have hit : IntegrableOn q (Ioi T) := hi.mono_set (Ioi_subset_Ioi hT.le)q:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volume⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|
  have hp : 0 ≤ᵐ[volume.restrict (Ioi T)] q := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t htq:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumet:ℝht:t ∈ Ioi T⊢ 0 t ≤ q t
    exact hpos t htq:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] q⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|
  have hsub : Icc (2 * T) (2 * T + 1) ⊆ Ioi T := by
    intro t htq:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qt:ℝht:t ∈ Icc (2 * T) (2 * T + 1)⊢ t ∈ Ioi T
    simp only [mem_Icc, mem_Ioi] at *q:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qt:ℝht:2 * T ≤ t ∧ t ≤ 2 * T + 1⊢ T < t
    linarith [ht.1]q:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qhsub:Icc (2 * T) (2 * T + 1) ⊆ Ioi T⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|
  have htail := setIntegral_mono_set (s := Icc (2 * T) (2 * T + 1)) hit hp (ae_of_all volume hsub)q:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qhsub:Icc (2 * T) (2 * T + 1) ⊆ Ioi Thtail:∫ (x : ℝ) in Icc (2 * T) (2 * T + 1), q x ≤ ∫ (x : ℝ) in Ioi T, q x⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|
  have hsplit := intervalIntegral.integral_Ioi_sub_Ioi hi hT.leq:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qhsub:Icc (2 * T) (2 * T + 1) ⊆ Ioi Thtail:∫ (x : ℝ) in Icc (2 * T) (2 * T + 1), q x ≤ ∫ (x : ℝ) in Ioi T, q xhsplit:∫ (x : ℝ) in Ioi 0, q x ∂volume - ∫ (x : ℝ) in Ioi T, q x ∂volume = ∫ (x : ℝ) in 0..T, q x⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|
  rw [intervalIntegral.integral_of_le hT.le,q:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qhsub:Icc (2 * T) (2 * T + 1) ⊆ Ioi Thtail:∫ (x : ℝ) in Icc (2 * T) (2 * T + 1), q x ≤ ∫ (x : ℝ) in Ioi T, q xhsplit:∫ (x : ℝ) in Ioi 0, q x ∂volume - ∫ (x : ℝ) in Ioi T, q x ∂volume = ∫ (x : ℝ) in Ioc 0 T, q x ∂volume⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t| ← integral_Icc_eq_integral_Iocq:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qhsub:Icc (2 * T) (2 * T + 1) ⊆ Ioi Thtail:∫ (x : ℝ) in Icc (2 * T) (2 * T + 1), q x ≤ ∫ (x : ℝ) in Ioi T, q xhsplit:∫ (x : ℝ) in Ioi 0, q x ∂volume - ∫ (x : ℝ) in Ioi T, q x ∂volume = ∫ (t : ℝ) in Icc 0 T, q t ∂volume⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|] at hsplitq:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qhsub:Icc (2 * T) (2 * T + 1) ⊆ Ioi Thtail:∫ (x : ℝ) in Icc (2 * T) (2 * T + 1), q x ≤ ∫ (x : ℝ) in Ioi T, q xhsplit:∫ (x : ℝ) in Ioi 0, q x ∂volume - ∫ (x : ℝ) in Ioi T, q x ∂volume = ∫ (t : ℝ) in Icc 0 T, q t ∂volume⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|
  have hhead := setIntegral_mono_on (μ := volume) hq.neg.integrableOn_Icc hq.abs.integrableOn_Icc
    measurableSet_Icc (fun t (_ : t ∈ Icc 0 T) ↦ neg_le_abs (q t))q:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qhsub:Icc (2 * T) (2 * T + 1) ⊆ Ioi Thtail:∫ (x : ℝ) in Icc (2 * T) (2 * T + 1), q x ≤ ∫ (x : ℝ) in Ioi T, q xhsplit:∫ (x : ℝ) in Ioi 0, q x ∂volume - ∫ (x : ℝ) in Ioi T, q x ∂volume = ∫ (t : ℝ) in Icc 0 T, q t ∂volumehhead:∫ (x : ℝ) in Icc 0 T, (-q) x ≤ ∫ (x : ℝ) in Icc 0 T, |q x|⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|
  simp only [Pi.neg_apply, integral_neg] at hheadq:ℝ → ℝhq:Continuous qhi:IntegrableOn q (Ioi 0) volumeT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ q thit:IntegrableOn q (Ioi T) volumehp:0 ≤ᵐ[volume.restrict (Ioi T)] qhsub:Icc (2 * T) (2 * T + 1) ⊆ Ioi Thtail:∫ (x : ℝ) in Icc (2 * T) (2 * T + 1), q x ≤ ∫ (x : ℝ) in Ioi T, q xhsplit:∫ (x : ℝ) in Ioi 0, q x ∂volume - ∫ (x : ℝ) in Ioi T, q x ∂volume = ∫ (t : ℝ) in Icc 0 T, q t ∂volumehhead:-∫ (a : ℝ) in Icc 0 T, q a ≤ ∫ (x : ℝ) in Icc 0 T, |q x|⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), q t ≤ (∫ (t : ℝ) in Ioi 0, q t) + ∫ (t : ℝ) in Icc 0 T, |q t|
  linarithAll goals completed! 🐙theorem continuous_normalizedHardyKernel (k : ℕ) (h : ℝ) :
    Continuous (normalizedHardyKernel k h) := byk:ℕh:ℝ⊢ Continuous (normalizedHardyKernel k h)
  unfold normalizedHardyKernel differenceMultiplierk:ℕh:ℝ⊢ Continuous fun t =>
  (2 * (Real.cosh (h * t) - Real.cos (h / 2)) / h ^ 2) ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t)
  fun_propAll goals completed! 🐙theorem tendsto_compact_normalizedHardyKernel {f : ℝ → ℝ} (hf : Continuous f)
    (k : ℕ) (l r : ℝ) :
    Tendsto (fun h : ℝ ↦ ∫ t in Icc l r, f t * normalizedHardyKernel k h t)
      (𝓝[>] 0) (𝓝 (∫ t in Icc l r,
        f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t))) := byf:ℝ → ℝhf:Continuous fk:ℕl:ℝr:ℝ⊢ Tendsto (fun h => ∫ (t : ℝ) in Icc l r, f t * normalizedHardyKernel k h t) (𝓝[>] 0)
  (𝓝 (∫ (t : ℝ) in Icc l r, f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))
  simpa only [normalizedHardyKernel, mul_assoc] using
    tendsto_integral_differenceKernel_Icc hf (Real.pi / 4) ((k : ℝ) + 1) l r kAll goals completed! 🐙theorem boundary_compact_comparison {f : ℝ → ℝ} (hf : Continuous f)
    {T : ℝ} (hT : 0 < T) (hpos : ∀ t > T, 0 ≤ f t) (k : ℕ)
    (hi : ∀ᶠ h : ℝ in 𝓝[>] 0,
      IntegrableOn (fun t ↦ f t * normalizedHardyKernel k h t) (Ioi 0))
    (hl : Tendsto (fun h : ℝ ↦ ∫ t in Ioi 0, f t * normalizedHardyKernel k h t)
      (𝓝[>] 0) (𝓝 0)) :
    (∫ t in Icc (2 * T) (2 * T + 1),
      f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)) ≤
    ∫ t in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t) := byf:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ f tk:ℕhi:∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel k h t) (Ioi 0) volumehl:Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k h t) (𝓝[>] 0) (𝓝 0)⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t) ≤
  ∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)
  have hleft := tendsto_compact_normalizedHardyKernel hf k (2 * T) (2 * T + 1)f:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ f tk:ℕhi:∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel k h t) (Ioi 0) volumehl:Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k h t) (𝓝[>] 0) (𝓝 0)hleft:Tendsto (fun h => ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * normalizedHardyKernel k h t) (𝓝[>] 0)
  (𝓝 (∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t) ≤
  ∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)
  have hright := hl.add (tendsto_compact_normalizedHardyKernel hf.abs k 0 T)f:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ f tk:ℕhi:∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel k h t) (Ioi 0) volumehl:Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k h t) (𝓝[>] 0) (𝓝 0)hleft:Tendsto (fun h => ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * normalizedHardyKernel k h t) (𝓝[>] 0)
  (𝓝 (∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))hright:Tendsto
  (fun x =>
    (∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k x t) + ∫ (t : ℝ) in Icc 0 T, |f t| * normalizedHardyKernel k x t)
  (𝓝[>] 0) (𝓝 (0 + ∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t) ≤
  ∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)
  simp only [zero_add] at hrightf:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ f tk:ℕhi:∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel k h t) (Ioi 0) volumehl:Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k h t) (𝓝[>] 0) (𝓝 0)hleft:Tendsto (fun h => ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * normalizedHardyKernel k h t) (𝓝[>] 0)
  (𝓝 (∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))hright:Tendsto
  (fun x =>
    (∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k x t) + ∫ (t : ℝ) in Icc 0 T, |f t| * normalizedHardyKernel k x t)
  (𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t) ≤
  ∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)
  apply le_of_tendsto_of_tendsto hleft hrightf:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ f tk:ℕhi:∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel k h t) (Ioi 0) volumehl:Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k h t) (𝓝[>] 0) (𝓝 0)hleft:Tendsto (fun h => ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * normalizedHardyKernel k h t) (𝓝[>] 0)
  (𝓝 (∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))hright:Tendsto
  (fun x =>
    (∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k x t) + ∫ (t : ℝ) in Icc 0 T, |f t| * normalizedHardyKernel k x t)
  (𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))⊢ (fun h => ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * normalizedHardyKernel k h t) ≤ᶠ[𝓝[>] 0] fun x =>
  (∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k x t) + ∫ (t : ℝ) in Icc 0 T, |f t| * normalizedHardyKernel k x t
  filter_upwards [hi] with h hhf:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ f tk:ℕhi:∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel k h t) (Ioi 0) volumehl:Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k h t) (𝓝[>] 0) (𝓝 0)hleft:Tendsto (fun h => ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * normalizedHardyKernel k h t) (𝓝[>] 0)
  (𝓝 (∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))hright:Tendsto
  (fun x =>
    (∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k x t) + ∫ (t : ℝ) in Icc 0 T, |f t| * normalizedHardyKernel k x t)
  (𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))h:ℝhh:IntegrableOn (fun t => f t * normalizedHardyKernel k h t) (Ioi 0) volume⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * normalizedHardyKernel k h t ≤
  (∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k h t) + ∫ (t : ℝ) in Icc 0 T, |f t| * normalizedHardyKernel k h t
  have hc := compact_tail_le_total_add_initial
    (hf.mul (continuous_normalizedHardyKernel k h)) hh hT
    (fun t ht ↦ mul_nonneg (hpos t ht) (normalizedHardyKernel_nonneg k h t))f:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ f tk:ℕhi:∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel k h t) (Ioi 0) volumehl:Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k h t) (𝓝[>] 0) (𝓝 0)hleft:Tendsto (fun h => ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * normalizedHardyKernel k h t) (𝓝[>] 0)
  (𝓝 (∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))hright:Tendsto
  (fun x =>
    (∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k x t) + ∫ (t : ℝ) in Icc 0 T, |f t| * normalizedHardyKernel k x t)
  (𝓝[>] 0) (𝓝 (∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))h:ℝhh:IntegrableOn (fun t => f t * normalizedHardyKernel k h t) (Ioi 0) volumehc:∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), (f * normalizedHardyKernel k h) t ≤
  (∫ (t : ℝ) in Ioi 0, (f * normalizedHardyKernel k h) t) + ∫ (t : ℝ) in Icc 0 T, |(f * normalizedHardyKernel k h) t|⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * normalizedHardyKernel k h t ≤
  (∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel k h t) + ∫ (t : ℝ) in Icc 0 T, |f t| * normalizedHardyKernel k h t
  simpa only [Pi.mul_apply, abs_mul, abs_of_nonneg (normalizedHardyKernel_nonneg k h _)] using hcAll goals completed! 🐙theorem positive_tail_mass {w : ℝ → ℝ} (hw : Continuous w) {T : ℝ}
    (hT : 0 < T) (hpos : ∀ t > T, 0 < w t) :
    0 < ∫ t in Icc (2 * T) (2 * T + 1), w t := byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w t⊢ 0 < ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t
  rw [integral_Icc_eq_integral_Ioc,w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w t⊢ 0 < ∫ (t : ℝ) in Ioc (2 * T) (2 * T + 1), w t
    ← intervalIntegral.integral_of_le (byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w t⊢ 2 * T ≤ 2 * T + 1 linarithAll goals completed! 🐙 : 2 * T ≤ 2 * T + 1)]w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w t⊢ 0 < ∫ (x : ℝ) in 2 * T..2 * T + 1, w x
  apply intervalIntegral.integral_pos (byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w t⊢ 2 * T < 2 * T + 1 linarithAll goals completed! 🐙) hw.continuousOn
  ·hlew:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w t⊢ ∀ x ∈ Ioc (2 * T) (2 * T + 1), 0 ≤ w x intro t hthlew:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w tt:ℝht:t ∈ Ioc (2 * T) (2 * T + 1)⊢ 0 ≤ w t
    exact (hpos t (byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w tt:ℝht:t ∈ Ioc (2 * T) (2 * T + 1)⊢ t > T linarith [ht.1]All goals completed! 🐙)).le
  ·hltw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w t⊢ ∃ c ∈ Icc (2 * T) (2 * T + 1), 0 < w c exact ⟨2 * T, ⟨le_rfl, byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w t⊢ 2 * T ≤ 2 * T + 1 linarithAll goals completed! 🐙⟩, hpos _ (byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w t⊢ 2 * T > T linarithAll goals completed! 🐙)⟩theorem initial_polynomial_bound {w : ℝ → ℝ} (hw : Continuous w)
    {T : ℝ} (hT : 0 < T) (k : ℕ) :
    (∫ t in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ k) ≤
      (∫ t in Icc 0 T, |w t|) * (T ^ 2 + 1 / 4) ^ k := byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Tk:ℕ⊢ ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ k ≤ (∫ (t : ℝ) in Icc 0 T, |w t|) * (T ^ 2 + 1 / 4) ^ k
  rw [← integral_mul_constw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Tk:ℕ⊢ ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ k ≤ ∫ (a : ℝ) in Icc 0 T, |w a| * (T ^ 2 + 1 / 4) ^ k]w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Tk:ℕ⊢ ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ k ≤ ∫ (a : ℝ) in Icc 0 T, |w a| * (T ^ 2 + 1 / 4) ^ k
  apply setIntegral_mono_on (μ := volume)
    (show Continuous (fun t : ℝ ↦ |w t| * (t ^ 2 + 1 / 4) ^ k) byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Tk:ℕ⊢ ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ k ≤ (∫ (t : ℝ) in Icc 0 T, |w t|) * (T ^ 2 + 1 / 4) ^ k fun_propAll goals completed! 🐙).integrableOn_Icc
    (hw.abs.mul_const _).integrableOn_Icc measurableSet_Icc
  intro t htw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Tk:ℕt:ℝht:t ∈ Icc 0 T⊢ |w t| * (t ^ 2 + 1 / 4) ^ k ≤ |w t| * (T ^ 2 + 1 / 4) ^ k
  apply mul_le_mul_of_nonneg_left _ (abs_nonneg _)w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Tk:ℕt:ℝht:t ∈ Icc 0 T⊢ (t ^ 2 + 1 / 4) ^ k ≤ (T ^ 2 + 1 / 4) ^ k
  apply pow_le_pow_left₀ (byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Tk:ℕt:ℝht:t ∈ Icc 0 T⊢ 0 ≤ t ^ 2 + 1 / 4 positivityAll goals completed! 🐙)
  nlinarith [ht.1, ht.2]All goals completed! 🐙theorem tail_polynomial_bound {w : ℝ → ℝ} (hw : Continuous w)
    {T : ℝ} (hT : 0 < T) (hpos : ∀ t > T, 0 ≤ w t) (k : ℕ) :
    (∫ t in Icc (2 * T) (2 * T + 1), w t) * ((2 * T) ^ 2 + 1 / 4) ^ k ≤
      ∫ t in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ k := byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ w tk:ℕ⊢ (∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t) * ((2 * T) ^ 2 + 1 / 4) ^ k ≤
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ k
  rw [← integral_mul_constw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ w tk:ℕ⊢ ∫ (a : ℝ) in Icc (2 * T) (2 * T + 1), w a * ((2 * T) ^ 2 + 1 / 4) ^ k ≤
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ k]w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ w tk:ℕ⊢ ∫ (a : ℝ) in Icc (2 * T) (2 * T + 1), w a * ((2 * T) ^ 2 + 1 / 4) ^ k ≤
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ k
  apply setIntegral_mono_on (μ := volume)
    (hw.mul_const _).integrableOn_Icc
    (show Continuous (fun t : ℝ ↦ w t * (t ^ 2 + 1 / 4) ^ k) byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ w tk:ℕ⊢ (∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t) * ((2 * T) ^ 2 + 1 / 4) ^ k ≤
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ k fun_propAll goals completed! 🐙).integrableOn_Icc
    measurableSet_Icc
  intro t htw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ w tk:ℕt:ℝht:t ∈ Icc (2 * T) (2 * T + 1)⊢ w t * ((2 * T) ^ 2 + 1 / 4) ^ k ≤ w t * (t ^ 2 + 1 / 4) ^ k
  apply mul_le_mul_of_nonneg_left _ (hpos t (byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ w tk:ℕt:ℝht:t ∈ Icc (2 * T) (2 * T + 1)⊢ t > T linarith [ht.1]All goals completed! 🐙))
  apply pow_le_pow_left₀ (byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 ≤ w tk:ℕt:ℝht:t ∈ Icc (2 * T) (2 * T + 1)⊢ 0 ≤ (2 * T) ^ 2 + 1 / 4 positivityAll goals completed! 🐙)
  nlinarith [ht.1]All goals completed! 🐙theorem not_positive_tail_of_compact_moments {w : ℝ → ℝ} (hw : Continuous w)
    {T : ℝ} (hT : 0 < T) (hpos : ∀ t > T, 0 < w t)
    (hcomp : ∀ k : ℕ,
      (∫ t in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1)) ≤
        ∫ t in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)) : False := byw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)⊢ False
  let m := ∫ t in Icc (2 * T) (2 * T + 1), w tw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t⊢ False
  let R := ∫ t in Icc 0 T, |w t|w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|⊢ False
  let A := T ^ 2 + 1 / 4w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4⊢ False
  let B := (2 * T) ^ 2 + 1 / 4w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4⊢ False
  have hm : 0 < m := positive_tail_mass hw hT hposw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < m⊢ False
  have hA : 0 < A := by dsimp [A]w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < m⊢ 0 < T ^ 2 + 1 / 4; positivityw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < mhA:0 < A⊢ False
  have hB : 0 < B := by dsimp [B]w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < mhA:0 < A⊢ 0 < (2 * T) ^ 2 + 1 / 4; positivityw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < mhA:0 < AhB:0 < B⊢ False
  have hAB : A < B := by dsimp [A, B]w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < mhA:0 < AhB:0 < B⊢ T ^ 2 + 1 / 4 < (2 * T) ^ 2 + 1 / 4; nlinarith [sq_pos_of_pos hT]w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < mhA:0 < AhB:0 < BhAB:A < B⊢ False
  apply not_geometric_domination (m := m * B) (R := R * A) (mul_pos hm hB) hA hABw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < mhA:0 < AhB:0 < BhAB:A < B⊢ ∀ (k : ℕ), m * B * B ^ k ≤ R * A * A ^ k
  intro kw:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < mhA:0 < AhB:0 < BhAB:A < Bk:ℕ⊢ m * B * B ^ k ≤ R * A * A ^ k
  have he := (tail_polynomial_bound hw hT (fun t ht ↦ (hpos t ht).le) (k + 1)).trans
    ((hcomp k).trans (initial_polynomial_bound hw hT (k + 1)))w:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < mhA:0 < AhB:0 < BhAB:A < Bk:ℕhe:(∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t) * ((2 * T) ^ 2 + 1 / 4) ^ (k + 1) ≤
  (∫ (t : ℝ) in Icc 0 T, |w t|) * (T ^ 2 + 1 / 4) ^ (k + 1)⊢ m * B * B ^ k ≤ R * A * A ^ k
  change m * B ^ (k + 1) ≤ R * A ^ (k + 1) at hew:ℝ → ℝhw:Continuous wT:ℝhT:0 < Thpos:∀ t > T, 0 < w thcomp:∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)m:ℝ := ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w tR:ℝ := ∫ (t : ℝ) in Icc 0 T, |w t|A:ℝ := T ^ 2 + 1 / 4B:ℝ := (2 * T) ^ 2 + 1 / 4hm:0 < mhA:0 < AhB:0 < BhAB:A < Bk:ℕhe:m * B ^ (k + 1) ≤ R * A ^ (k + 1)⊢ m * B * B ^ k ≤ R * A * A ^ k
  simpa only [pow_succ, ← mul_assoc, mul_right_comm] using heAll goals completed! 🐙theorem not_positive_tail_of_vanishing_differences {f : ℝ → ℝ} (hf : Continuous f)
    {T : ℝ} (hT : 0 < T) (hpos : ∀ t > T, 0 < f t)
    (hi : ∀ k : ℕ, ∀ᶠ h : ℝ in 𝓝[>] 0,
      IntegrableOn (fun t ↦ f t * normalizedHardyKernel (k + 1) h t) (Ioi 0))
    (hl : ∀ k : ℕ, Tendsto (fun h : ℝ ↦ ∫ t in Ioi 0,
      f t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0)) : False := byf:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 < f thi:∀ (k : ℕ), ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volumehl:∀ (k : ℕ), Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0)⊢ False
  let w : ℝ → ℝ := fun t ↦ f t * Real.cosh (Real.pi / 4 * t)f:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 < f thi:∀ (k : ℕ), ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volumehl:∀ (k : ℕ), Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0)w:ℝ → ℝ := fun t => f t * Real.cosh (Real.pi / 4 * t)⊢ False
  have hw : Continuous w := by dsimp [w]f:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 < f thi:∀ (k : ℕ), ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volumehl:∀ (k : ℕ), Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0)w:ℝ → ℝ := fun t => f t * Real.cosh (Real.pi / 4 * t)⊢ Continuous fun t => f t * Real.cosh (Real.pi / 4 * t); fun_propf:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 < f thi:∀ (k : ℕ), ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volumehl:∀ (k : ℕ), Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0)w:ℝ → ℝ := fun t => f t * Real.cosh (Real.pi / 4 * t)hw:Continuous w⊢ False
  apply not_positive_tail_of_compact_moments hw hT
    (fun t ht ↦ mul_pos (hpos t ht) (Real.cosh_pos _))f:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 < f thi:∀ (k : ℕ), ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volumehl:∀ (k : ℕ), Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0)w:ℝ → ℝ := fun t => f t * Real.cosh (Real.pi / 4 * t)hw:Continuous w⊢ ∀ (k : ℕ),
  ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
    ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)
  intro kf:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 < f thi:∀ (k : ℕ), ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volumehl:∀ (k : ℕ), Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0)w:ℝ → ℝ := fun t => f t * Real.cosh (Real.pi / 4 * t)hw:Continuous wk:ℕ⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
  ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)
  have hc := boundary_compact_comparison hf hT (fun t ht ↦ (hpos t ht).le)
    (k + 1) (hi k) (hl k)f:ℝ → ℝhf:Continuous fT:ℝhT:0 < Thpos:∀ t > T, 0 < f thi:∀ (k : ℕ), ∀ᶠ (h : ℝ) in 𝓝[>] 0, IntegrableOn (fun t => f t * normalizedHardyKernel (k + 1) h t) (Ioi 0) volumehl:∀ (k : ℕ), Tendsto (fun h => ∫ (t : ℝ) in Ioi 0, f t * normalizedHardyKernel (k + 1) h t) (𝓝[>] 0) (𝓝 0)w:ℝ → ℝ := fun t => f t * Real.cosh (Real.pi / 4 * t)hw:Continuous wk:ℕhc:∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ (k + 1) * Real.cosh (Real.pi / 4 * t) ≤
  ∫ (t : ℝ) in Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ (k + 1) * Real.cosh (Real.pi / 4 * t)⊢ ∫ (t : ℝ) in Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
  ∫ (t : ℝ) in Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)
  simpa only [w, abs_mul, abs_of_pos (Real.cosh_pos _), mul_right_comm] using hcAll goals completed! 🐙