Heavy-tail Laplace expansion and canonical tail normalization

The tail convention throughout is the strict right tail. The canonical constant is -Gamma (1 - θ), which is positive for 1 < θ < 2.

The proof applies Laplace--Karamata to the square-weighted absolute-step law, then integrates its transform twice using Taylor's formula and a dyadic power majorant. The negative atom and deterministic centering give negligible quadratic corrections. The final theorem supplies the one-step limit for D2. Ported from BGWLeaves/StableAnalysis/LaplaceExpansion.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

noncomputable def BGW.StableTrees.Attraction.LaplaceExpansion.centeredLaplace (ν : MeasureTheory.Measure ℤ) (s : ℝ) : ℝ

The centered one-step Laplace transform.

Equations

• BGW.StableTrees.Attraction.LaplaceExpansion.centeredLaplace ν s = ∫ (z : ℤ), Real.exp (-s * (↑z - BGW.StableTrees.Attraction.mean ν)) ∂ν

noncomputable def BGW.StableTrees.Attraction.LaplaceExpansion.tailNorming (ν : MeasureTheory.Measure ℤ) (θ : ℝ) (n : ℕ) : ℝ

The corrected tail norming, before selecting the variance branch of norming.

Equations

• BGW.StableTrees.Attraction.LaplaceExpansion.tailNorming ν θ n = (-Real.Gamma (1 - θ)) ^ (1 / θ) * BGW.StableTrees.Attraction.tailQuantile ν n

theorem BGW.StableTrees.Attraction.LaplaceExpansion.uncenteredLaplace_integrable {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) {s : ℝ} (hs : 0 ≤ s) : MeasureTheory.Integrable (fun (z : ℤ) => Real.exp (-s * ↑z)) ν

theorem BGW.StableTrees.Attraction.LaplaceExpansion.centeredLaplace_integrable {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) {s : ℝ} (hs : 0 ≤ s) : MeasureTheory.Integrable (fun (z : ℤ) => Real.exp (-s * (↑z - mean ν))) ν

theorem BGW.StableTrees.Attraction.LaplaceExpansion.centeredLaplace_eq (ν : MeasureTheory.Measure ℤ) (s : ℝ) : centeredLaplace ν s = Real.exp (s * mean ν) * ∫ (z : ℤ), Real.exp (-s * ↑z) ∂ν

theorem BGW.StableTrees.Attraction.LaplaceExpansion.centeredLaplace_sub_one_eq_integral {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {s : ℝ} (hs : 0 ≤ s) : centeredLaplace ν s - 1 = ∫ (z : ℤ), Real.exp (-s * (↑z - mean ν)) - 1 + s * (↑z - mean ν) ∂ν

Centering removes the linear term exactly inside the expectation.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.regularlyVarying_of_nonneg {T : ℝ → ℝ} {ρ : ℝ} (hnn : ∀ (x : ℝ), 0 ≤ T x) (hT : MonotoneDensity.IsRegVaryAtTop T ρ) : KaramataTransforms.RegularlyVarying T ρ

Convert the ratio-only convention to the positive-function convention.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.slowlyVarying_factor {T : ℝ → ℝ} {θ : ℝ} (hnn : ∀ (x : ℝ), 0 ≤ T x) (hT : MonotoneDensity.IsRegVaryAtTop T (-θ)) : SlowlyVarying fun (x : ℝ) => x ^ θ * T x

The slowly varying factor extracted from a regularly varying nonnegative function.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.rpow_mul_tail_tendsto_atTop {T : ℝ → ℝ} {θ p : ℝ} (hnn : ∀ (x : ℝ), 0 ≤ T x) (hmeas : Measurable T) (hT : MonotoneDensity.IsRegVaryAtTop T (-θ)) (hp : θ < p) : Filter.Tendsto (fun (x : ℝ) => x ^ p * T x) Filter.atTop Filter.atTop

Polynomially weighted tails grow when the weight exceeds the tail index.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.quadratic_div_tail_tendsto_zero {T : ℝ → ℝ} {θ : ℝ} (hnn : ∀ (x : ℝ), 0 ≤ T x) (hmeas : Measurable T) (hT : MonotoneDensity.IsRegVaryAtTop T (-θ)) (hθ : θ < 2) (C : ℝ) : Filter.Tendsto (fun (x : ℝ) => C / x ^ 2 / T x) Filter.atTop (nhds 0)

Any bounded quadratic correction is negligible on the heavy-tail scale.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.exp_remainder_div_tail_tendsto_zero {T : ℝ → ℝ} {θ : ℝ} (hnn : ∀ (x : ℝ), 0 ≤ T x) (hmeas : Measurable T) (hT : MonotoneDensity.IsRegVaryAtTop T (-θ)) (hθ : θ < 2) (m : ℝ) : Filter.Tendsto (fun (x : ℝ) => (Real.exp (m / x) - 1 - m / x) / T x) Filter.atTop (nhds 0)

The quadratic Taylor remainder of a deterministic exponential is negligible relative to a tail of index strictly below two.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.centered_ratio_of_uncentered {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) {C : ℝ} (hU : Filter.Tendsto (fun (x : ℝ) => (∫ (z : ℤ), Real.exp (-(1 / x) * ↑z) ∂ν - 1 + mean ν / x) / ν.real {z : ℤ | x < ↑z}) Filter.atTop (nhds C)) : Filter.Tendsto (fun (x : ℝ) => (centeredLaplace ν (1 / x) - 1) / ν.real {z : ℤ | x < ↑z}) Filter.atTop (nhds C)

Multiplication by the deterministic centering exponential does not alter the heavy-tail expansion. The hypothesis concerns only the uncentered remainder.

noncomputable def BGW.StableTrees.Attraction.LaplaceExpansion.secondMomentMeasure (ν : MeasureTheory.Measure ℤ) : MeasureTheory.Measure ℝ

The square-weighted law of the absolute step. Its cumulative mass is the truncated second moment, with no correction for the negative atom.

Equations

• BGW.StableTrees.Attraction.LaplaceExpansion.secondMomentMeasure ν = (MeasureTheory.Measure.map (fun (z : ℤ) => |↑z|) ν).withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ 2)

instance BGW.StableTrees.Attraction.LaplaceExpansion.secondMomentMeasure_locallyFinite (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsLocallyFiniteMeasure (secondMomentMeasure ν)

theorem BGW.StableTrees.Attraction.LaplaceExpansion.secondMomentMeasure_cumulative (ν : MeasureTheory.Measure ℤ) (x : ℝ) : KaramataTransforms.cumulative (secondMomentMeasure ν) x = truncSecondMoment ν x

theorem BGW.StableTrees.Attraction.LaplaceExpansion.truncatedMoment_regularlyVarying {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : KaramataTransforms.RegularlyVarying (truncSecondMoment ν) (2 - θ)

The truncated second moment is regularly varying with index 2 - θ, in the positive-function convention required by Laplace--Karamata.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.secondMomentMeasure_laplace_integrable (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {s : ℝ} (hs : 0 < s) : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) (secondMomentMeasure ν)

The weighted measure has a finite Laplace transform at every positive argument, even when the unweighted law has infinite second moment.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.secondMomentMeasure_laplace (ν : MeasureTheory.Measure ℤ) (s : ℝ) : KaramataTransforms.laplace (secondMomentMeasure ν) s = ∫ (z : ℤ), ↑z ^ 2 * Real.exp (-s * |↑z|) ∂ν

The transform of the square-weighted law is the exponentially damped second moment of the absolute step.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.dampedSecondMoment_div_tail_tendsto (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Filter.Tendsto (fun (x : ℝ) => (∫ (z : ℤ), ↑z ^ 2 * Real.exp (-(1 / x) * |↑z|) ∂ν) / (x ^ 2 * ν.real {z : ℤ | x < ↑z})) Filter.atTop (nhds (θ * Real.Gamma (2 - θ)))

An Abelian second-moment expansion, obtained directly from the proved Laplace--Karamata provider. This is integrated twice below to obtain the one-step Laplace remainder.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.reciprocal_integral_ratio_tendsto {G : ℝ → ℝ} {ρ : ℝ} (hnn : ∀ (x : ℝ), 0 ≤ G x) (hmono : Monotone G) (hG : KaramataTransforms.RegularlyVarying G ρ) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioo 0 1, (1 - t) * (G (x / t) / G x)) Filter.atTop (nhds (∫ (t : ℝ) in Set.Ioo 0 1, (1 - t) * t ^ (-ρ)))

Integrating a reciprocal rescaling of a monotone regularly varying function. The index restriction below one supplies an integrable power majorant at zero.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.reciprocal_integral_ratio_limit {G : ℝ → ℝ} {ρ : ℝ} (hnn : ∀ (x : ℝ), 0 ≤ G x) (hmono : Monotone G) (hG : KaramataTransforms.RegularlyVarying G ρ) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioo 0 1, (1 - t) * (G (x / t) / G x)) Filter.atTop (nhds (1 / ((1 - ρ) * (2 - ρ))))

The explicit constant in the twice-integrated reciprocal rescaling.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.exp_remainder_integral {s : ℝ} (hs : s ≠ 0) (y : ℝ) : ∫ (t : ℝ) in Set.Ioo 0 1, (1 - t) * (y ^ 2 * Real.exp (-s * t * y)) = (Real.exp (-s * y) - 1 + s * y) / s ^ 2

Exact scalar Taylor integral, before taking the step-law expectation.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.absolute_remainder_eq_integrated_laplace {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {s : ℝ} (hs : 0 < s) : (∫ (z : ℤ), Real.exp (-s * |↑z|) - 1 + s * |↑z| ∂ν) / s ^ 2 = ∫ (t : ℝ) in Set.Ioo 0 1, (1 - t) * KaramataTransforms.laplace (secondMomentMeasure ν) (s * t)

Fubini's formula for the exponential remainder of the absolute step. Finite first moment suffices; the second moment need not be finite.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.integrated_laplace_ratio_limit (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {ρ : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hU : KaramataTransforms.RegularlyVarying (KaramataTransforms.cumulative M) ρ) : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioo 0 1, (1 - t) * (KaramataTransforms.laplace M (t / x) / KaramataTransforms.laplace M (1 / x))) Filter.atTop (nhds (1 / ((1 - ρ) * (2 - ρ))))

The integrated Laplace kernel has the universal beta-integral constant.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.absolute_remainder_div_tail_tendsto (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Filter.Tendsto (fun (x : ℝ) => (∫ (z : ℤ), Real.exp (-(1 / x) * |↑z|) - 1 + 1 / x * |↑z| ∂ν) / ν.real {z : ℤ | x < ↑z}) Filter.atTop (nhds (-Real.Gamma (1 - θ)))

The Abelian expansion for the exponential remainder of the absolute step.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.uncentered_remainder_eq_absolute {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {s : ℝ} (hs : 0 ≤ s) : ∫ (z : ℤ), Real.exp (-s * ↑z) ∂ν - 1 + s * mean ν = ∫ (z : ℤ), Real.exp (-s * |↑z|) - 1 + s * |↑z| ∂ν + ν.real {-1} * (Real.exp s - Real.exp (-s) - 2 * s)

The bounded negative support contributes just the atom at -1.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.uncentered_remainder_div_tail_tendsto (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Filter.Tendsto (fun (x : ℝ) => (∫ (z : ℤ), Real.exp (-(1 / x) * ↑z) ∂ν - 1 + mean ν / x) / ν.real {z : ℤ | x < ↑z}) Filter.atTop (nhds (-Real.Gamma (1 - θ)))

The uncentered Laplace remainder has the heavy-tail Gamma constant.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.centeredLaplace_tail_ratio (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Filter.Tendsto (fun (x : ℝ) => (centeredLaplace ν (1 / x) - 1) / ν.real {z : ℤ | x < ↑z}) Filter.atTop (nhds (-Real.Gamma (1 - θ)))

D1: the centered Laplace expansion, in reciprocal tail-ratio form.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.centeredLaplace_expansion (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Filter.Tendsto (fun (s : ℝ) => (centeredLaplace ν s - 1) / ν.real {z : ℤ | 1 / s < ↑z}) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-Real.Gamma (1 - θ)))

D1 expressed at the positive side of zero.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.centeredLaplace_sub_one_isEquivalent (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Asymptotics.IsEquivalent (nhdsWithin 0 (Set.Ioi 0)) (fun (s : ℝ) => centeredLaplace ν s - 1) fun (s : ℝ) => -Real.Gamma (1 - θ) * ν.real {z : ℤ | 1 / s < ↑z}

The usual asymptotic-equivalence form of the centered expansion.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.not_integrable_sq_of_tail {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν

A tail index below two rules out a finite second moment.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.norming_eq_tailNorming {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : norming ν θ = tailNorming ν θ

On a regularly varying tail of index below two, norming selects the tail branch.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.tailNorming_tendsto_atTop {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : Filter.Tendsto (tailNorming ν θ) Filter.atTop Filter.atTop

theorem BGW.StableTrees.Attraction.LaplaceExpansion.canonical_mul_tail_tendsto {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fun (n : ℕ) => ↑n * -Real.Gamma (1 - θ) * ν.real {z : ℤ | tailNorming ν θ n / lam < ↑z}) Filter.atTop (nhds (lam ^ θ))

The corrected Gamma constant cancels the limiting tail intensity.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.canonical_limit_of_tail_ratio {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} {F : ℝ → ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) (hF : Filter.Tendsto (fun (x : ℝ) => (F (1 / x) - 1) / ν.real {z : ℤ | x < ↑z}) Filter.atTop (nhds (-Real.Gamma (1 - θ)))) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fun (n : ℕ) => ↑n * (F (lam / tailNorming ν θ n) - 1)) Filter.atTop (nhds (lam ^ θ))

Transfer an asymptotic formula on the reciprocal tail scale to the canonical sequence. This is a general transfer lemma; it does not assert the Abelian expansion.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.canonical_centeredLaplace_limit {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fun (n : ℕ) => ↑n * (centeredLaplace ν (lam / tailNorming ν θ n) - 1)) Filter.atTop (nhds (lam ^ θ))

The one-step limit needed by D2, with the corrected canonical tail norming.

theorem BGW.StableTrees.Attraction.LaplaceExpansion.norming_centeredLaplace_limit {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fun (n : ℕ) => ↑n * (centeredLaplace ν (lam / norming ν θ n) - 1)) Filter.atTop (nhds (lam ^ θ))

The same D2 input using the public canonical norming from Defs.