def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatExponentialDecay (H : Section13HatLayers) : Prop

The source-faithful κ=1 content of (T5): for each sign, T̂ is eventually bounded by a (sign-dependent) constant times exp (-s). This says decay only; it does not mention a pairing.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatExponentialDecay H = ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign), ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (s : ℝ) in Filter.atTop, |H.T sign s| ≤ C * Real.exp (-s)