Alphabeta Math
Pipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Analytic double fibrations and Bolker visibility

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Distributions, conormal kernels, and cotangent relations

Definition

Let M be a smooth n-manifold. A distribution on M is a continuous complex-linear functional on compactly supported smooth densities on M. Its topology is generated locally by the fixed-support seminorms max⁡∣α∣≤msup⁡K∣∂αφ∣, followed by the locally convex test-function topology. In a chart x=(x1,…,xn) a test density is φ(x)∣dx∣; under a coordinate change it transforms by the absolute Jacobian. A distribution is compactly supported when its support, the complement of its largest vanishing open set, is compact.

For a smooth submersion p:Y→M, define the pullback p∗u by transposing fiber integration: in submersion coordinates p(x,v)=x,

⟨p∗u,ψ(x,v)∣dx dv∣⟩=⟨u,(∫ψ(x,v)∣dv∣)∣dx∣⟩.

The absolute density quotient gives the fiber density in other submersion coordinates. For a distributional density V on Y, meaning a continuous functional on compactly supported smooth scalar functions, define its support by the same largest-vanishing-open-set rule. If q:Y→M is smooth and proper on supp⁡V, then for a test function φ on M the set q−1(supp⁡φ)∩supp⁡V is compact. Choose a smooth compact cutoff β equal to one near this set and define the pushforward by

⟨q∗V,φ⟩=⟨V,β(φ∘q)⟩.

The support property makes this independent of β; the cutoff is needed because φ∘q need not be compactly supported on all of Y. A smooth density μ times a distribution u in the test-density convention is the distributional density μu defined by ⟨μu,φ⟩=⟨u,φμ⟩.

Let G,X be smooth manifolds and Z⊆G×X an embedded submanifold whose two projections are submersions. For a smooth density ωZ on Z, assume ambient local finiteness: ∫Z∩Q∣ωZ∣<∞ for every compact Q⊆G×X. This holds, in particular, when Z is closed in G×X. Its incidence delta kernel is the distributional density

⟨KZ,Φ⟩=∫ZΦ∣Z ωZ.

In coordinates (g,x)=(u,t) with Z={t=0}, this is the delta distribution in the t variables paired with the chosen density on Z. The conormal bundle and associated cotangent relation are

N∗Z={(z,ζ)∈T∗(G×X):z∈Z, ζ∣TzZ=0},CZ={(g,η;x,ξ):(g,x;η,−ξ)∈N∗Z∖0}.

Here N∗Z∖0 removes the zero covector, and the minus sign is the distribution-kernel convention for an operator from X to G. Since both projections are submersions, every nonzero conormal in this relation has both η≠0 and ξ≠0. For the analytic terminology, equip G and X with fixed real-analytic atlases compatible with their smooth structures: chart transitions and their inverses have locally convergent real power series. An analytic incidence kernel additionally requires that Z admit real-analytic local defining submersions in these product charts and that ωZ have real-analytic coefficients in the induced analytic charts on Z. This definition covers the incidence kernels used below; it does not assert a general Fourier-integral-operator calculus.

Facts & Assumptions

Given: A smooth manifold M, a submersion p:Y→M, an embedded incidence submanifold Z⊆G×X whose two projections are submersions, and a smooth density on Z satisfying ambient local finiteness. The analytic clause uses the fixed compatible real-analytic structures specified above.

[F1]

Test function space d of an open set: test functions are compactly supported smooth functions.

[F2]

Test function topology: test functions carry the locally convex test-function topology.

[F3]

Distribution: a distribution is a continuous linear functional on test functions.

[F4]

Support of a distribution: support is the complement of the largest vanishing open set; tests supported away from it pair to zero.

[F5]

Density bundle and smooth density fields: a density transforms by the absolute coordinate Jacobian and can be integrated without an orientation.

[F6]

Cotangent space and cotangent bundle as a disjoint union: cotangent vectors are dual tangent vectors and transform by the inverse transpose of the tangent coordinate change.

[F7]

Smooth manifolds and their smooth charts: chart transitions are smooth.

[F8]

Cr and smooth maps between smooth manifolds: smooth maps have smooth coordinate representatives.

[F9]

Compactly supported distributions are tempered: a compactly supported Euclidean distribution has a unique tempered extension.

[F10]

Compactly supported distributions extend to smooth functions: a compactly supported distribution has a unique continuous extension to smooth functions by a cutoff equal to one near its support.

[F11]

Local normal form for submersions: near any point a submersion has coordinates (x,v)↦x.

[F12]

A smooth bump between concentric Euclidean balls: nested coordinate balls admit smooth cutoffs equal to one on the smaller ball and supported in the larger ball.

[F13]

Real analytic germs in several variables: real-analytic scalar and finite-vector germs are represented by locally absolutely convergent real power series.

Proof

Given: The data in the definition.

1.1givenF1F2F3F5F11algebra

In submersion coordinates (x,v), a compactly supported test density on Y is ψ(x,v)∣dx dv∣. Its fiber integral is ψ~(x)=∫ψ(x,v)∣dv∣. The integrand has compact support, so differentiation under the integral gives a smooth function; its support lies in the compact projection of supp⁡ψ. Thus ψ~(x)∣dx∣ is a test density and transposing this operation defines p∗u.

1.2F1F2F4F5F7F8F12givenalgebra

If q is smooth and proper on supp⁡V and K is compact in M, then QK=q−1(K)∩supp⁡V is compact. Choose one smooth cutoff βK equal to one near QK. For every test function φ supported in K, smoothness of q makes βK(φ∘q) smooth with support in the fixed compact set supp⁡βK, so define ⟨q∗V,φ⟩=⟨V,βK(φ∘q)⟩. If another cutoff is used, the difference of the two test functions vanishes on a neighborhood of supp⁡V: it vanishes near QK because both cutoffs equal one there, and at every point of supp⁡V∖QK, continuity of q gives a neighborhood mapped outside the closed set K, where φ∘q=0. Hence [F4] gives the same pairing; choosing a common cutoff for the union of two compact test supports also proves linearity. The chain and product rules bound every fixed-support seminorm of βK(φ∘q) by finitely many fixed-support seminorms of φ, so continuity of V proves continuity of q∗V. A finite cover by coordinate balls and [F12] supplies βK. Multiplication by a smooth density is defined by the stated transpose formula, so the typed pushforward is well-defined.

1.3F2F5F7F8given

For tests supported in a fixed compact Q⊆G×X, ambient local finiteness gives ∣⟨KZ,Φ⟩∣≤sup⁡Q∣Φ∣∫Z∩Q∣ωZ∣. Thus the integral is finite and continuous in the fixed-support test topology. If Z is closed, Z∩Q is compact in Z, and finitely many relatively compact charts bound this integral for every smooth density. In coordinates where Z={t=0}, the functional is integration of the restricted test function against ωZ. Under a change of coordinates on Z, the coefficient transforms by the absolute tangential Jacobian [F5], so the functional is independent of the defining chart.

1.4F6F11givenalgebra

A covector annihilating TzZ transforms by the inverse transpose rule [F6], so N∗Z and CZ are coordinate independent. If a conormal has the form (η,0), it annihilates the image of dπG:T(g,x)Z→TgG, which is all of TgG because πG is a submersion; therefore η=0. Applying the same argument to πX shows that (0,ξ) can only be zero.

1.5F5F13givenalgebra

The analytic conditions are relative to the fixed atlases. On overlaps of induced analytic charts on Z, the nonzero coordinate Jacobian has locally constant sign, so its absolute value is analytic. The density transition rule therefore preserves analyticity of its coefficient. The defining submersions and analytic chart changes specify the same analytic embedded submanifold, while the underlying smooth distribution operations are unchanged.

2.1F5F7F8F11algebrastep 1.1

On overlapping submersion charts, the full absolute Jacobian factors into the base Jacobian and the fiber-density quotient. The fiber integral therefore transforms as a base density. This proves that the transposed functional in step 1.1 is chart independent.

3.1F9F10F12givenalgebrachoose∎

Let φ be any compactly supported test density on M; the zero test is immediate. Its support K is compact. Cover K by finitely many smaller coordinate balls Bi whose closures lie in coordinate balls Ui. Using [F12] in each chart, choose βi supported in Ui and equal to one on Bi, and put σ=∑iβi. Then σ>0 on a neighborhood of K. A second finite cover by coordinate balls and [F12] gives a compactly supported smooth θ in {σ>0} equal to one near K. Define χi=θβi/σ on {σ>0} and extend by zero outside. Each χi is smooth and compactly supported in Ui, and ∑iχi=θ. Hence u(φ)=∑iu(χiφ), since θ=1 near K. Each term is a chartwise pairing with a compactly supported Euclidean distribution, so [F9] and [F10] give its tempered and smooth-function realizations. The finite sum therefore recovers the original functional and its packet pairings, without assuming supp⁡u compact or choosing global coordinates.

LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Finite-order analytic cutoff sequence

Statement

Let n≥1, let U⊂Rn be open, and let K⊂U be compact. There are constants A,C>0 and functions χN∈Cc∞(U) for each integer N≥1 such that 0≤χN≤1, χN=1 on a fixed neighborhood of K, and

∣∂αχN(x)∣≤C(AN)∣α∣(x∈Rn, ∣α∣≤N).

These are smooth compact cutoffs; no compactly supported analytic function is asserted.

Facts & Assumptions

Given: A compact set K contained in an open set U⊂Rn.

[F1]

A smooth bump between concentric Euclidean balls: nested balls admit a smooth function between zero and one, equal to one on the smaller ball and supported in the larger ball.

[F2]

Ck maps and multi-index derivative notation in Euclidean space: ∂α denotes the specified iterated coordinate derivatives, with ∣α∣ their order.

[F3]

Every continuous function on a closed nondegenerate rectangle in Rm is Riemann integrable: every continuous real function on a closed nondegenerate rectangle is Riemann integrable. Thus a continuous compactly supported function, restricted to a rectangle containing its support in the interior, has the finite Euclidean-space integral of The support of a function on Rn and its compactly supported Riemann integral.

[F4]

Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections: for continuous functions on compact product rectangles, iterated integrals equal the product integral.

Proof

Given: The compact set K and open neighborhood U.

1.1givenF1choosealgebra

If K=∅, set χN=0 for all N; the empty set is a neighborhood of K, so every assertion holds. Assume henceforth K≠∅. Consider all pairs of concentric balls Br(x)⋐BR(x)⋐U with x∈K and 0<r<R. Their smaller balls cover K, so compactness supplies finitely many pairs Brj(xj)⋐BRj(xj), 1≤j≤m, whose smaller balls cover K. Choose their finitely many bumps bj by [F1], translated to xj, with 0≤bj≤1, bj=1 on Brj(xj) and compact support in BRj(xj). The smooth function g=1−∏j=1m(1−bj) satisfies 0≤g≤1, equals one on the open set O=⋃j=1mBrj(xj) containing K, and has compact support S⋐U. Only finitely many bumps are selected.

2.1F1F3step 1.1choose

Choose a nonnegative smooth bump ρ0 supported in the unit ball and equal to one on the ball of radius 1/2, using [F1]. Its compactly supported integral is finite by [F3] and positive: a closed nondegenerate rectangle inside B1/2(0) has positive volume and ρ0=1 there. Normalize ρ=ρ0/∫ρ0, so ∫ρ=1, ρ≥0, and supp⁡ρ⊂B‾1(0). Since K⋐O and S⋐U, choose ε>0 smaller than one third of each distance dist⁡(K,Oc) and dist⁡(S,Uc), omitting the second restriction when U=Rn.

3.1F1F3F4step 1.1step 2.1given

For each N≥1, put δ=ε/N, ρδ(x)=δ−nρ(x/δ), and recursively η1=ρδ, ηj+1=ηj∗ρδ for 1≤j<N. Compact-rectangle Fubini [F4] and change of variables give ∫ηN=1 and supp⁡ηN⊂B‾ε(0); [F4] also permits reassociation of these compact convolution integrals. Define χN=g∗ηN. The integral defining χN is over a fixed compact rectangle. Differentiating the smooth kernel under this compact integral is justified by uniform convergence of its difference quotients on that rectangle, so χN is smooth. Positivity and unit mass give 0≤χN≤1. If dist⁡(x,K)<ε, then every y∈supp⁡ηN satisfies dist⁡(x−y,K)<2ε<dist⁡(K,Oc), hence g(x−y)=1 and χN(x)=1. Also supp⁡χN⊂S+B‾ε(0)⋐U.

4.1F2F3F4step 2.1step 3.1algebra

For smooth compactly supported f,h, write ∥h∥1=∫Rn∣h∣. Fubini on a rectangle containing their supports and the triangle inequality give ∥f∗h∥1≤∫ ⁣ ⁣∫∣f(x−y)∣∣h(y)∣ dy dx=∥f∥1∥h∥1. Also ∂j(f∗h)=(∂jf)∗h=f∗(∂jh) by differentiating under the compact integral and integration by parts; there is no boundary term because the factors have compact support. For k=∣α∣≤N, distribute the k coordinate derivatives to k distinct convolution factors in ηN. Scaling gives ∥∂jρδ∥1=δ−1∥∂jρ∥1, so repeated use of the preceding inequality yields ∥∂αηN∥1≤(AN)k,A=ε−1max⁡(1,max⁡j∥∂jρ∥1). For k=0 this is ∥ηN∥1=1.

5.1F1step 1.1step 3.1step 4.1algebra∎

Since ∥g∥∞≤1, ∣∂αχN(x)∣=∣g∗(∂αηN)(x)∣≤∥g∥∞∥∂αηN∥1≤(AN)∣α∣. Thus the lemma holds with C=1 (or any larger fixed constant), uniformly for every ∣α∣≤N. The cutoffs are smooth and no analytic bump is used.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Holomorphic Morse normalization and Gaussian contour

Statement

Let ϕ be holomorphic on a neighborhood of 0∈Cn, with dϕ(0)=0 and complex Hessian H=ϕ′′(0) invertible. There is a local biholomorphic coordinate map w=Ψ(z) with Ψ(0)=0 such that

ϕ(z)=ϕ(0)+12∑j=1nwj2.

Its linear part satisfies (det⁡DΨ(0))2=det⁡H. For a continuous parameter family of invertible Hessians H(p), near any fixed parameter p0 the determinant remains in a disc avoiding 0; choosing one square root at p0 therefore fixes a continuous branch on that neighborhood. If Re⁡H is positive definite, then

∫Rne−λxTHx/2 dx=(2π/λ)n/2(det⁡H)−1/2,λ>0,

with the integral interpreted as an absolutely convergent improper integral and the branch analytically continued from real positive-definite matrices. Finally, deforming a holomorphic contour preserves the integral of a holomorphic top-degree form when the contours are homologous through a region of holomorphy and the swept boundary integrals tend to zero.

Facts & Assumptions

Given: A holomorphic germ ϕ with a critical point at 0 and invertible Hessian.

[F1]

Real analytic germs in several variables: real-analytic germs complexify to holomorphic germs.

[F2]

Multi-indexed power series in Cm and their absolute convergence: the defining series converges absolutely on smaller polydiscs.

[F4]

The holomorphic inverse function theorem in several complex variables: an invertible complex derivative gives a local biholomorphism.

[F5]

A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically: holomorphic functions agreeing on a nonempty open subset of a connected domain agree throughout it.

[F6]

Dominated convergence: pointwise convergence under a common integrable majorant permits passage of limits through integrals.

[F7]

Stokes theorem for smooth singular chains: the integral of a closed differential form over the boundary of a smooth chain is zero.

[F8]
[F9]

The determinant of a triangular matrix is the product of its diagonal entries: the determinant of a triangular matrix is the product of its diagonal entries.

[F11]

Change of variables for an injective C1 map on a compact Jordan set: a C1 diffeomorphism changes compact Jordan integrals by its absolute Jacobian.

[F12]

Every Jordan exhaustion computes a nonnegative improper multiple integral: a compact Jordan exhaustion computes the nonnegative improper integral.

[F13]

The Gaussian integral ∫−∞∞e−x2 dx=π: ∫Re−t2 dt=π, by a proof that adds no choice axiom.

[F14]

Change of variable in an improper integral: a monotone differentiable substitution preserves convergent improper integrals on corresponding truncations.

[F15]

Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections: continuous functions on compact product rectangles have equal product and iterated Riemann integrals.

[F16]

For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries: determinant is a polynomial in the matrix entries, with linear term tr⁡(M) in det⁡(I+tM) at t=0.

Proof

Given: The function ϕ and Hessian H in the statement.

1.1givenF1F3F4algebra

Because H is complex symmetric and invertible, some vector v has vTHv≠0: otherwise polarization would give uTHv=0 for every u,v, contradicting invertibility. Extend v to a basis and use this as a complex linear coordinate change, so H11≠0. From now on, compose each coordinate change with the preceding ones; Ψ denotes the final map from the original coordinates. The holomorphic equation ∂z1ϕ(z1,z′)=0 has a unique holomorphic solution z1=ψ(z′) near 0 by [F3] and [F4], since ∂z1ϕ(0)=0 and ∂z12ϕ(0)=H11≠0.

2.1F1F2F3step 1.1construct

Set t=z1−ψ(z′). Taylor's formula in t, with the linear term zero, gives ϕ(ψ(z′)+t,z′)=ϕ(ψ(z′),z′)+t2a(t,z′),a(t,z′)=∫01(1−s)∂z12ϕ(ψ(z′)+st,z′) ds. The integral is holomorphic by locally uniform convergence of the power series [F2]; a(0,0)=H11/2≠0. Shrink the polydisc so a=a(0,0)(1+b) with ∣b∣<1. The binomial series for (1+b)1/2 converges absolutely by [F2], so w1=t2a(t,z′) is holomorphic and has nonzero t-derivative at 0.

3.1F4step 2.1algebra

By [F4], (t,z′)↦(w1,z′) is biholomorphic near 0, and the phase becomes ϕ(ψ(z′),z′)+w12/2. The Hessian of the reduced phase in z′ is the Schur complement H22−H21H11−1H12. It is invertible because the block determinant formula gives det⁡H=H11det⁡(H22−H21H11−1H12).

3.2F8F9F10F11F12F13F14F15algebrastep 2.1

For real symmetric positive-definite H, [F8] gives H=LL∗ with L lower triangular and positive diagonal. Since H is real, L‾ is another such factorization; uniqueness in [F8] gives L=L‾, so L is real and H=LLT. On each ball BR, the map x↦LTx sends a compact Jordan set to a compact Jordan set; [F11] changes variables by ∣det⁡L∣−1. Letting R→∞ and using [F12] gives the corresponding nonnegative improper-integral equality. Since det⁡L>0, [F9]–[F10] give det⁡H=(det⁡L)2. Repeated compact-rectangle Fubini [F15] factors the standard Gaussian integral on [−R,R]n into one-dimensional integrals, and [F12] lets R→∞. By [F13] and the substitution t=x/2 in [F14], each one-dimensional integral of e−x2/2 is 2π. Finally, z=λw scales the integral by λ−n/2, proving the formula for real positive-definite H with the positive determinant root.

4.1step 3.1inductionalgebragiven

Repeating steps 1.1–2.1 on the reduced phase proves the normal form by induction on n, with the constant phase as the n=0 case. Because Ψ is the composite from the original coordinates, differentiating ϕ(z)=ϕ(0)+12Ψ(z)TΨ(z) twice at 0 gives the original Hessian identity H=(DΨ(0))TDΨ(0); taking determinants gives the asserted square relation. For a continuous parameter family, continuity of det⁡H lets one restrict to a neighborhood whose determinant image lies in a disc avoiding zero, where a square-root branch can be fixed from its base value.

4.2F5F6F10F16step 3.2algebra

For complex symmetric H with positive-definite real part, the Gaussian integral is holomorphic in its entries: on each compact subset of this matrix domain, the integrand and its entry derivatives are bounded by a polynomial times e−c∣x∣2 for some c>0, so [F6] permits differentiation under the integral. This domain is convex, hence connected, and det⁡H≠0 there because Hv=0 would imply Re⁡(v∗Hv)=v∗(Re⁡H)v>0 for v≠0. For Ht=I+t(H−I), [F16] and determinant multiplicativity give ddtdet⁡Ht=(det⁡Ht)tr⁡(Ht−1(H−I)). Thus L(H)=∫01tr⁡(Ht−1(H−I)) dt depends holomorphically on H, satisfies eL(H)=det⁡H, and is zero at I. When H is real positive definite, its segment Ht is real positive definite, so L(H) is real and the branch eL(H)/2 is positive. The real Gaussian formula from step 3.2 and the complex integral formula agree on a real open set of positive-definite matrices. In a polydisc centered at any point of that set, apply the one-variable identity theorem successively in the independent entries of a complex symmetric matrix; then [F5] extends the identity from that polydisc to the connected matrix domain.

5.1F7given∎

The holomorphic n-form in the statement is closed: in complex coordinates its exterior derivative has repeated holomorphic differentials and no antiholomorphic coefficients. The difference of two homologous admissible contours is the boundary of the swept chain. By [F7], its integral is the boundary integral on the truncation of that chain; the stated decay makes this term tend to zero as the truncation expands. Therefore the contour integrals agree.

DefinitionDefinition: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Analytic double-fibration transform and canonical relation

Definition

An analytic double fibration is a diagram of real-analytic manifolds and real-analytic submersions

G← πG Z→ πX X

such that Z is embedded in G×X, both projections are submersions, and

dim⁡G+dim⁡X>dim⁡Z>dim⁡G≥dim⁡X.

Write CZ={(g,η;x,ξ):(g,x;η,−ξ)∈N∗Z∖0} for the incidence cotangent relation. Assume πG is proper on πX−1(K) for every compact K⊂X. Let ωZ be a nowhere vanishing real-analytic smooth density on Z and let κ ⁣:Z→C be real analytic and nowhere zero. For a compactly supported distribution u on X, the weighted transform is the distributional density

Ru=(πG)∗(κ ωZ πX∗u),

where pullback, multiplication by a density, proper pushforward, and CZ use the conventions of the preceding definition. In local fiber coordinates this is integration of u over the incidence fibers with weight κ and density ωZ. The hypotheses on proper support ensure this transform is defined for every compactly supported input. This is the class treated on this page; no noisy-data or stability assertion is included.

Facts & Assumptions

Given: The real-analytic double fibration, its density and nonvanishing analytic weight, and a compactly supported distribution u on X.

[F1]

Distributions, conormal kernels, and cotangent relations: submersion pullback is defined by transposed fiber integration; density multiplication turns it into a distributional density; pushforward is defined when proper on support; the canonical relation uses (η,−ξ).

[F2]

Smooth manifolds and their smooth charts: local charts define the smooth manifold structures.

[F3]

Cr and smooth maps between smooth manifolds: smooth submersions have smooth local coordinate representatives.

[F4]

Density bundle and smooth density fields: densities transform by absolute Jacobians and can be integrated without orientations.

[F5]

Real analytic germs in several variables: the analytic maps and coefficients have holomorphic local complexifications.

[F6]

Multi-indexed power series in Cm and their absolute convergence: those complexifications are represented by convergent power series on smaller polydiscs.

Proof

Given: The manifolds G,Z,X, maps πG,πX, density ωZ, weight κ, and input u.

1.1givenF2F3F5F6

The chart representatives are smooth submersions by [F2]–[F3], and their analytic representatives have local holomorphic extensions by [F5]–[F6]. Hence the fiber and incidence data in the statement are well-defined in the stated smooth and analytic categories.

1.2F1given

The pullback πX∗u exists by [F1]. Multiplying it by the nowhere vanishing analytic density ωZ gives a distributional density; multiplication by the smooth function κ preserves that type. If supp⁡u⊂K with K compact, the support of this product lies in πX−1(K), on which πG is proper by hypothesis.

2.1F1F3F4step 1.1step 1.2∎

The proper pushforward in [F1] therefore defines Ru as a distributional density on G. In coordinates, transposing fiber integration in the two submersions shows that it pairs a data test function with the integral over the corresponding incidence fiber, weighted by κωZ; the density Jacobians cancel by [F4]. The cotangent relation of the kernel is precisely CZ by the sign convention in [F1].

DefinitionDefinition: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Analytic wavefront set by Gaussian FBI packets

Definition

Let u be a distribution, not necessarily compactly supported, or a distributional density (a continuous functional on compactly supported smooth scalar functions), on a real-analytic n-manifold X. Let x0 lie in an analytic coordinate chart and let ξ0∈Tx0∗X∖{0} have coordinate components in that chart. For χ∈Cc∞ supported in the chart and equal to 1 near x0, define the Gaussian FBI packet

Fχu(x,λω)=⟨u(y),χ(y)exp⁡ ⁣(iλ(x−y)⋅ω−λ2∣x−y∣2)⟩,λ≥1,∣ω∣=1.

When u is a scalar distribution, the pairing is with the displayed function times coordinate density ∣dy∣; when u is a distributional density, the pairing is with the displayed scalar function. In both cases λω is the cotangent frequency. The covector (x0,ξ0) is analytically regular for u in this chart if there are such a cutoff χ, a neighborhood U of x0, an open neighborhood Γ of ξ0/∣ξ0∣ in the unit sphere, and constants c,C>0 such that

∣Fχu(x,λω)∣≤Ce−cλ(x∈U, ω∈Γ, λ≥1).

The analytic wavefront set WF⁡A(u) is the set of nonzero cotangent vectors for which this exponential estimate fails. This is a chart-local definition. The separate local FBI-invariance claim needed for a geometric interpretation is stated by the companion lemma.

Facts & Assumptions

Given: A distribution or distributional density u, an analytic chart, a point x0, and a nonzero cotangent vector ξ0.

[F1]

Distributions, conormal kernels, and cotangent relations: distributions act continuously on compactly supported smooth densities; multiplication by the compactly supported cutoff localizes any distribution to the chart.

[F2]

Real analytic germs in several variables: analytic charts have holomorphic complexifications near each point.

[F3]

Multi-indexed power series in Cm and their absolute convergence: the chart complexifications and their derivatives are represented by convergent power series on smaller polydiscs.

Proof

Given: The data in the definition.

1.1givenF1algebra

For fixed x,λ,ω, the function of y in the displayed pairing is smooth and supported in supp⁡χ, hence it is a test density. Therefore the packet is a well-defined complex number by [F1].

1.2givenalgebra

Replacing ξ0 by a positive multiple leaves the unit direction ξ0/∣ξ0∣ unchanged; the definition quantifies over all λ≥1 and an open cone of unit directions. Thus analytic regularity is conic in the cotangent variable, and its complement defines a conic subset of T∗X∖0.

2.1F2F3given∎

By [F2]–[F3], an analytic coordinate change near x0 extends to a holomorphic map on a smaller complex neighborhood, so its cotangent action and Gaussian packet phase are locally defined there. The definition makes no claim that the numeric packet is unchanged under this change; the next lemma proves equivalence for the packet families actually used on this page.

TheoremStatement: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Analytic stationary phase with optimal truncation

Statement

Let n≥1, let U⊂Rn be a bounded open set, let Φ be holomorphic on a complex neighborhood of U‾, and let a∈Cc∞(U) have a holomorphic extension near 0. Assume 0∈supp⁡a, Φ(0)=Φ0, dΦ(0)=0, and dΦ(x)≠0 at every x∈supp⁡a∖{0}. Let H=−iΦ′′(0) be complex symmetric with positive-definite real part. Assume there are r,cquad,d0>0 such that

Im⁡(Φ(x)−Φ0)≥cquad∣x∣2(∣x∣≤r),Im⁡(Φ(x)−Φ0)≥d0(x∈supp⁡a, ∣x∣≥r).

Let χN be the finite-order cutoff sequence equal to one on a fixed neighborhood of 0, with 0≤χN≤1, and supported where these phase hypotheses hold. For every integer N≥1 and every λ≥1, put IN(λ)=∫eiλΦ(x)a(x)χN(x) dx. There are coefficients cj determined by the full Taylor series of the phase and amplitude at 0 and constants C,δ>0, independent of N,λ, such that

IN(λ)=eiλΦ0(2π/λ)n/2(det⁡H)−1/2(∑j=0N−1cjλ−j)+EN(λ), ∣cj∣≤Cj+1j!,∣e−iλΦ0EN(λ)∣≤CN+1N!λ−N−n/2+Ce−δλ.

The square-root branch is fixed by the preceding holomorphic Morse/Gaussian-contour lemma, and c0=a(0). Taking N=⌊ϵλ⌋ for sufficiently small fixed ϵ>0 and sufficiently large λ makes the normalized remainder e−iλΦ0EN(λ)=O(e−δ2λ) for some δ2>0. The expansion includes every coefficient through the stated truncation order; it is not only a leading-term estimate.

Facts & Assumptions

Given: The phase, amplitude, cutoff sequence, stationary point, and positivity hypotheses in the statement.

[F1]

Holomorphic Morse normalization and Gaussian contour: the phase is holomorphically reduced to a nondegenerate quadratic form, the Gaussian determinant branch is fixed, and admissible contours may be deformed when boundary terms vanish.

[F2]

Finite-order analytic cutoff sequence: χN equals one near 0, is supported in U, and has finite-order derivative bounds.

[F3]

Real analytic germs in several variables: analytic phase and amplitude germs extend holomorphically near 0.

[F4]

Multi-indexed power series in Cm and their absolute convergence: convergent Taylor series converge absolutely on smaller polydiscs.

[F5]

Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle: a holomorphic function bounded on a polydisc has Taylor coefficients bounded by its supremum times inverse powers of the polyradius.

[F6]

The Euclidean inverse function theorem: a C1 map with invertible real derivative has a local real C1 inverse.

[F7]

Stokes theorem for smooth singular chains: the integral of a closed differential form over the boundary of a smooth chain is zero.

Proof

Given: The data in the statement.

1.1givenF2choose

Choose r>0 so that χN=1 on B2r(0) for every N, the phase and amplitude are holomorphic near B‾2r(0), and the stated positivity holds. The positive-phase hypothesis and compactness of supp⁡a∖Br(0) give Im⁡(Φ−Φ0)≥d>0 there. Since a is bounded and χN is bounded by one, the absolute value of that contribution after multiplication by e−iλΦ0 is at most ∥a∥∞∣U∣e−λd, uniformly in N. Thus only the integral over the fixed local ball affects the power series; the complement contributes O(e−dλ).

2.1F1F3F4F5step 1.1

Put ϕ=−i(Φ−Φ0), so Re⁡ϕ=Im⁡(Φ−Φ0) and ϕ′′(0)=H. Apply [F1] to obtain a holomorphic Morse coordinate w=Ψ(x) with ϕ(x)=12w⋅w. The transformed real ball is a local contour Γ through 0. The transformed amplitude b(w)=a(Ψ−1(w))det⁡DΨ−1(w) is holomorphic in a fixed polydisc and has coefficients bounded by MR−∣α∣ for some M,R>0 by [F3]–[F5].

3.1F1F6F7step 2.1given

Differentiating the Morse identity in [F1] twice at 0 gives ATA=H, where A=DΨ(0). Taylor's formula gives Re⁡(ϕ(tv))=12t2vT(Re⁡H)v+o(t2); comparing with Re⁡ϕ(tv)≥ct2∣v∣2 and dividing by t2/2 as t→0 yields vT(Re⁡H)v≥2c∣v∣2. For a real vector v, write Av=u+iw with u,w∈Rn. Then ∣u∣2−∣w∣2=Re⁡(vTHv)>0 when v≠0. In particular, the real projection on ARn is injective, hence bijective by dimension, and ARn={u+iKu:u∈Rn} for a real linear map K. For nonzero u, applying the strict inequality to v=A−1(u+iKu) gives ∣Ku∣<∣u∣; compactness of the unit sphere gives ∥K∥<1. The real inverse theorem [F6] makes the nonlinear contour Γ a graph u+i(Ku+r(u)), with r(u)=O(∣u∣2). For sufficiently small r0, the homotopy graphs u+i(Ku+tr(u)) remain in the holomorphic chart and satisfy Re⁡(w⋅w)≥ccontour∣u∣2 for ∣u∣≤r0, because the linear margin ∣u∣2−∣Ku∣2≥(1−∥K∥2)∣u∣2 dominates the O(∣u∣3) error. The homotopy u+itKu, 0≤t≤1, also has Re⁡(w⋅w)=∣u∣2−t2∣Ku∣2≥(1−∥K∥2)∣u∣2. On the fixed outer boundary these bounds, together with boundedness of the transformed amplitude and Jacobian, make the integrals O(e−c1λ). [F7] and the contour statement in [F1] therefore deform Γ to the real Gaussian contour, with only that exponential boundary term.

3.2F1F5step 1.1step 2.1algebra

Truncate the Taylor series after total degrees below 2N. On a smaller ball ∣w∣≤r0<R, the Cauchy bound [F5] and a geometric-series estimate give ∣b(w)−∑∣α∣<2Nbαwα∣≤C2N+1∣w∣2N. Integrating this remainder against e−λ∣w∣2/2 and using z=λ w bounds it by C3N+1λ−N−n/2∫Rn∣z∣2Ne−∣z∣2/2 dz≤C4N+1N!λ−N−n/2. For the last inequality, convexity gives (∑j=1nzj2)N≤nN−1∑j=1n∣zj∣2N. Fubini factors each summand into one-dimensional Gaussian moments; integration by parts gives MN=(2N−1)MN−1 with M0=2π, since the polynomial times Gaussian boundary term tends to zero. Hence MN=(2N−1)!!2π≤2NN!2π, and the displayed integral is at most (2n)N(2π)n/2N!. Absorb this fixed-dimensional factor into C4N+1. The extension of the Taylor polynomial P<2N(w)=∑∣α∣<2Nbαwα from ∣w∣≤r0 to the full real Gaussian integral needs a separate estimate uniform in N. For ∣w∣≥r0 and k<2N, ∣w∣k≤r0k−2N∣w∣2N. Cauchy's coefficient bound and the at most exponential count of degree-k multi-indices give DN:=∑k<2N∑∣α∣=k∣bα∣r0k−2N≤C5N+1, since r0,R are fixed positive constants and the sum has 2N terms after grouping degrees. Consequently ∫∣w∣≥r0∣P<2N(w)∣e−λ∣w∣2/2 dw≤C5N+1λ−N−n/2∫Rn∣z∣2Ne−∣z∣2/2 dz≤C6N+1N!λ−N−n/2. Thus the polynomial extension tail is controlled by the factorial remainder for every N, rather than by an exponential constant independent of N. The actual amplitude away from the local critical region and the contour boundary still have the exponential estimates from step 1.1 and [F1]; no extension of that amplitude outside its holomorphy neighborhood is used. Combining these estimates proves the stated normalized error for every N.

4.1F1F3F5step 2.1step 3.1algebra

Expand b(w)=∑αbαwα and group by total degree. Odd monomials integrate to zero over Rn because the Gaussian and domain are invariant under w↦−w. Each monomial of degree 2j contributes a constant times λ−n/2−j by the change of variables z=λ w. In one dimension, integration by parts gives Ik=∫t2ke−t2/2dt=(2k−1)Ik−1 and I0=2π, hence Ik=(2k−1)!!2π. Products give the n-dimensional moments. If α=2k and ∣k∣=j, then ∏l(2kl−1)!!≤(2j−1)!!≤2jj!; all monomials with an odd coordinate vanish. After scaling, every degree-2j moment is therefore at most C0j+1j!λ−j. The number of degree-2j multi-indices is at most Cnj+1 and ∣bα∣≤MR−2j, so the coefficient of λ−j is bounded by C1j+1j!. The Jacobian at zero contributes (det⁡H)−1/2 on the chosen branch, and the degree-zero coefficient is a(0).

5.1step 3.2algebra∎

For N=⌊ϵλ⌋ and sufficiently large λ so that N≥ϵλ/2≥1, the factorial term is at most CN+1λ−n/2(N/λ)N because N!≤NN. Choose ϵ>0 with Cϵ<1/2. Since N≤ϵλ, the displayed term is at most CN+1λ−n/2ϵN, which is bounded by C′e−δ2λ because N≥ϵλ/2 and 2−N≤e−(ϵlog⁡2)λ/2. Combining this with the exponential term in step 3.2 proves optimal truncation of the normalized remainder at order proportional to λ, with all stationary-phase coefficients retained. For the absolute remainder multiply this bound by ∣eiλΦ0∣=e−λIm⁡Φ0; no sign restriction on Im⁡Φ0 is imposed.

DefinitionDefinition: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Bolker condition for a double-fibration transform

Definition

For an analytic double fibration with incidence cotangent relation CZ⊂(T∗G∖0)×(T∗X∖0), let

πL:CZ⟶T∗G∖0,πL(g,η;x,ξ)=(g,η).

The double fibration satisfies the global Bolker condition if πL is an injective immersion. The Bolker condition holds at a specified point c=(g,η;x,ξ)∈CZ if the full fiber over its data covector is the singleton πL−1(g,η)={c} and dπL∣c is injective. Thus the pointwise condition has both a fiber-uniqueness clause, which excludes every other relation point over the same data covector even outside a chosen chart, and a local differential-rank clause.

Facts & Assumptions

Given: An analytic double fibration and its incidence relation CZ.

[F1]

Analytic double-fibration transform and canonical relation: both incidence projections are analytic submersions and CZ is the relation of the transform.

[F2]

Distributions, conormal kernels, and cotangent relations: CZ consists of nonzero conormals with sign convention (η,−ξ) and is independent of coordinates.

Proof

Given: The incidence relation from [F2].

1.1F1F2algebra

The relation is a smooth conic submanifold in local incidence coordinates: the conormal equations are smooth constant-rank linear equations in the covector variables, and the zero section is removed. Thus projection onto its first cotangent factor is a well-defined smooth map.

2.1F2∎

Global injectivity means that every data covector has at most one object covector paired with it; at a specified point c, the corresponding fiber condition is exactly πL−1(πL(c))={c}. Injectivity of the differential means that every tangent vector to CZ mapped to zero is itself zero. Both conditions are invariant under coordinate changes because [F2] makes CZ coordinate independent and cotangent coordinate changes are diffeomorphisms. This proves the two clauses in the definition.

LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Incidence-coordinate conormal kernel and canonical relation

Statement

Let Z⊆G×X be an embedded incidence submanifold of codimension k>0, and let (g0,x0)∈Z. Choose coordinates near this point and a submersion F:G×X→Rk with Z={F=0}. Write F=(F1,…,Fk). For every τ∈Rk∖{0}, the conormal covector at (g,x)∈Z is

(g,x;DgF(g,x)Tτ, DxF(g,x)Tτ).

Consequently the incidence kernel has local delta representation b(g,x)δ(F(g,x))∣dg dx∣, with a smooth density coefficient b, and its cotangent relation consists exactly of

(g,DgFTτ; x,−DxFTτ),(g,x)∈Z,τ≠0.

No general Fourier-integral-operator composition calculus is used.

Facts & Assumptions

Given: The incidence submanifold Z, its two submersions, and a local defining submersion F of codimension k.

[F1]

Distributions, conormal kernels, and cotangent relations: the kernel is integration on Z against a smooth density, and the relation pairs conormal (η,−ξ).

[F2]

Analytic double-fibration transform and canonical relation: Z is embedded and both projections are submersions.

[F3]

Local normal form for submersions: a submersion is locally equivalent to coordinate projection.

[F4]

Density bundle and smooth density fields: density coefficients transform by absolute Jacobians.

Proof

Given: The data in the statement.

1.1F2F3algebra

Since F is a submersion, its differential has rank k. The tangent space of its zero level is T(g,x)Z=ker⁡DF(g,x). In finite-dimensional linear algebra, the annihilator of the kernel of a rank-k linear map is the image of its transpose: inclusion follows from τTDFv=0 for v∈ker⁡DF, and both spaces have dimension k. Hence every conormal is uniquely DFTτ=(DgFTτ,DxFTτ).

1.2F1F3F4algebra

By [F1], the incidence functional is integration of a test function against a smooth density on Z. Complete F to submersion coordinates (s,t) with t=F(g,x), using [F3]. In these coordinates its action is ∫t=0Φ(s,0)c(s)∣ds∣ for a smooth coefficient c. Rewriting the ambient density as ∣dg dx∣ and applying the ordinary change-of-variables rule gives b(g,x)δ(F(g,x))∣dg dx∣ for a smooth b; the Jacobian factor is nonzero because the coordinate map is a diffeomorphism.

2.1F1step 1.1algebra∎

The cotangent relation uses the conormal (η,−ξ) by [F1]. Substituting the formula from step 1.1 gives η=DgFTτ and −ξ=DxFTτ, so ξ=−DxFTτ. Since DFT is injective, τ≠0 gives a nonzero conormal. This proves the displayed relation, with every sign fixed by the kernel convention.

LemmaStatement: AI-adaptedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Local analytic elliptic packet reconstruction

Statement

Work near (q0,p0)∈Rn×(Rn∖0). A normalized positive analytic packet phase is a holomorphic function ϕ(y,q,p) on a fixed complex neighborhood of the indicated real variables, such that, for real arguments,

ϕ(q,q,p)=0,∂yϕ(q,q,p)=−p,Im⁡ϕ(y,q,p)≥c∣y−q∣2

for some c>0. A classical analytic amplitude is realized on each smaller complex neighborhood by

a(y,q,p;λ)=∑j<ϵλaj(y,q,p)λ−j,sup⁡∣aj∣≤Cj+1j!,

with sufficiently small fixed ϵ>0. Changing ϵ to a smaller positive number changes the realization by an exponentially small function on a smaller neighborhood. An elliptic amplitude has a0(q0,q0,p0)≠0.

For a distribution u localized to a sufficiently small fixed compact neighborhood of q0, the uniform exponential decay of

⟨u(y),a(y,q,p;λ)eiλϕ(y,q,p)⟩

for (q,p) in a neighborhood of (q0,p0) is independent of the normalized positive phase and elliptic classical analytic amplitude. Smooth fixed cutoffs equal to one near the packet centers are understood. This criterion agrees with the Gaussian criterion with unit directions and arbitrary λ≥1.

More precisely, after shrinking the parameter neighborhood W, every other such packet vβ with β in a smaller W0⋐W has a representation

vβ(y;λ)=∫Wa(y,α;λ)eiλϕ(y,α)K(β,α;λ) dα+Rβ(y;λ),

where ∣K∣≤CλL and ∥Rβ∥Cm≤Cme−cmλ on the fixed localization compact, for every fixed m. There is a representation in the reverse direction as well. All estimates are uniform on the stated smaller neighborhoods. Thus the inverse is an actual local operator modulo exponentially small errors, rather than just a formal inverse series.

Facts & Assumptions

Given: The phase, amplitude and nested compact neighborhoods in the statement. All holomorphic functions used below are restricted to smaller fixed neighborhoods before a constant is chosen.

[F1]

Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle bounds derivatives of a holomorphic function on a smaller polydisc by its supremum times α!r−∣α∣.

[F2]

Holomorphic Morse normalization and Gaussian contour gives local quadratic coordinates, Gaussian integrals and Stokes deformation with controlled boundary.

[F3]

Analytic stationary phase with optimal truncation gives factorial expansion and normalized exponential remainder after truncation proportional to λ.

[F4]

Finite-order analytic cutoff sequence supplies compact smooth localizers with derivatives through order N bounded by C(CN)∣α∣.

[F6]

Stokes theorem for smooth singular chains permits deformation of holomorphic integral kernels on truncated contours.

[F7]

Compactly supported distributions are tempered and continuity on a fixed support give a finite derivative order for every distributional pairing below.

[F8]

External input — specified analytic contour operator. Sjöstrand, Singularités analytiques microlocales, Astérisque 95 (1982), §4, printed pp. 23–24, equations (4.1)–(4.4), defines the operator on weighted holomorphic germs Hρ,x0, with analytic amplitude near (x0,x0,ξ0) and ξ0=(2/i)∂xρ(x0). Its real 2n-cycle is Γ(x)={(y,θ):θ=(2/i)∂xρ(x)+iRx−y‾, ∣x−y∣≤r}, with R sufficiently large and r sufficiently small. Integrate the holomorphic volume form dy∧dθ, with orientation chosen so its pullback is (2R)ndL(y), and prefactor (2πh)−n. The resulting kernel has Gaussian bound with loss (R−C)∣x−y∣2/h. Changing admissible radii/contours changes the germ only by an exponentially smaller weighted germ; amplitude 1 gives the identity in that sense. This is an external contour/operator theorem, not an inference from formal symbols alone.

[F9]

External input — actual analytic composition and elliptic inverse. The same source, Theorem 1.5 (printed p. 8), Theorem 4.2 (pp. 27–28), Remark 4.3 (p. 28) and Theorem 4.5 (pp. 31–32), supplies the analytic classical inverse symbol, actual operator composition with the usual reduced-symbol formula, nonstandard holomorphic-phase changes with invertible mixed derivative, and two-sided elliptic inverse on the corresponding weighted holomorphic germs. Analytic symbols and their equivalence are those of §1 (pp. 2–5): factorial coefficient bounds, truncation proportional to h−1, and equality modulo an exponentially smaller germ. These are imported results; the formal algebra below identifies their application but is not claimed to independently reconstruct this contour calculus.

[F10]

External input — real realization and packet transition. The same source, §5, equations (5.8)–(5.10) (printed pp. 33–35), its packet-action lemma (pp. 35–36), Theorem 5.3 (pp. 36–37), and Proposition 6.2 with equations (6.3)–(6.5) (p. 38), realizes positive analytic kernels on real variables with nested compact parameter domains and smooth spatial cutoffs. “Negligible” here means that ec/h times the error kernel is bounded in C∞ for some c>0 (definition on p. 34); in particular every fixed derivative is exponentially small on the smaller fixed compact. Classical analytic ellipticity gives the actual bidirectional packet superposition of (6.3)–(6.4), with transition kernel polynomially bounded in h−1, uniformly on the smaller packet-parameter neighborhood. The source normalization is ∂yϕ=αξ; our phases are its specialization α=(q,−p), with absolute parameter Jacobian 1. These real realization and packet-transition results are explicitly imported. They assert no global real-variable inverse outside the nested microlocal packet neighborhoods.

Proof

Given: The data in the statement; put h=λ−1. Complex conjugation of the coefficients of a holomorphic germ is denoted by a star: ϕ∗(z,α)=ϕ(zˉ,αˉ)‾.

1.1F1algebraconstruct

We retain the formal inverse algebra needed to identify the external operator construction [F9]. For a formal holomorphic symbol p=∑j≥0hjpj(x,ξ), with ∣pj∣≤Cj+1j! on a fixed polydisc, define p#q=∑j,k,γhj+k+∣γ∣i∣γ∣γ!(∂ξγpj)(∂xγqk). There are finitely many terms in each degree. Associativity follows directly by applying the product rule to the two triple products: splitting a multi-index γ=μ+ν contributes γ!/(μ!ν!), which cancels its denominator and leaves identical terms. The map p↦P=p(x,ξ+hDx), with Dx=∂x/i, respects this product; expansion by the product rule gives the displayed formula.

1.2F1F8F10algebraconstruct

The actual contour realization is [F8], with ρ=−Im⁡S and h=λ−1. In fixed-offset coordinates y=x+w, its oriented volume and prefactor give the explicit formula

Ahv(x)=(Rπh)n∫∣w∣≤rexp⁡(−iw⋅Sx(x)−R∣w∣2h)p(x,x+w,Sx(x)−iRw‾;h)v(x+w;h) dL(w).

Here dL is Euclidean 2n-dimensional measure, the phase-space cycle and its orientation are exactly those of [F8], and R,r are fixed within the common holomorphy neighborhood. The Gaussian bound and amplitude-1 identity are the specified operator theorem [F8]; equivalently, for amplitude 1 the holomorphic factor e−iw⋅Sx(x)/hv(x+w;h) has constant Taylor coefficient v(x;h) and all positive-degree holomorphic monomials have zero angular integral. The remaining Gaussian tail is exponentially small in the weighted germ. For this pluriharmonic weight the fixed-offset formula is holomorphic in x; it also specifies precisely the previously implicit cycle and measure. The fixed-derivative real-localization bounds used later are [F10], rather than an assertion obtained solely from this formal identity.

2.1F1step 1.1algebra

Here are estimates for this formal algebra that also control its inverse. Use nested complex x neighborhoods Ωt, 0<t<t0<1, whose boundary separation is at least t−s, and keep ξ in a smaller fixed polydisc. Write P=∑hkPk, where Pk has differential order at most k. Cauchy's inequality, first in the fixed ξ polydisc and then in x, gives ∥Pk∥t,s≤Ck+1kk(t−s)−k,0<s<t<t0. Indeed a term with j+∣γ∣=k costs at most Ck+1j!γ!(t−s)−∣γ∣; j!γ!≤k!≤kk, t−s<1, and the number of terms is at most exponential in k. For k=0 use 00=1. Let fk(P) be the least admissible constant in ∥Pk∥t,s≤fk(P)kk(t−s)−k. If R=PQ, choose the intermediate radius with r−s=j(t−s)/(j+k) for the term PjQk. Then fℓ(PQ)≤∑j+k=ℓfj(P)fk(Q). The endpoint cases use the same estimate without an intermediate loss. Consequently ∥P∥ρ=∑ρkfk(P) is submultiplicative whenever finite. Conversely pk=Pk1, evaluated with a fixed radius loss, satisfies ∣pk∣≤Ck+1kk≤(eC)k+1k!; the last inequality follows by integrating log⁡t from 1 to k. These estimates are on one fixed smaller neighborhood, independent of k.

3.1F1step 1.1step 2.1algebraconstruct

If p0≠0, shrink so 1/p0 is bounded holomorphic. The formal product p#(1/p0)=1−r has r0=0 and finite ∥r∥ρ for small ρ by step 2.1; decreasing ρ makes this norm less than 1/2. Thus q=(1/p0)#∑ℓ≥0r#ℓ has finite norm, because in each degree its defining sum is finite and the geometric norm sum is at most 2. It follows that qj have factorial bounds on a fixed smaller neighborhood. This gives a right inverse. The identical construction on the other side gives a left inverse; associativity shows they agree. Truncating at j<ϵ/h realizes these symbols. A term with index j has modulus at most C(Chj)j; for j≤ϵ/h and Cϵ<1/2 it is at most C2−j. Two admissible truncations therefore differ by O(e−c/h), also in every fixed derivative by [F1].

4.1F1F2F3F6F9F10step 1.1step 2.1step 3.1step 1.2algebra

The actual composition and inverse statements invoked here are the external results [F9]–[F10]. The following calculation identifies their specialization and symbol; it is not an independent reconstruction of that analytic contour calculus. Products of these kernels are actual iterated contour integrals. All weights needed here are of this form, with S the packet phase and its holomorphic critical value; thus the saddle phases used for contour comparison are holomorphic. Their composed contour is good: if the inner integration has loss c∣y−y(z)∣2 and the outer one loss c∣z−z(x)∣2, their sum controls the square distance from the combined critical point, since the critical-point maps have bounded derivatives. The holomorphic Morse coordinates [F2] identify this contour and the contour obtained by doing the integrations in the other order with graphs over a common negative-definite real subspace. Such graphs have slope less than one after a linear scaling; their straight interpolation has the same positive quadratic margin on a smaller ball. Stokes therefore changes the order and reduces the composition, with exponentially small boundary errors. Taylor expansion in y−x, followed by integration by parts in θ, gives the full symbol pred(x,ξ;h)∼∑γh∣γ∣i∣γ∣γ!∂ξγ∂yγp(x,y,ξ;h)∣y=x. For a product this is exactly the # formula in step 1.1. To estimate rather than just manipulate this expansion, apply [F3] on the good contour after its quadratic normalization. Cauchy bounds for the analytic amplitudes give CN+1N!hN for the remainder after total degree N; each of the finitely many symbol indices contributes the convolution estimates in step 2.1. Taking N=⌊ϵ/h⌋ makes this O(e−c/h). The actual operator consequences are supplied by [F9]–[F10]: a zero reduced symbol acts by an exponentially small operator, and the inverse symbol of step 3.1 gives an actual two-sided inverse modulo such errors. Fixed-contour local remainders and symbols are holomorphic in x by the fixed-offset representation in step 1.2, so Cauchy on a further smaller neighborhood controls their fixed derivatives. Errors involving smooth spatial cutoffs or moving outer boundaries are instead differentiated by the chain rule under the fixed-parameter boundary integrals. Each of their fixed m derivatives costs at most Cmh−Mm, or an additional fixed power of N for a finite-order localizer with N proportional to h−1. The boundary has a fixed positive phase margin, so these polynomial losses are absorbed by reducing that margin. No Cauchy estimate is applied to a merely smooth cutoff error.

5.1F5step 1.2step 4.1algebra

The same calculation permits a nonstandard holomorphic phase S(x,y,θ) with S(x,x,θ)=0 and invertible mixed derivative Sxθ at the diagonal. Indeed S(x,y,θ)=(x−y)⋅Θ(x,y,θ),Θ=∫01Sx(y+t(x−y),y,θ) dt. By [F5], θ↦Θ is a local biholomorphism. The change of variable, including its holomorphic Jacobian, gives the standard kernel of step 1.2. A good contour for one kernel is good for the other because the exponent is identical. Ellipticity is preserved by the nonzero Jacobian. Hence the composition and inverse theorems [F9], with the symbol identification above, hold for these phases too.

6.1F2F3F9step 3.1step 1.2step 4.1step 5.1algebraconstruct

For the given positive phase form the kernel A(x,y;h)=h−3n/2∫ei(ϕ(x,q,p)−ϕ∗(y,q,p))/ha(x,q,p;h) dq dp. Locally this is a kernel of the type just constructed. To see this, first integrate in q by analytic stationary phase. At x=y=q the q derivative vanishes, and the imaginary part of its Hessian is positive definite because Im⁡ϕ(x,q,p)+Im⁡ϕ(y,q,p)≥c(∣x−q∣2+∣y−q∣2). Its critical value S(x,y,p) is zero at x=y, and Sx(x,x,p)=−p. Thus Sxp=−I there. The resulting kernel has prefactor h−n and a classical analytic amplitude whose leading term is a nonzero Gaussian determinant times a0(x,x,p). It is elliptic. The actual elliptic inverse theorem [F9], with the phase and symbol identified in steps 1.2, 3.1, 4.1 and 5.1, gives an analytic operator B with AB=BA=I modulo exponential errors on the appropriate holomorphic germs.

7.1F1F2F4F5F6F10step 4.1step 6.1algebra

Real realization, nested-domain composition, and all fixed-derivative localization bounds are the external input [F10]. We identify its hypotheses here, preserving the local contour and cutoff calculations. Restrict (q,p) to W and insert a fixed smooth spatial cutoff equal to one near x=y=q. Away from this diagonal, positivity supplies Im⁡(ϕ(x,α)−ϕ∗(y,α))≥d>0 on the cutoff transition. When the kernel acts on a holomorphic packet vβ(y)=t(y,β;h)eiψ(y,β)/h, the total phase has its unique nearby critical point at y=q=x, p=pβ when x=qβ. In a small neighborhood it satisfies the stronger contour estimate Im⁡Stotal≥c(∣x−q∣2+∣y−q∣2+∣p−pβ∣2) after deforming y by y↦y+iδ∂yStotal‾ near the diagonal. Here Taylor's formula gives an added δ∣∂yStotal∣2+O(δ2∣∂yStotal∣2); ∂yStotal=p−pβ+O(∣x−q∣+∣y−q∣), so sufficiently small δ proves the estimate. For complex x nearby continue the critical point by [F5] and use the quadratic coordinates to deform a further O(∣x−qβ∣), leaving the outer boundary fixed. The good-contour estimates of step 4.1 then apply uniformly. On the spatial cutoff transition the original positive margin persists; on ∂W, for β∈W0, the displayed estimate supplies a fixed margin. Every swept boundary integral is consequently O(e−c/h). For a fixed number of derivatives, its smoothly parameterized compact boundary, cutoff and phase contribute only fixed powers of h−1 and, for finite-order localizers, of N. Those powers are absorbed into a smaller exponential margin. Holomorphic fixed-domain contour remainders separately have the Cauchy derivative bounds of step 4.1. If finite-order localization is needed in an integration by parts, [F4] with N=⌊ϵ/h⌋ gives a factor at most (ChN)N on the nonstationary part; choose Cϵ<1/2. This verifies the real realization of the compositions and of the identity on each such packet.

8.1F7F9F10step 1.2step 4.1step 6.1step 7.1algebra

The packet-action lemma, Theorem 5.3 and Proposition 6.2 in [F10] supply the actual realization of this step. Applying B to vβ gives eiψ(y,β)/hb(y,β;h) modulo exponential errors, where b is a classical analytic amplitude bounded by a fixed power of h−1. This follows from the same composition calculation, treating β as a parameter and taking the weight ρ=−Im⁡ψ in step 1.2; the combined critical point is the diagonal, and steps 4.1 and 7.1 give the factorial remainder on smaller fixed neighborhoods. Therefore ABvβ=vβ+Rβ, and its realized real-variable expression is the representation in the statement with K(β,α;h)=h−3n/2∫ei(ψ(y,β)−ϕ∗(y,α))/hb(y,β;h) dy. The imaginary part of this exponent is at least c(∣y−qβ∣2+∣y−qα∣2) for real parameters, so the compact integral is bounded by a power of h−1, uniformly in α∈W, β∈W0. Errors and cutoff transitions retain the derivative bounds of step 7.1. Pairing the representation with u is legitimate by [F7]; its finite-order seminorm bound makes ⟨u,Rβ⟩ exponential. The integral of a uniformly exponentially small source transform times the polynomially bounded K is exponential too. Interchange the two elliptic packet families to obtain the reverse implication.

9.1step 8.1algebra∎

Finally use the reference phase ϕG(y,q,p)=(q−y)⋅p+i∣p∣2∣q−y∣2. It is holomorphic on a complex neighborhood of any nonzero real p0, choosing the branch of p⋅p positive there. Its packet with parameter λ is exactly the unit-direction Gaussian packet with frequency parameter λ∣p∣ and direction p/∣p∣. On a fixed small parameter neighborhood ∣p∣ is bounded above and below by positive constants, so the exponential criteria agree; bounded frequencies are absorbed into the constant. All amplitude and inverse constructions above involve finite sums or a uniquely determined formal recursion and its finite truncation. No choice axiom is used.

External source qualification and reading limits

The analytic operator/contour, composition, elliptic inversion and packet-transition assertions in [F8]–[F10] are imported established theorems under the run's external-source policy. The remaining finite algebra, normalization, localization and distributional pairing calculations above are retained. No global inverse on arbitrary real-variable functions, no uniform estimate outside the smaller parameter sets, and no reconstruction of the full analytic microlocal calculus is asserted.

For this repair the actual 169-page Numdam PDF was retrieved. Theorem 1.5 on printed p. 8, §4 on pp. 23–32, §5 on pp. 32–37, and Definition 6.1/Proposition 6.2 on pp. 37–38 were inspected in the primary text; the integration-cycle/measure formulas on p. 23, real realization and C∞ error definition on p. 34, and packet transition on p. 38 were also checked in rendered page images. This is the actual relevant source reading, not a claim to have read or audited all 169 pages, all earlier historical source references, or every foundation used by Sjöstrand.

LemmaStatement: AI-adaptedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Analytic incidence localization away from a data cotangent fiber

Statement

Let R be an analytic double-fibration transform and u∈E′(X) with support K. Fix a nonzero data covector (z0,ζ0). Suppose there is no relation point (z0,ζ0;x,ξ)∈CZ with x∈K. Then (z0,ζ0)∉WF⁡A(Ru). More precisely, the transpose of a data Gaussian packet, localized near z0, is exponentially small with every fixed number of object derivatives on a neighborhood of K, uniformly for data centers and directions near (z0,ζ0/∣ζ0∣).

Facts & Assumptions

Given: The transform, support compact, covector and empty relation fiber in the statement.

[F1]

Analytic double-fibration transform and canonical relation gives analytic submersions and properness over compact object supports.

[F2]

Distributions, conormal kernels, and cotangent relations identifies conormals and supplies fixed-support finite derivative bounds for distributions.

[F3]

Finite-order analytic cutoff sequence gives finite-order localizers.

[F4]

Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle gives factorial bounds for all derivatives of the analytic fiber maps, density coefficients and reciprocals of nonzero analytic phase derivatives on smaller neighborhoods.

[F5]

Real analytic inverse and implicit functions gives analytic local fiber coordinates.

Proof

Given: The data in the statement.

1.1F1F2F5givenalgebra

If K=∅, then u=0 and the conclusion is immediate; assume K≠∅. Fix a relatively compact data chart V0 about z0 and a compact object neighborhood K2 with K⊂int⁡K2. By [F1], the incidence portion over V‾0 and K2 is compact. The portion of CZ over it with unit data covector is compact as well. Indeed, at each incidence point the projection of its conormal fiber (η,−ξ)↦η is injective: if η=0, then −ξ annihilates the image of dπX, which is all of TxX by [F1], so ξ=0. On the compact incidence portion these injective linear maps have a uniform lower bound in fixed local metrics. Thus ∣η∣=1 bounds ξ, and closedness of the normalized relation gives compactness. Write ω0=ζ0/∣ζ0∣ in the data chart. If no product neighborhood of (z0,ω0,K) were disjoint from the normalized relation, there would be relation points with data bases tending to z0, unit data covectors tending to ω0, and object bases tending to K. Compactness would give a limiting relation point over (z0,ω0) and some x∈K, contradicting the hypothesis after rescaling by ∣ζ0∣. Hence there are neighborhoods V⋐V0, Γ⊂Sdim⁡G−1 of ω0, and an open neighborhood O of K, with O‾⊂int⁡K2, such that no relation point lies over (q,ω,x) for q∈V, ω∈Γ, and x∈O. Choose a compact neighborhood K1 with K⊂int⁡K1⊂K1⊂O. The incidence portion over V‾ and K1 is compact by [F1]. Use [F5] to cover it by finitely many analytic fiber charts for the projection to X, written (t,x)↦(z(t,x),x). In these coordinates the transpose data packet has integrals of the form ∫eiλΨ(t,x;q,ω)b(t,x)χ(z(t,x)) dt,Ψ=(q−z(t,x))⋅ω+i2∣q−z(t,x)∣2, where b is analytic and χ is a data cutoff. At incidence points z(t,x)=q, ∂tΨ=−DtzTω. If this vanished in every fiber direction, then ω would annihilate the vertical tangent of πX and extend to a nonzero conormal (ω,−ξ) of Z; the submersion hypotheses ensure both components are nonzero. This would be a relation point over (q,ω,x), excluded by the neighborhoods just chosen.

2.1F1F4step 1.1choose

On the compact incidence portion over V‾ and K1, the no-relation property from step 1.1 gives a positive lower bound for max⁡j∣∂tjΨ∣ when z=q and (q,ω) ranges over smaller compactly contained neighborhoods of (z0,ω0). By continuity, shrink the data chart, direction neighborhood and fiber charts so this lower bound persists whenever ∣z−q∣ is sufficiently small. A finite refinement therefore gives the uniform alternative on each piece, for x in a neighborhood of K and (q,ω) near the supplied data point: either ∣z−q∣≥d>0, or one fiber coordinate satisfies ∣∂tjΨ∣≥d>0. The first pieces have Gaussian exponential decay in every fixed object derivative. For the second pieces shrink the analytic neighborhoods so 1/∂tjΨ is holomorphic and has uniform factorial derivative bounds by [F4]. The data cutoff can be chosen equal to one on the central data neighborhood. Its transition contributes only pieces of the first type, so it is never differentiated to an order growing with λ in the second estimate.

3.1F3step 2.1algebraconstruct

For integration by parts choose finite-order localizers in the finitely many refined fiber charts. They can form an exact partition near the incidence compact without reciprocal derivatives: if χj,N are the cutoffs in [F3], take ρj,N=χj,N∏ℓ<j(1−χℓ,N). At every point of the compact at least one χj,N is identically one on a fixed neighborhood. Hence ∑jρj,N=1 there. There are a fixed finite number of factors; the product rule gives ∣∂αρj,N∣≤C(CN)∣α∣ for ∣α∣≤N. Extend the construction to a fixed slightly larger compact in the incidence charts, so all object derivatives through any fixed order m preserve the exact partition identity near K. Use the sequence indexed by N+m.

4.1F2F3F4step 3.1algebra

On a nonstationary piece use L=(iλ∂tjΨ)−1∂tj, so LeiλΨ=eiλΨ. There are no boundary terms because the localizers have compact support in the chart. After N integrations by parts the integrand is eiλΨ(L∗)N(bρj,N+m). The factorial coefficient bounds and the product rule give ∥(L∗)N(bρj,N+m)∥∞≤CN+1λ−N∑k=0NN!k!(C(N+m))k≤Cm(CmN/λ)N for N≥m+1. To obtain the first bound, expand each adjoint as a first-order derivative plus its differentiated analytic coefficient; induction distributes k derivatives to the localizer and bounds the remaining analytic derivatives by CN+1N!/k!. In the second bound use N!≤NN and ∑k≤N(C(N+m))k/k!≤eC(N+m). The bounded integration volumes and ∣eiλΨ∣≤1 leave the same bound for the integral. Applying m object derivatives first adds at most a fixed power of λ and N; the same induction with N+m gives CmλMmNMm(CmN/λ)N. Fix this m and take N=⌊ϵmλ⌋ with Cmϵm<1/2. The result is O(e−cmλ).

5.1F2step 2.1step 4.1algebra∎

The transpose packet coefficient is independent of N because the partition is exact near the support. Summing the finitely many estimates in steps 2.1 and 4.1 proves the asserted Cm estimate on a fixed neighborhood of K. Take m to be the finite distributional order in [F2] and pair with u. It follows that the data Gaussian FBI pairing of Ru is uniformly exponentially small. The definition of analytic wavefront gives the conclusion. This proof uses neither an unproved wavefront pushforward theorem nor a compact analytic bump.

LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Analytic cutoff sequence and local FBI invariance

Statement

Let u be a compactly supported distribution or a compactly supported distributional density on a real-analytic manifold. In each analytic chart use the Gaussian FBI packets of the preceding definition, paired with test densities in the first case and test functions in the second. The exponential-decay criterion is independent of the compact cutoff that equals one near the base point. It is also equivalent after an analytic chart change, with covectors transformed by the cotangent differential, and after replacing the standard Gaussian packets by their analytic pullbacks under that chart change. The latter equivalence is asserted only for the local packet and chart changes used on this page; it is the analytic-wavefront invariance needed to interpret the set geometrically.

Facts & Assumptions

Given: A compactly supported distribution u, a point-covector pair, nested coordinate neighborhoods, and the Gaussian packet families in the statement.

[F1]

Analytic wavefront set by Gaussian FBI packets: analytic regularity means a uniform exponential bound on localized Gaussian FBI pairings.

[F2]

Finite-order analytic cutoff sequence: smooth compact cutoffs can be chosen with ∣∂αχN∣≤C(CN)∣α∣ for ∣α∣≤N.

[F3]

Distributions, conormal kernels, and cotangent relations: scalar distributions act on test densities, while distributional densities act on scalar test functions; both are continuous with local fixed-support seminorm control.

[F4]

Compactly supported distributions are tempered: compactly supported Euclidean distributions have unique tempered extensions.

[F5]

Compactly supported distributions extend to smooth functions: compactly supported distributions act continuously on smooth functions by local cutoffs.

[F6]

Local analytic elliptic packet reconstruction proves bidirectional equivalence for normalized positive analytic phases and elliptic analytic amplitudes, including actual inverse and fixed-order exponentially small localization errors.

Proof

Given: The data in the statement.

1.1F1F3givenalgebra

Fix one real-analytic chart and two smooth cutoffs χ,χ~ that both equal one on a neighborhood of the base point. Choose a smaller center neighborhood U0 and a compact support neighborhood so that ∣x−y∣≥d>0 whenever x∈U0 and y∈supp⁡(χ−χ~). By continuity in the fixed-support topology [F3], in either distributional type the pairing is bounded by C0 times the maximum of finitely many derivatives of its test object; a coordinate density factor, when present, has bounded derivatives on the compact chart support. Those derivatives of (χ−χ~)eiλ(x−y)⋅ω−λ∣x−y∣2/2 are bounded by C1(1+λ)me−λd2/2 uniformly for x∈U0, directions near ω0, and λ≥1. Since a polynomial times e−λd2/2 is bounded by C2e−cλ for any fixed 0<c<d2/2, replacing one fixed-chart cutoff by the other changes the FBI packet by an exponentially small term.

1.2F3F6givenalgebra

Let κ be an analytic chart change. After shrinking to nested compact neighborhoods, ∣κ(q)−κ(y)∣≥c∣q−y∣ and Dκ(q) is invertible uniformly. The pulled-back packet has phase ϕ(y,q,ω)=ω⋅(κ(q)−κ(y))+i2∣κ(q)−κ(y)∣2. It is holomorphic after complexification, vanishes at y=q, and has derivative −Dκ(q)Tω there. First [F6] allows ω to range over a bounded open ball about its nonzero reference direction: its reference phase (q−y)⋅ω+i∣ω∣∣q−y∣2/2 is exactly the unit-direction packet with parameter λ∣ω∣, and [F6] equates this phase to the Gaussian of width λ on that open ball. Apply the same reference criterion in the new chart before pulling its packets back. We may therefore reparameterize the open frequency ball by p=Dκ(q)Tω; this is an analytic local diffeomorphism of open frequency parameters and is precisely the cotangent rule. The phase is now normalized and positive in the sense of [F6]. The Jacobian amplitude for scalar distributions is analytic and nonzero: the sign of the real determinant is constant on the smaller connected chart, so its absolute value has an analytic continuation. For distributional densities the amplitude is 1.

2.1F2F3F4F5step 1.1

Thus the exponential-decay criterion is independent of the fixed-chart cutoff. The finite-order sequence [F2] supplies the uniform localizers required when a distribution is restricted to a smaller chart; it avoids any use of compactly supported analytic bumps. For a distributional density V in the fixed chart, define the scalar distribution uV by ⟨uV,φ∣dy∣⟩=⟨V,φ⟩. Continuity follows from [F3], and the vanishing-open sets of uV and V agree because ∣dy∣ is nowhere zero, so their supports agree. The packet pairings agree by definition. Hence [F4]–[F5] give the local Euclidean tempered and smooth-function realizations for either distributional type. This proves the cutoff and localization clauses without a choice axiom.

3.1F3F6step 1.1step 2.1step 1.2algebra∎

Apply [F6] to the standard and pulled-back packets on the smaller neighborhoods. It supplies actual transition representations in both directions, with polynomially bounded transition kernels and errors exponentially small in every fixed derivative; the finite distributional order from [F3] therefore preserves their exponential size after pairing. The known exponential estimate on the source parameter neighborhood transfers to the target one. Swapping the two families gives the converse. Step 1.1 removes all fixed cutoff choices, and step 2.1 covers both distributional conventions. This proves every invariance clause in the statement, with the exact cotangent transformation from step 1.2.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Global fiber and local differential criteria for Bolker

Statement

Let Z⊂G×X be an analytic double fibration, and fix a local parameterization of its fibers over G,

(g,s)⟼(g,x(g,s)),

where s∈Rd and Dsx has rank d. Define

Eg={(s,ξ):ξ∈Tx(g,s)∗X∖0, (Dsx(g,s))Tξ=0},Lg(s,ξ)=(Dgx(g,s))Tξ.

On the cotangent relation over this incidence chart, the left projection is

(g,s,ξ)⟼(g,Lg(s,ξ)).

Consequently it is injective on this chart portion exactly when each map (s,ξ)↦Lg(s,ξ) is injective on Eg. Its differential is injective exactly when the only (s˙,ξ˙) satisfying

(Dsx)Tξ˙+(Ds2x[s˙,⋅])Tξ=0,(DsDgx[s˙,⋅])Tξ+(Dgx)Tξ˙=0

is (0,0). At a specified point of the full relation, the Bolker condition also requires that no point outside this chart portion has the same data covector; this is the global fiber-singleton clause. The displayed system is the local differential rank test.

Facts & Assumptions

Given: The local fiber parameterization and its analytic double-fibration hypotheses.

[F1]

Analytic double-fibration transform and canonical relation: πG and πX are submersions and the incidence relation is defined by the conormal bundle.

[F2]

Bolker condition for a double-fibration transform: the global condition is an injective immersion of the left projection; the pointwise condition is a singleton full fiber together with an injective differential at that point.

[F3]

Incidence-coordinate conormal kernel and canonical relation: local defining functions give the conormal relation with sign convention (η,−ξ).

Proof

Given: The parameterization (g,s)↦(g,x(g,s)).

1.1F1F3givenalgebra

A tangent vector to Z at (g,x(g,s)) has the form (g˙,Dgx g˙+Dsx s˙). A pair (η,−ξ) annihilates every such tangent vector exactly when (Dsx)Tξ=0 and η=(Dgx)Tξ. This follows by setting g˙=0 and then varying g˙ arbitrarily. Thus all conormal pairs, except the zero pair, are parameterized by (g,s,ξ)∈Eg. The rank condition on Dsx makes this conormal parameterization smooth.

2.1step 1.1F2

Under this parameterization, the left projection sends (g,s,ξ) to (g,(Dgx)Tξ), as stated. Because the first component is retained, two points in this chart portion have the same left image exactly when their g coordinates agree and their values under Lg agree. This proves the chart-portion injectivity criterion; it says nothing about a second preimage outside this chart.

3.1F2step 1.1algebra∎

A tangent vector in the kernel of the differential of the left projection has g˙=0. Differentiating the defining equation (Dsx)Tξ=0 along (s˙,ξ˙) gives (Dsx)Tξ˙+(Ds2x[s˙,⋅])Tξ=0. Differentiating its output (Dgx)Tξ gives the second displayed equation in the statement. Therefore the differential is injective exactly when the simultaneous system has only the zero solution. This is the asserted rank test, and by [F2] it is precisely the local immersion clause of Bolker.

LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Both analytic normal directions at a flat support boundary

Statement

Let u be a distribution near 0∈Rn, vanishing where xn<0. If either (0,dxn) or (0,−dxn) is absent from its Gaussian analytic wavefront set, then u=0 on a neighborhood of 0. Equivalently, if 0∈supp⁡u, both normal orientations belong to that wavefront set. The assertion also holds with the two half-spaces interchanged.

Facts & Assumptions

Given: The distribution and one of the two absent oriented normals in the statement.

[F1]

Local analytic elliptic packet reconstruction permits a bounded open neighborhood of nonzero frequency parameters and gives fixed-order exponential localization errors.

[F2]

Boundary maximum modulus principle on a bounded domain bounds a holomorphic function by its boundary modulus on a bounded domain.

[F3]

Compactly supported distributions extend to smooth functions permits pairing a localized distribution with Gaussian functions and differentiating such pairings by fixed-support seminorm estimates.

[F4]

Support of a distribution characterizes vanishing on open sets by support.

Proof

Given: The data in the statement.

1.1F3F4givenalgebra

Multiply u by a compact smooth cutoff equal to one near 0 and supported where the one-sided hypothesis holds. It remains supported in yn≥0, and the wavefront hypothesis is unchanged by exponential Gaussian tail estimates. Denote this compact distribution again by u and put U(z,λ)=⟨u(y),e−λ(z−y)2/2⟩,z∈Cn. This is entire by [F3]. A finite distributional derivative order gives the following bound on every fixed bounded complex set: ∣U(z,λ)∣≤CλMeλΦ(z),Φ(z)=∣Im⁡z∣2−(Re⁡zn)−22, where s−:=max⁡(−s,0). To justify the sharp half-space bound for a distribution, insert a smooth factor ϑ(λyn) that is one for λyn>−1/2 and zero for λyn<−1. It equals one on a neighborhood of the support, so does not change the pairing. Its derivatives of each fixed order cost only a power of λ. On its support, yn≥−1/λ, and Re⁡(z−y)2=∣Re⁡z−y∣2−∣Im⁡z∣2 gives the bound with (s+1/λ)−2 in place of s−2. Their difference is O(1/λ) uniformly for bounded s, so it changes the exponential by a bounded factor. Gaussian derivatives contribute another fixed power of λ. This proves the displayed bound using the ordinary fixed-support distributional seminorm, without assuming an estimate on the exact support set.

1.2F2algebraconstruct

We record the elementary quantitative continuation used in the left half-plane. If a holomorphic g is bounded by 1 on a disk of radius R and by e−dλ on the concentric disk of radius r<R, then on the disk of radius r<ρ<R, ∣g∣≤exp⁡ ⁣(−dλlog⁡(R/ρ)log⁡(R/r)). For the annulus compare log⁡∣g∣ with the harmonic function that is −dλ on the inner circle and 0 on the outer circle. This comparison follows from [F2]: near any hypothetical positive interior maximum of their difference, subtract a local harmonic conjugate and apply the maximum modulus principle; a small strict harmonic perturbation excludes a non-strict maximum, then let that perturbation decrease to zero. Zeros of g cannot be positive maxima. Chaining finitely many overlapping disks contained in the connected left half-plane propagates a strictly positive exponent from the initial disk to any chosen compact subset there. To make the finite chain explicit, cover a polygonal path from the initial disk to the compact set by equal small disks whose doubled disks lie in the half-plane, take successive center distances less than one quarter of the radius, and iterate the displayed estimate. The exponent is multiplied by finitely many positive radius ratios.

2.1F1step 1.1algebra

Write z=(z′,s+it). The identity e−λ∣p∣2/2U(x−ip,λ)=⟨u,eiλ(x−y)⋅p−λ∣x−y∣2/2⟩ and [F1] imply that absence of either normal gives ∣U(z,λ)∣≤Ceλ(∣Im⁡z∣2/2−c) in a fixed complex neighborhood of (0,∓i) for some c>0. The use of [F1] here is only to let p range over an open ball about ±en, rather than the unit sphere. Fix a small neighborhood of z′=0 and treat z′ as a parameter. For each such z′ the holomorphic function of one variable G(zn,λ)=e−λ∣Im⁡z′∣2/2eλzn2/2U(z′,zn,λ) satisfies ∣G∣≤CλMeλs+2/2 on bounded rectangles. On one small disk lying in s<0 near ∓i it satisfies ∣G∣≤Ce−c1λ: in this regularity estimate the additional exponent is s2/2, which is less than c/2 after shrinking that disk. Constants are uniform in z′.

3.1step 2.1step 1.2construct

Divide G by its uniform polynomial bound CλM. In the left half-plane this quotient has modulus at most 1. Step 1.2 gives r,b,d>0 such that on the segment s=−r, ∣t∣≤b, it is at most e−dλ, after decreasing d and taking λ large. The same construction works whether the initial disk is near i or −i; both lie in the same connected left half-plane neighborhood joined by a bounded path to this segment. All paths, rectangles and constants can be fixed uniformly for the chosen z′ parameters.

4.1F2step 2.1step 3.1algebrachoose

Extend to the rectangle −r≤s≤a, ∣t∣≤b, where a>0 will be small. For k=π/(2b) define w(s,t)=sinh⁡(k(a−s))sinh⁡(k(a+r))cos⁡(kt). This is harmonic, nonnegative in the rectangle, zero on the top, bottom and right sides, and between zero and one on its left side. For H=G/(CλM), the global bound in step 2.1 and the left-side improvement give, by [F2] with a harmonic conjugate of w, log⁡∣H(s+it)∣≤λ(a2/2−dw(s,t)). On the left the proposed upper bound is at least −dλ, and on the other three sides it is λa2/2, so all boundary inequalities hold. At (s,t)=(0,0), w(0,0)=sinh⁡(ka)sinh⁡(k(a+r))≥c2a for sufficiently small a, with fixed c2>0. Choose a so a2/2<dc2a/2. Continuity then gives a fixed disk about zn=0 on which ∣H∣≤e−d2λ for some d2>0. This is the needed strict improvement across the boundary.

5.1F3F4step 4.1algebra∎

For real z=x in a sufficiently small neighborhood of 0, the exponential factors defining G give ∣U(x,λ)∣≤CλMe−d2λ. On this real neighborhood the normalized Gaussian convolutions (λ/(2π))n/2U(x,λ) converge distributionally to u. For completeness, after pairing with a compact test ϑ, Fubini for a compact distribution and a rapidly decreasing Gaussian writes the pairing as ⟨u,ρλ∗ϑ⟩, where ρλ has mass one. Every fixed derivative of ρλ∗ϑ−ϑ tends uniformly to zero on the support compact: split the integral into ∣y∣<δ, where uniform continuity controls the translated derivative, and ∣y∣≥δ, where the Gaussian tail tends to zero; the same argument bounds the derivatives outside the test support. Thus [F3] proves the asserted distributional convergence. The exponential bound makes its limit zero for tests in the smaller neighborhood, so u=0 there. Reflecting xn interchanges the half-spaces and interchanges the two normal orientations. Both claims follow without a reality assumption on u.

LemmaStatement: AI-adaptedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Local Bolker incidence packets have a positive reduced phase

Statement

Let R be an analytic double-fibration transform, and fix a relation point (z0,ζ0;x0,ξ0) at which dπL is injective. For distributions u supported in a sufficiently small neighborhood of x0, data Gaussian exponential regularity at (z0,ζ0) implies object Gaussian exponential regularity at (x0,ξ0).

More precisely, for data parameters v=(q,p) near that point on the local embedded image V of πL, write χ(v)=(X(v),Ξ(v)) for the paired object covector. Writing Tλ(x,v) for the transpose localized data Gaussian, define the phase-normalized kernel Kλ(x,v)=e−iλq⋅pTλ(x,v). It has the form

Kλ(x,v)=λ−d/2eiλψ(x,v)A(x,v;λ)+Eλ(x,v),d=dim⁡Z−dim⁡X,

where A is an elliptic classical analytic amplitude, Eλ=O(e−cmλ) in every fixed object derivative, and

ψ(X(v),v)=−q⋅p,dxψ(X(v),v)=−Ξ(v),Im⁡ψ(x,v)≥c∣x−X(v)∣2

for real parameters. The map χ is an analytic submersion onto an open object cotangent neighborhood and has a local analytic section there. The constant factor in the kernel formula includes the nonzero Gaussian determinant on its continuous branch.

Facts & Assumptions

Given: The analytic transform and the relation point with injective left differential.

[F1]

Distributions, conormal kernels, and cotangent relations gives the incidence pairing, its signed conormal relation and fixed distributional derivative order.

[F2]

Analytic double-fibration transform and canonical relation gives analytic submersions, properness and a nowhere vanishing analytic total density and weight.

[F3]

Real analytic inverse and implicit functions gives analytic fiber charts and local sections of analytic submersions by selecting an invertible derivative minor.

[F4]

Holomorphic Morse normalization and Gaussian contour and Analytic stationary phase with optimal truncation give Gaussian determinant, holomorphic critical point reduction, admissible contour deformation and normalized factorial remainders.

[F5]

Local analytic elliptic packet reconstruction gives equivalence of normalized positive analytic elliptic packets with Gaussian packets, including fixed-order exponentially small errors.

[F6]

The holomorphic inverse function theorem in several complex variables gives the holomorphic inverse, and hence the implicit critical-point map after retaining the parameter coordinates.

Proof

Given: The data in the statement. All coordinate neighborhoods below are fixed and then shrunk; bounds are uniform on their compactly contained successors.

1.1F1F2F3givenalgebra

Choose analytic fiber coordinates for πX, (t,x)⟼(z(t,x),x)∈Z,t∈Rd. The matrix Dtz is injective because this map is an immersion with x retained. The conormal equations from [F1] are (Dtz)Tp=0,ξ=(Dxz)Tp. The first equations define an analytic bundle of rank dim⁡G−d in the p variables, so (t,x,p) with these equations parameterize CZ locally. The map to data cotangent space is (t,x,p)↦(z(t,x),p). Its derivative is injective by the hypothesis; selecting a full-rank coordinate minor and applying [F3] makes it an analytic embedding on a smaller neighborhood. Denote its image by V.

1.2F1F4constructalgebra

We make the exact packet resolution explicit, without importing a Fourier inversion theorem with an additional choice assumption. In Rn, set ma,bλ(y)=2−n/2π−3n/4λ3n/4eiλy⋅b−λ∣y−a∣2/2. Then, with the frequency integral interpreted by the indicated Gaussian regularization, u(y)=lim⁡ε↓0∫e−ε∣b∣2⟨u,ma,bλ‾⟩ma,bλ(y) da db in distributions. Indeed the b integral is (π/ε)n/2e−λ2∣y−y′∣2/(4ε), by completing the square and the Gaussian contour formula [F4]. The a integral is (π/λ)n/2e−λ∣y−y′∣2/4. Including the squared normalization, their product is a Gaussian kernel in y−y′ with mass tending to 1 as ε↓0 and width tending to 0. Pairing against a compact test, each fixed derivative converges uniformly on the support of u: split into a small translation neighborhood controlled by uniform continuity and its Gaussian tail. Thus [F1] justifies the distributional limit. The limiting normalization is exactly one, as also follows by multiplying (2π/λ)n and (π/λ)n/2 by the squared packet constant. Applying this identity on data space, or directly transposing the incidence integral, gives the same object kernel as direct transposition of the incidence integral.

2.1F3step 1.1algebra

The paired map χ:V→T∗X is a submersion. Here is a local linear-algebra proof. On CZ, the one-form p dz−ξ dx vanishes by the conormal equations; hence its differential also vanishes. The tangent space L of CZ therefore is isotropic for the nondegenerate bilinear alternating form dp∧dz−dξ∧dx. Its dimension is dim⁡G+dim⁡X, half the ambient dimension, so L equals its alternating orthogonal complement. If dπR(L) were a proper subspace, the nondegenerate form dξ∧dx would give a nonzero vector w orthogonal to it. Then (0,w) would be orthogonal to L, hence in L, and would lie in the kernel of dπL. This contradicts injectivity. Thus dπR is onto. The argument uses only the matrix criterion for an alternating form to be nondegenerate and the dimension formula for its orthogonal complement. By [F3], χ has a local analytic section v=v(Q,P) onto an open neighborhood of (x0,ξ0).

2.2F1F2step 1.1step 1.2algebra

Pair Ru with the data Gaussian and use the typed transpose in [F1]. Up to the harmless unit factor eiλq⋅p its object kernel is Kλ(x,v)=∫eiλΨ(t,x,v)b(t,x) dt,Ψ=−z(t,x)⋅p+i2∣z(t,x)−q∣2. The analytic coefficient b is nowhere zero by [F2] and the fiber-coordinate Jacobian. Data and fiber cutoffs are one near the base incidence point. Their transition pieces have ∣z−q∣≥r>0 after shrinking x,v; their integrals are O(e−cλ) in every fixed object derivative by the finite-order distribution estimates and the Gaussian factor. Properness ensures the remaining relevant incidence portion is compact, so finitely many such estimates suffice. A fixed fiber cutoff can therefore be inserted without changing the formula except for these errors.

2.3F3F4F6step 1.1algebra

For v∈V real there is a unique nearby real t0(v) with z(t0(v),X(v))=q. At this point Ψt=0 by step 1.1. Put D=Dxz, T=Dtz, evaluated there. Its complex t Hessian is H=B+iTTT,B=−∂t2(z⋅p), where B is real symmetric and T is injective. This matrix is invertible: if Hw=0, the imaginary part of w∗Hw is ∣Tw∣2, forcing w=0. Apply [F6] to the map retaining (x,v) and replacing t by Ψt; it gives a unique nearby complex critical point tc(x,v) for all nearby complex x,v. Shrink the original fiber neighborhood so it contains no other critical point: outside a small ball about t0, continuity and the injectivity of the local coordinate chart preserve a positive lower bound for the phase gradient or for ∣z−q∣. Define ψ(x,v)=Ψ(tc(x,v),x,v).

3.1step 1.1step 2.3algebra

We prove its strict object positivity directly, rather than assume a positivity property of a formal stationary phase. At (t0,X(v),v) the full Hessian in (t,x) is a complex symmetric matrix H=R+iS,S=[T D]T[T D],R=−∂t,x2(z⋅p). For a real object variation h, let τ be the complex solution of the stationary linearized equation Httτ+Htxh=0. Write U=(Re⁡τ,h) and W=(Im⁡τ,0). The real part of the stationary equation gives (RU)t=(SW)t. Therefore Im⁡((τ,h)TH(τ,h))=UTSU−WTSW+2WTRU=∣TRe⁡τ+Dh∣2+∣TIm⁡τ∣2. This is precisely Im⁡(hTψxxh) by differentiating the critical-point identity. If it is zero, injectivity of T gives Im⁡τ=0, and Tτ+Dh=0. The remaining stationary equation is Rttτ+Rtxh=0. These two equations say that (τ,h,p˙=0) is a tangent variation of the conormal equations (Dtz)Tp=0 and has z˙=p˙=0. By injectivity of dπL it is zero, so h=0. Compactness of the real unit sphere now gives a strictly positive lower bound for Im⁡ψxx, uniform for v in a smaller compact neighborhood in V.

4.1step 1.1step 2.3step 3.1algebra

The critical-value and derivative identities are ψ(X(v),v)=−q⋅p,ψx(X(v),v)=−Dxz(t0,X(v))Tp=−Ξ(v). The imaginary part and its first object derivative vanish there. Taylor's integral formula and the strict Hessian bound in step 3.1 therefore give Im⁡ψ(x,v)≥c∣x−X(v)∣2 for real x,v nearby. This fixes the sign for the FBI pairing: the test function has derivative −Ξ, while the distributional covector detected is +Ξ.

5.1F3F4step 2.2step 2.3step 4.1algebra

Apply analytic stationary phase at the complex critical point in step 2.3. Its applicability here includes uniform contour and remainder estimates as follows. At the base real parameters the real t contour has positive quadratic imaginary part TTT; its outer boundary has a fixed positive imaginary margin by step 2.2. For nearby parameters move the interior contour through tc(x,v) using the holomorphic quadratic coordinates in [F4], keeping the boundary fixed. In those coordinates the contour remains a graph whose Gaussian real part is bounded below by a fixed positive quadratic form, by openness of positive definiteness. Interpolate to its linear tangent contour as in the Gaussian-contour proof; the cubic error is dominated after shrinking the fixed ball. Stokes deformation consequently has a fixed exponential boundary margin. Cauchy bounds for the amplitude and the inverse coordinate map are uniform on smaller complex parameter neighborhoods. Applying the normalized remainder in [F4] with N=⌊ϵλ⌋ gives Kλ=λ−d/2eiλψA+Eλ. The leading coefficient of A is (2π)d/2b(tc(x,v),x)(det⁡(−iΨtt(tc(x,v),x,v)))−1/2 on the fixed analytic branch. At x=X(v) the critical point is the real t0(v), where the density coefficient and Hessian determinant are nonzero; continuity and holomorphy therefore make this coefficient elliptic on a smaller neighborhood. Its coefficients have uniform factorial bounds. For real parameters Im⁡ψ≥0, so normalized exponential errors also give absolute exponential errors. For fixed object derivatives take a smaller complex neighborhood where ∣Im⁡ψ∣ is less than half the boundary/remainder margin and apply Cauchy; the cutoff transition pieces already have the corresponding finite-order real derivative bounds. Hence Eλ=O(e−cmλ) in every fixed object derivative as claimed.

6.1F1F5step 2.1step 4.1step 5.1algebra∎

Suppose the data Gaussian criterion holds. By [F5], its unit-direction formulation is equivalent to the Gaussian packet with p in an open ball about the supplied nonzero data covector; positive radial frequency scaling only changes the exponential constant. Thus the data Gaussian pairings used in step 2.2 are uniformly exponentially small on an open parameter neighborhood. Pair the formula in step 5.1 with u; its finite order absorbs the errors. Multiply by λd/2eiλq⋅p, whose modulus on real parameters is only polynomial. Pull back v by the analytic section v(Q,P) from step 2.1. The resulting object test phase ψ~(x,Q,P)=ψ(x,v(Q,P))+q(Q,P)⋅p(Q,P) vanishes at x=Q, has derivative −P there and imaginary part at least c∣x−Q∣2. Its amplitude is elliptic by step 5.1. Thus [F5] converts this exponential estimate into the Gaussian criterion at (x0,ξ0). All input support here is in the chosen local object neighborhood, and every tail and inverse error has been estimated before pairing with the distribution. This proves the local implication.

LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

One-sided support forces its analytic conormal wavefront

Statement

Let X be a real-analytic manifold, let x0∈X, and let Σ be a C2 hypersurface through x0, meaning that in a smooth local chart it is the graph of a C2 function with nonzero conormal ν0∈Tx0∗X. Let f∈D′(X) vanish on one side of Σ in a neighborhood of x0, meaning that in such a chart its restriction is zero on either the strict epigraph or strict subgraph of that defining function. If either (x0,ν0)∉WF⁡A(f) or (x0,−ν0)∉WF⁡A(f), then f=0 in a neighborhood of x0.

Facts & Assumptions

Given: The real-analytic manifold X, a C2 hypersurface Σ through x0, a distribution f, one-sided vanishing, and the stated analytic-wavefront hypothesis.

[F1]

Distributions, conormal kernels, and cotangent relations: distributions are continuous functionals on compactly supported smooth densities, so localization to a chart is defined.

[F2]

Support of a distribution: the support is the complement of the largest open set on which the distribution vanishes.

[F3]

Both analytic normal directions at a flat support boundary: a distribution supported in a closed half-space at a support point has both oriented normal covectors in its Gaussian analytic wavefront set.

[F5]

The Euclidean inverse function theorem supplies the local inverse used to put the C2 hypersurface in graph form; differentiating the inverse identity preserves its C2 regularity.

[F4]

Analytic cutoff sequence and local FBI invariance: analytic coordinate changes preserve the Gaussian criterion with its cotangent transformation.

Proof

Given: The data in the statement.

1.1F1F5givenalgebraconstruct

Work in an analytic ambient chart centered at x0. The hypersurface remains C2 in that chart, since changing from its given smooth chart is a smooth diffeomorphism. A real linear coordinate change makes its tangent plane nonvertical. The C2 implicit graph theorem then writes it as xn=ψ(x′), with ψ of class C2: the inverse of a C2 map with invertible derivative is C2, by differentiating the identity for its inverse twice. Translate to have ψ(0)=0. Shrink to a convex x′ ball on which ∥D2ψ∥≤2C. Taylor's integral formula gives q−(x′):=Dψ(0)x′−C∣x′∣2≤ψ(x′)≤Dψ(0)x′+C∣x′∣2=:q+(x′). Both supporting quadratics are real analytic and have the same differential as ψ at 0.

2.1F1F2step 1.1algebraconstruct

Suppose first that f vanishes on the strict subgraph of ψ. Its local support lies in xn≥ψ(x′), hence in xn≥q−(x′). The analytic shear (x′,xn)↦(x′,xn−q−(x′)) has analytic inverse (y′,yn)↦(y′,yn+q−(y′)), determinant 1, and sends this latter closed side into yn≥0. If instead f vanishes on the strict epigraph, its support lies in xn≤ψ(x′)≤q+(x′) and use the corresponding analytic shear with q+. In either case the pulled-back normal dyn at 0 is dxn−Dψ(0)dx′, a nonzero scalar multiple of the supplied conormal ν0. This flattens an analytic supporting quadratic; it does not flatten the original C2 graph analytically.

3.1F2F3F4step 2.1givenalgebra∎

If f already vanishes near x0, there is nothing to prove. Otherwise x0∈supp⁡f by [F2]. Localize inside the chart. Under the appropriate shear, [F3] then puts both dyn and −dyn in the analytic wavefront set at the origin. By [F4] these are exactly both conormal orientations at x0, up to positive frequency scaling. Either absence hypothesis in the statement contradicts this conclusion. Thus f=0 near x0. Every construction used finite-dimensional coordinates and explicit quadratics; it introduces no choice assumption.

TheoremStatement: Literature-sourcedProof: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Analytic wavefront recovery under Bolker

Statement

Let R be an analytic double-fibration transform and let

(z0,ζ0;x0,ξ0)∈CZ

be a point of its incidence cotangent relation. Assume the Bolker condition holds at this point, meaning πL−1(z0,ζ0)={(z0,ζ0;x0,ξ0)} and dπL is injective at that relation point. For every compactly supported distribution f∈E′(X), if (z0,ζ0)∉WF⁡A(Rf), then (x0,ξ0)∉WF⁡A(f). This is a qualitative microlocal implication; it asserts no noisy-data stability estimate.

Facts & Assumptions

Given: The analytic transform R, the relation point with singleton full left fiber and injective left differential, and compactly supported f with the stated data analytic regularity.

[F1]

Analytic double-fibration transform and canonical relation: the transform is properly supported on compact object supports and has a nowhere vanishing analytic incidence density and weight.

[F2]

Bolker condition for a double-fibration transform: the pointwise condition gives the entire singleton left fiber and injective differential at this point.

[F3]

Analytic incidence localization away from a data cotangent fiber: input support with no incidence cotangent relation over the supplied data covector has an exponentially small data Gaussian transform, with finite-order distributional estimates.

[F4]

Local Bolker incidence packets have a positive reduced phase: for distributions supported sufficiently near the supplied object point, data Gaussian regularity implies object Gaussian regularity, by the exact packet resolution, reduced positive phase, estimated stationary phase and elliptic packet criterion.

[F5]

Analytic cutoff sequence and local FBI invariance: the Gaussian criterion is independent of local cutoff and analytic chart and applies to distributional densities as well as scalar distributions.

Proof

Given: The data in the statement.

1.1F1F2F3givenchoose

Choose a smooth compact object cutoff ρ equal to one near x0 and supported in the small object neighborhood supplied by [F4]. Write f=ρf+(1−ρ)f. The second summand is compactly supported away from x0. By [F2] its support has no relation point over (z0,ζ0), because that full fiber consists of the supplied point over x0. Hence [F3] gives (z0,ζ0)∉WF⁡A(R((1−ρ)f)). This includes all incidence points outside the local coordinate patch; it is not inferred merely from local injectivity.

2.1F2F4F5step 1.1givenalgebra

By hypothesis the Gaussian data transform of Rf is exponentially small on some data parameter neighborhood. Subtract the exponential estimate from step 1.1, using the same data chart and a common smaller cutoff neighborhood by [F5]. Linearity gives the same estimate for R(ρf) at the supplied data covector. The differential clause of [F2] supplies the local Bolker hypothesis in [F4]. Since ρf is supported in its chosen small object neighborhood, [F4] yields (x0,ξ0)∉WF⁡A(ρf).

3.1F4F5step 2.1algebra∎

The localized distributions ρf and f agree on a neighborhood of x0. Their Gaussian transforms with any common cutoff supported there agree exactly; all other cutoff choices differ only by the exponential Gaussian tails in [F5]. Thus step 2.1 gives (x0,ξ0)∉WF⁡A(f), as asserted. The two suppliers account separately for global fiber uniqueness and local differential injectivity, and all errors are controlled in the finite number of derivatives needed by the compact distribution. No stability or choice assumption has been added.

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Local support from one-sided vanishing and visible conormal data

Statement

Let R be an analytic double-fibration transform, let (z0,ζ0;x0,η0)∈CZ, and let Σ be a C2 hypersurface through x0 with (x0,η0)∈N∗Σ∖0. Let f∈E′(X) vanish on one side of Σ near x0. If the pointwise Bolker condition holds at (z0,ζ0;x0,η0) and Rf=0 in a neighborhood of z0, then f=0 in a neighborhood of x0.

Facts & Assumptions

Given: The transform R, a relation point satisfying pointwise Bolker, a C2 hypersurface Σ, and a compactly supported distribution f with the stated vanishing and data hypotheses.

[F1]

Analytic double-fibration transform and canonical relation: Rf is a distributional density on the data manifold.

[F2]

Analytic wavefront recovery under Bolker: if the data covector is absent from WF⁡A(Rf) under pointwise Bolker, then the paired object covector is absent from WF⁡A(f).

[F3]

One-sided support forces its analytic conormal wavefront: one-sided vanishing plus absence of either oriented analytic conormal implies local vanishing.

[F4]

Analytic wavefront set by Gaussian FBI packets: exponential decay of the localized Gaussian FBI pairings is the criterion for absence from WF⁡A.

Proof

Given: The data in the statement.

1.1F1F4given

Choose a data cutoff supported inside the neighborhood on which Rf=0 and equal to one near z0. Its localized FBI test functions are supported where the distribution vanishes, so all the pairings are exactly zero for every frequency. By [F4], this gives (z0,ζ0)∉WF⁡A(Rf).

2.1F2F3step 1.1given∎

By [F2], step 1.1 gives (x0,η0)∉WF⁡A(f). Applying the one-sided continuation implication [F3] then gives f=0 near x0. All their hypotheses hold: the relation point has pointwise Bolker, f has compact support, and the same nonzero object covector is a conormal to the supplied C2 hypersurface.

4 · Examples, counterexamples and false statements

None yet.

Sources