Eq.(12): bright-noise leading coherent exponent

Proved

QAlgorithms.Papers.Independent.Intakenext100.P85.coherent_bright_noise_exponent

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Fix $0<\kappa<1$ and $N_S\ge0$ . Let $c(\kappa,N_S,N_B)=\kappa N_S(\sqrt{N_B+1}-\sqrt{N_B})^2$ be the exact exponent coefficient in the coherent Chernoff upper bound. Then

\lim_{N_B\to\infty}N_B\,c(\kappa,N_S,N_B)=\frac{\kappa N_S}{4}.

This pins the leading bright-noise coefficient in Eq.(12). It does not specify a simultaneous copy-number limit or a uniform relative approximation of exponentially small error bounds.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P85

Formal statement

noncomputable section

open MeasureTheory Filter

open scoped BigOperators ENNReal Topology

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakenext100.P85

open QAlgorithms.Papers.Independent.Claimed50.P19 (Cov)

open QAlgorithms.Papers.Independent.Renew46.P41 (coherentProductCoefficient)

/-- Source p.3, Eq.(12): leading coefficient of the coherent upper-bound
exponent as NB tends to infinity, with k and NS fixed. No uniform relative
approximation of exponentials for arbitrarily growing M is asserted. -/
theorem coherent_bright_noise_exponent (k NS : ℝ)
    (hk : 0 < k) (hk1 : k < 1) (hNS : 0 ≤ NS) :
    Tendsto (fun NB : ℝ => NB * coherentExponent k NS NB)
      atTop (nhds (k * NS / 4)) := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P85

end

Source

Quantum Illumination with Gaussian States, arXiv:0810.0534v1, PDF p. 3, Eq.(12): bright-noise leading coherent exponent

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every real $k$ with $0<k<1$ and every real $N_S\ge0$ ,

N_B\,kN_S\bigl(\sqrt{N_B+1}-\sqrt{N_B}\bigr)^2 \longrightarrow \frac{kN_S}{4} \qquad\text{as the real variable }N_B\to+\infty.

The quantified function is defined on all real $N_B$ , using the total real square-root function, and the limit is along $+\infty$ . The case $N_S=0$ , in which the function and limiting value are zero, is included.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph