Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: teretenkov-2024-interaction-picture-asymptotics
bibkey: madouremizovvafadar2024semigroups
doi: 10.48550/arXiv.2410.00416
url: https://arxiv.org/abs/2410.00416v2
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Semigroups/InteractionPictureAsymptotics.result

Interaction-picture asymptotics

Problem

F. Madou, I. Remizov, M. Vafadar (eds.), Open problems in one-parameter operator semigroups theory, arXiv:2410.00416v2, p. 21, Problem 29 (A. E. Teretenkov), state verbatim:

Problem 29 (A.E. Teretenkov). Let B be a Banach space. Let P be a projection on a finite-dimensional Banach subspace of B. Let L0 + λL be a generator of C0-semigroup U^λ_t on B for all λ ∈ [0, λsup). Let U^0_t leave both PB and its complement (I − P)B invariant, let PLP = 0. Denote L_t ≡ (U^0_t)^{−1} L U^0_t. Let the integrals ∫{−∞}^{t} dt_1 … ∫{−∞}^{t_{k−1}} dt_k P L_{t_1} … L_{t_k} P, k = 1, …, n + 1 be finite for all t ⩾ 0. If is it possible to find such a λ-dependent operator r^{n,λ} on PB, which is polynomial in λ, and λ-dependent semigroup u^{n,λ}t on PB, whose generator is polynomial in λ, such that P(U^0{t/λ²})^{−1} U^λ_{t/λ²} P = u^{n,λ}_t r^{n,λ} + O(λ^{2n+2}), λ → +0 for all t > 0 ? Let us emphasize that we do not assume here asymptotic behaviour to be uniform in t, it is just assumed for each fixed t > 0. If there are counterexamples, what further restrictions should be assumed to obtain such an asymptotic estimate?

Motivation

The problem concerns perturbative corrections to Markovian quantum master equations and generalization of E. B. Davies’ weak-coupling results. It asks whether finiteness of past interaction integrals suffices for a polynomial preparation and polynomial-generator semigroup approximation on the weak-coupling time scale .

Gap

The problem list keeps Problem 29 open and asks both for counterexamples and for restrictions restoring the estimate. Its first question is refuted by the finite-dimensional instance below; sufficient additional restrictions are not settled by this result. The source’s presentation does not establish novelty outside the list.

Route

Take with the sup norm, , , and

Here uses one-based coordinates. Bounded matrix generators give -semigroups for every real . The free evolution is a group. The relations , , and give a rank-two projection, invariance of both summands, and the source condition .

The interaction-picture coupling is

Consequently and . The inner and outer integrals are

These are Lebesgue integrals, with integrable integrands for every real endpoint, which is stronger than the source’s restriction to . Thus the order-one hypotheses hold. The exact interaction-picture formula is

Projection removes the linear term. The Lean module establishes the projected entry needed for the contradiction; the full displayed matrix identity and the finite-dimensional semigroup correspondence are exact mathematical reasoning.

Falsifier

For each fixed and , the projected entry at satisfies

The inequality follows from for . Every candidate with matrix polynomials is continuous at and hence bounded near zero. An error bounded by cannot reconcile these bounds. The Lean contradiction uses the single fixed time , so no uniformity in is needed.

Operators on embed as matrices supported on the projected subspace. If and , then the full matrix exponential equals the embedded semigroup on times its preparation. Allowing arbitrary coefficient matrices therefore enlarges the class of approximants; refuting this larger class refutes the source’s class as well.

Evidence

The public declarations in D5/S3/Quantum/Semigroups/InteractionPictureAsymptotics.lean are M3, coupling, Hyp, Expansion, claim, and result. The matrices P, D, N, E, the change-of-basis matrices S, T, and supporting lemmas are private.

M3 is Matrix (Fin 3) (Fin 3) ℂ. The matrix norm in the estimate is the entrywise sup norm. coupling D N s is . Hyp P D N asserts , , , integrability of the first projected integrand on , integrability of each second inner integrand on , and integrability of the resulting inner integral as a function of on , for every real .

Expansion P D N asserts that there exist and coefficient families such that for every there exist real with and, for every ,

The degree bound is arbitrary and fixed independently of and ; different polynomial degrees can be padded with zero coefficients. The constants may depend on , and no separate positivity condition is imposed on . The formal order is .

claim is . coupling_formula, projection_algebra, first_integrand, second_integrand, inner_integral, and hypotheses establish the instance’s hypotheses. ST, conjugate, exp_D, and exp_perturbed give the exponential calculation used by projected_entry. entry_norm_le and growth turn that entry into the lower bound . polynomial_continuous and locally_bounded bound the approximant near zero. no_expansion contradicts the error estimate at . The theorem D5.S3.Quantum.Semigroups.InteractionPictureAsymptotics.result has type ¬ claim.

The module’s axiom closure is , with no sorry or additional axiom. Identification of bounded matrices with generators on , invariance of the two summands, and embedding operators on explain the correspondence with the source; the formal predicates are the matrix conditions above.

Triage

What the settlement shows

  1. Proved (Lean) — the counterexample at . The instance satisfies Hyp and admits no Expansion, even with arbitrary matrix polynomial coefficients. Via the finite-dimensional correspondence, the first question of Problem 29 has a negative answer.

  2. Computed (exact mathematical reasoning) — higher orders. Since and , all projected products with three or more interactions vanish. The same instance satisfies the source’s integrability assumptions for every . An error would imply an error for , contradicting the order-one result. This extension is not formalized in the module.

  3. Computed (exact mathematical reasoning) — the mechanism. The free evolution contracts exponentially, while its inverse amplifies the interaction-picture coupling to . Finiteness of past integrals at each fixed endpoint supplies no bound at endpoints . The projected quadratic term diverges at each fixed positive rescaled time.

  4. Open — sufficient restrictions, the second question of Problem 29. Requiring on to be isometric, or uniformly bounded with uniformly bounded inverse for , excludes this example: on that complement and its inverse has norm . Whether either restriction suffices for the desired asymptotic estimate, with the other source hypotheses, is not settled by this result. These are candidate restrictions, not sufficient conditions proved here.

ASSUMED-UNVERIFIED

The connection to Teretenkov’s motivating physics literature (arXiv:2008.02820) and Davies’ weak-coupling literature is limited to titles and abstracts. Their detailed hypotheses, estimates, and applicability to this counterexample are ASSUMED-UNVERIFIED. No theorem from those works is used to establish the matrix refutation.

Whether the observation is known outside the problem list is unverified; no literature priority is established. The quotation binds to arXiv:2410.00416v2, p. 21, Problem 29. The full matrix identity, finite-dimensional source correspondence, and extension are exact mathematical reasoning, rather than additional statements of the Lean module. Sufficiency of the proposed restrictions is not settled by this result.