QIQTH.StripUniqueness

← all sections · ← StandardSubspaceModularFlow · ValueSelection →

StripUniqueness · entries 979–992 of 1000

Definition 979 (kmsStrip).  source ↗

The (closed) KMS strip {0 ≤ Im z ≤ 1} — the inverse temperature is normalised to β = 1.

Used by im_zero_on_strip, eqConst_of_im_zero_strip.

Definition 980 (kmsStripOpen).  source ↗

The open KMS strip {0 < Im z < 1}.

Used by im_zero_on_strip, eqConst_of_im_zero_strip, eqConst_of_im_zero_halfStrip.

Lemma 981 (im_zero_on_strip).  source ↗

Max-modulus on the strip: vanishing imaginary part propagates from the edges to the interior. If g is bounded-holomorphic on the KMS strip (DiffContOnCl + a uniform bound) and its imaginary part vanishes on both boundary edges (Im g = 0 on Im z = 0 and Im z = 1), then Im g = 0 on the whole closed strip. Proof: |exp(±i·g)| = exp(∓Im g) = 1 on the edges, so by PhragmenLindelof’s horizontal-strip max-modulus principle |exp(i·g)| ≤ 1 and |exp(−i·g)| ≤ 1 throughout, forcing Im g = 0. This is the reflection-free substitute for RvD’s “real on both edges ⇒ constant” step (the crux of the KMS-uniqueness Theorem 3.8).

Proof. Immediate from the definitions. $\square$

Used by eqConst_of_im_zero_strip.

Lemma 982 (eqConst_of_im_zero_strip).  source ↗

Bounded-holomorphic with imaginary part zero on both strip edges ⟹ constant. Combining the max-modulus propagation im_zero_on_strip (Im g = 0 throughout) with the open-mapping corollary AnalyticOnNhd.eq_const_of_re_eq_const (a holomorphic function with constant real part is constant): since Re(i·g) = −Im g = 0 on the (open, connected) strip, i·g is constant, hence g is constant. This is RvD Theorem 3.8’s “real on both edges ⇒ constant” conclusion, obtained reflection-free.

Proof. By kmsStrip, im_zero_on_strip. $\square$

Used by eqConst_of_im_zero_halfStrip.

Definition 983 (kmsHalfStrip).  source ↗

The (closed) half KMS strip {−1/2 ≤ Im z ≤ 0} — the strip RvD Theorem 3.8 / Prop 3.5 actually use: the g-function lives here, with the lower edge Im = −1/2 (the half-shift Δ^{1/2} = J).

Used by h1_of_stripKMSrvd, corrC_bdd_halfStrip, gFunction_bottom_real_of_kms_match, gFunction_bottom_real_of_faithful_kms, eqZero_of_im_zero_edge_halfStrip, eqOn_of_im_zero_edge_halfStrip.

Definition 984 (kmsHalfStripOpen).  source ↗

The open half KMS strip {−1/2 < Im z < 0}.

Used by h1_of_stripKMSrvd, gFunction_eq_zero_const, gFunction_bottom_real_of_kms_match, gFunction_bottom_real_of_faithful_kms, eqZero_of_im_zero_edge_halfStrip, eqOn_of_im_zero_edge_halfStrip, eqConst_of_im_zero_halfStrip.

Lemma 985 (eqZero_of_im_zero_edge_halfStrip).  source ↗

One-edge boundary uniqueness on the HALF strip {−1/2 ≤ Im z ≤ 0}: a function bounded-holomorphic there and vanishing on the top edge Im z = 0 vanishes on the whole closed half-strip. Same Hadamard three-lines route as eqZero_of_im_zero_edge, rotated to the vertical strip re⁻¹'[−1/2, 0] with the zero edge at u = 0 (‖f‖ ≤ M^{1−θ}·0^θ = 0 interior), then Set.EqOn.of_subset_closure. This is the CORRECT-strip analytic core of RvD Theorem 3.8 (the full-strip corrC framework mis-modeled it).

Proof. Immediate from the definitions. $\square$

Used by eqOn_of_im_zero_edge_halfStrip.

Lemma 986 (eqOn_of_im_zero_edge_halfStrip).  source ↗

One-edge determination on the HALF strip (RvD Prop 3.5 / Theorem 3.8 setting): two bounded-holomorphic functions on {−1/2 ≤ Im z ≤ 0} agreeing on the top edge Im z = 0 agree on the whole closed half-strip. Apply eqZero_of_im_zero_edge_halfStrip to F − G. This is the correct-strip analog of eqOn_of_im_zero_edge: the matching step where the entire-orbit correlation ⟨h(z), w⟩ and the KMS function (which share their Im = 0 boundary values ⟨U_t ξ, η⟩) coincide on the half-strip, so the KMS function’s lower-edge Im = −1/2 reality transfers to the orbit correlation.

Proof. By eqZero_of_im_zero_edge_halfStrip. $\square$

Used by gFunction_bottom_real_of_kms_match.

Lemma 987 (eqConst_of_im_zero_halfStrip).  source ↗

Real on both edges ⟹ constant on the HALF-strip {−1/2 < Im z < 0}. Adapts the unit-strip two-edge Phragmén–Lindelöf constancy (eqConst_of_im_zero_strip, edges Im = 0, Im = 1) via the affine map φ(w) = −w/2, which maps {0 < Im w < 1} onto {−1/2 < Im z < 0} (top edge Im w = 0 ↦ Im z = 0, bottom edge Im w = 1 ↦ Im z = −1/2). G(w) = g(−w/2) is bounded-holomorphic on the unit strip and real on both its edges, hence constant; pulling back gives g constant on the half-strip. This is the constancy the RvD Theorem 3.8 g-function (real on Im = 0 and Im = −1/2) consumes.

Proof. By kmsStripOpen, eqConst_of_im_zero_strip. $\square$

Used by gFunction_eq_zero_const.

Definition 988 (negStrip).  source ↗

The unit KMS strip {−1 ≤ Im z ≤ 0} and its interior — the strip of RvD Definition 3.4 (the full-width KMS condition, before Proposition 3.5 folds it to the half-strip).

Used by stripKMSrvd_real_midline, h1_of_stripKMSrvd, eqZero_of_im_zero_edge_negStrip, eqOn_of_im_zero_edge_negStrip, real_on_midline_of_conj_flip.

Definition 989 (negStripOpen).  source ↗

Used by eqZero_of_im_zero_edge_negStrip, eqOn_of_im_zero_edge_negStrip, real_on_midline_of_conj_flip.

Lemma 990 (eqZero_of_im_zero_edge_negStrip).  source ↗

One-edge boundary uniqueness on the UNIT strip {−1 ≤ Im z ≤ 0}: a function bounded-holomorphic there and vanishing on the top edge Im z = 0 vanishes on the whole closed strip. Same Hadamard three-lines route as eqZero_of_im_zero_edge_halfStrip, on re⁻¹'[−1, 0]. This is the uniqueness that powers RvD Proposition 3.5’s reflection argument (the full-width KMS strip of Definition 3.4).

Proof. Immediate from the definitions. $\square$

Used by eqOn_of_im_zero_edge_negStrip.

Lemma 991 (eqOn_of_im_zero_edge_negStrip).  source ↗

One-edge determination on the UNIT strip {−1 ≤ Im z ≤ 0}: two bounded-holomorphic functions agreeing on the top edge Im z = 0 agree on the whole closed strip. Apply eqZero_of_im_zero_edge_negStrip to F − G. The full-width companion of eqOn_of_im_zero_edge_halfStrip, the uniqueness RvD Proposition 3.5 invokes for the KMS extension on {−1 ≤ Im ≤ 0}.

Proof. By eqZero_of_im_zero_edge_negStrip. $\square$

Used by real_on_midline_of_conj_flip.

Lemma 992 (real_on_midline_of_conj_flip).  source ↗

RvD Proposition 3.5 — reality on the mid-line. A bounded-holomorphic f on the unit strip {−1 < Im z < 0} (DiffContOnCl), satisfying the conjugate-flip boundary relation f(t − i) = conj(f(t)) on the real axis, is real on the mid-line Im z = −1/2: Im f(t − i/2) = 0 for all real t. This is RvD’s reflection argument: the reflected function g(z) = conj(f(conj z − i)) is holomorphic (DifferentiableAt.conj_conj), bounded, and agrees with f on the edge Im = 0 (g(t) = conj(f(t − i)) = conj(conj(f(t))) = f(t) by the flip), so g = f on the strip (eqOn_of_im_zero_edge_negStrip); evaluating at t − i/2 gives f(t − i/2) = conj(f(t − i/2)). …

Proof. By eqOn_of_im_zero_edge_negStrip. $\square$

Used by stripKMSrvd_real_midline, h1_of_stripKMSrvd.

← all sections · ← StandardSubspaceModularFlow · ValueSelection →