kernel_response_limit
The declaration proves that the truncated response integral for the Debye kernel converges pointwise in frequency to the closed-form expression Δ / (1 + iωτ) as the upper limit B tends to infinity. Researchers modeling causal memory effects in gravitational or cosmological systems would invoke this result to justify replacing finite-time truncations with the steady-state transfer function. The proof derives an explicit antiderivative for the truncated integral using the exponential integral lemma, establishes that the real part of the Laplace a
claimLet $H$ be a Caldeira-Leggett transfer function with positive parameters $Δ$ and $τ$, and let $ω ∈ ℝ$. Then the limit as $B → +∞$ of the truncated Debye-kernel response at frequency $ω$ equals $Δ / (1 + i ω τ)$.
background
The CausalKernelChain module develops the frequency-domain properties of the single-timescale exponential memory kernel, known as the Debye kernel. This kernel arises as the exponential case in BITKernelFamilies, where the kernel function returns exp(-z/z0). The transfer function $H$ encodes response parameters $Δ$ (strength) and $τ$ (timescale). The Laplace exponent $a = 1/τ + iω$ appears in the complex exponential decay of the integrand for the response integral.
proof idea
The proof first defines $a :=$ laplaceExponent $H$ $ω$ and verifies that its real part equals $1/τ > 0$. It then establishes a closed-form expression for the truncated response by rewriting the integrand as a multiple of exp($t$ • (-$a$)) and applying the integral_exp_smul_neg lemma. With the closed form in hand, it shows that exp($B$ • (-$a$)) tends to zero using tendsto_exp_neg_mul_ofReal_atTop, subtracts the constant term, multiplies by the inverse, and scales by the prefactor $Δ/τ$. Algebraic simplification using the definition of $a$ yields the target expression.
why it matters in Recognition Science
This result closes the loop from the time-domain Debye kernel (defined via the exponential case in BITKernelFamilies.kernel) to its frequency response in the Caldeira-Leggett model. It supports the broader program of deriving transfer functions from causal kernels, where the exponential kernel corresponds to the single-pole response. No immediate downstream theorems depend on it yet, but it provides the rigorous justification for the Newtonian and steady-state limits mentioned in the module documentation.
scope and limits
- Does not extend to kernels with multiple timescales or continuous spectra.
- Does not address the ω → 0 or ω → ∞ limits of the response function.
- Does not prove uniqueness of the transfer function representation.
- Does not incorporate quantum corrections or higher-order effects.
formal statement (Lean)
169theorem kernel_response_limit (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
170 Filter.Tendsto (fun B => kernel_response_trunc H ω B) Filter.atTop
171 (nhds ((H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)))) := by
proof body
Tactic-mode proof.
172 -- Abbreviate `a = (1/τ) + iω`.
173 set a : ℂ := laplaceExponent H ω with ha_def
174
175 have ha_re : 0 < a.re := by
176 have h : 0 < (1 / H.τ) := one_div_pos.2 H.τ_pos
177 -- `a.re = 1/τ` since `Re(iω)=0`.
178 simpa [ha_def, laplaceExponent] using h
179
180 have ha : a ≠ 0 := by
181 have hne : a.re ≠ 0 := ne_of_gt ha_re
182 intro h0
183 apply hne
184 simpa [h0]
185
186 -- Closed form for each truncation bound `B`.
187 have hclosed (B : ℝ) :
188 kernel_response_trunc H ω B =
189 (H.Δ / H.τ : ℂ) * ((Complex.exp (B • (-a)) - 1) * (-a)⁻¹) := by
190 -- Rewrite the integrand into the `exp (t • (-a))` shape and apply `integral_exp_smul_neg`.
191 unfold kernel_response_trunc
192 -- Push the real kernel into `ℂ`, and turn `Real.exp` into `Complex.exp`.
193 simp_rw [debye_kernel]
194 simp_rw [Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_exp]
195 -- Combine the two exponentials.
196 simp_rw [← Complex.exp_add, ← mul_assoc, ← mul_left_comm, ← mul_comm]
197 -- Pull out the constant factor and evaluate the remaining exponential integral.
198 -- (At this point the integrand is exactly `exp (t • (-a))` after simp.)
199 simp [ha_def, laplaceExponent, Complex.real_smul, intervalIntegral.integral_const_mul,
200 integral_exp_smul_neg a ha B, mul_assoc, mul_left_comm, mul_comm, add_assoc, add_left_comm,
201 add_comm]
202
203 -- Reduce to the closed form and take `B → ∞`.
204 have hExp :
205 Filter.Tendsto (fun B : ℝ => Complex.exp (B • (-a))) Filter.atTop (nhds (0 : ℂ)) := by
206 -- `B • (-a) = -((B:ℂ) * a)`, and `Re(a) > 0`.
207 have :=
208 tendsto_exp_neg_mul_ofReal_atTop a ha_re
209 simpa [Complex.real_smul, mul_assoc, mul_left_comm, mul_comm] using this
210
211 have hExpSub :
212 Filter.Tendsto (fun B : ℝ => Complex.exp (B • (-a)) - (1 : ℂ)) Filter.atTop (nhds (-1 : ℂ)) :=
213 (hExp.sub tendsto_const_nhds)
214
215 have hExpMul :
216 Filter.Tendsto (fun B : ℝ => (Complex.exp (B • (-a)) - (1 : ℂ)) * (-a)⁻¹) Filter.atTop
217 (nhds ((-1 : ℂ) * (-a)⁻¹)) :=
218 (Filter.Tendsto.mul_const (-a)⁻¹ hExpSub)
219
220 have hMain :
221 Filter.Tendsto (fun B : ℝ => (H.Δ / H.τ : ℂ) * ((Complex.exp (B • (-a)) - 1) * (-a)⁻¹))
222 Filter.atTop (nhds ((H.Δ / H.τ : ℂ) * ((-1 : ℂ) * (-a)⁻¹))) :=
223 (Filter.Tendsto.const_mul (H.Δ / H.τ : ℂ) hExpMul)
224
225 -- Rewrite the limit into the desired `Δ / (1 + iωτ)` form.
226 have hlim_simplify :
227 (H.Δ / H.τ : ℂ) * ((-1 : ℂ) * (-a)⁻¹) =
228 (H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)) := by
229 -- `(-1) * (-a)⁻¹ = a⁻¹`, then regroup as a division by `τ*a = 1 + iωτ`.
230 have : ((-1 : ℂ) * (-a)⁻¹) = a⁻¹ := by
231 -- `(-a)⁻¹ = -(a⁻¹)`
232 simp
233 -- Rewrite `(Δ/τ) * a⁻¹` as `Δ / (τ * a)`, and compute `τ * a`.
234 -- Use `ha_def` to expand `a = (1/τ) + iω`.
235 -- `τ * ((1/τ) + iω) = 1 + iωτ`.
236 -- Finally, cast `Δ/τ` into `ℂ` consistently.
237 simp [this, ha_def, laplaceExponent, div_div, div_eq_mul_inv, mul_add, add_mul,
238 mul_assoc, mul_left_comm, mul_comm]
239
240 -- Assemble the tendsto statement.
241 have hMain' :
242 Filter.Tendsto (fun B : ℝ => kernel_response_trunc H ω B) Filter.atTop
243 (nhds ((H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)))) := by
244 -- Rewrite by the pointwise closed form, then apply `hMain`.
245 have hcongr :
246 (fun B : ℝ => kernel_response_trunc H ω B) =
247 fun B : ℝ => (H.Δ / H.τ : ℂ) * ((Complex.exp (B • (-a)) - 1) * (-a)⁻¹) := by
248 funext B
249 simpa [hclosed B]
250 -- Transfer the limit.
251 simpa [hcongr, hlim_simplify] using hMain
252-- ... 6 more lines elided ...