QIQTH.ModularRelativeEntropy

← all sections · ← LocalizedMode · PPWaveMetric →

ModularRelativeEntropy · entries 491–533 of 1000

Definition 491 (rvdSpecMeasure).  source ↗

The scalar spectral measure of R = P + Q at the one-particle vector ξ — a finite measure on spectrum ℝ R, with total mass ‖ξ‖².

Used by borelFC_congr_ae, deviceOpC_neg_half_eq, borelFC_inner_self, borelFC_apply_norm_sq, rvdSpec_borelFC_diag, rvdSpecMeasure_zero_levelSet, rvdSpecMeasure_two_levelSet, rvdSpecMeasure_endpoints, and 6 more.

Definition 492 (devSpecReal).  source ↗

The device spectral symbol on the real axis ω ↦ d_t(ω) = u_t(ω)·√ω, the bounded measurable function of R whose functional calculus is the real-axis device operator Δ^{it}·√R.

Used by devSpecReal_measurable, devSpecReal_norm_le, deviceOpReal, deviceOpReal_zero, deviceOpReal_eq.

Lemma 493 (devSpecReal_measurable).  source ↗

Proof. By devChar, measurable_devChar. $\square$

Used by deviceOpReal, deviceOpReal_zero, deviceOpReal_eq.

Lemma 494 (devSpecReal_norm_le).  source ↗

Proof. By rvdRC_spectrum_mem_Icc, devChar_norm_le_Icc. $\square$

Used by deviceOpReal, deviceOpReal_zero, deviceOpReal_eq.

Definition 495 (deviceOpReal).  source ↗

The real-axis device operator Δ^{it}·√R = d_t(R), the bounded Borel functional calculus of R at the device symbol devSpecReal (‖d_t‖ ≤ √2 on the spectrum, no regular window).

Used by deviceOpC_ofReal, deviceOpReal_zero, deviceOpReal_eq, deviceVecF_real_eq.

Definition 496 (deviceOpC).  source ↗

The complex-z device operator d_z(R) = (2−R)^{iz} R^{−iz+1/2} for z in the half-strip −1/2 ≤ Im z ≤ 0, where ‖d_z‖ ≤ √2 on σ(R) ⊆ [0,2] (no regular window, devChar_norm_le_Icc + rvdRC_spectrum_mem_Icc). This is RvD’s Proposition 3.7 device (verified against the rendered source): the operator whose J-image J·(d_z(R) ζ) is the (anti-holomorphic, since J is antilinear) second-slot vector of the Theorem 3.8 g-function g(z) = ⟨h(z), J d_z(R) ζ⟩. Generalizes deviceOpReal (the z = t real-axis case) to the whole half-strip.

Used by deviceOpC_neg_half_eq, modConj_deviceOpC_neg_half, modConj_deviceVecF_bottom_eq, deviceVecF, deviceVecF_eq_of_mem, deviceOpC_ofReal, deviceOpC_norm_le, deviceOpC_bottomEdge_eq, and 9 more.

Definition 497 (deviceVecF).  source ↗

Total device-vector function z ↦ deviceOpC(z)ζ (piece 4 of the strong holomorphy): a dite-total function on all of ℂ, equal to deviceOpC(z)ζ on the closed half-strip {−1/2 ≤ Im z ≤ 0} (where the device operator’s √2 bound holds) and 0 outside. The totality sidesteps the deviceOpC-takes-proofs friction: HasDerivAt (deviceVecF S ζ) is a statement about a genuine ℂ → H function, provable at every interior z₀ because deviceVecF agrees with the borelFC branch on a neighborhood. Its Fréchet derivative is borelFC(ω ↦ i·log((2−ω)/ω)·d_{z₀}(ω))ζ, with ‖slope − deriv‖² = ∫‖Δ_z − ∂d‖² dμ^R_ζ → 0 (borelFC_sub + borelFC_smul + borelFC_apply_norm_sq + tendsto_integral_devChar_remainder_sq).

Used by h1_of_stripKMSrvd, gConstancy_of_inputs, oneParticleBW_of_inputs, oneParticleBW_of_stripKMSrvd_density, gFunction_eq_zero_const, gConstancy_entire, gFunction_top_edge_real_all, gConstancy_entire_of_bottom, and 22 more.

Lemma 498 (deviceVecF_eq_of_mem).  source ↗

On the closed half-strip, deviceVecF is the device operator applied to ζ (proof-irrelevant dite).

Proof. Immediate from the definitions. $\square$

Used by hasDerivAt_deviceVecF, deviceVecF_real_eq, deviceVecF_bottom_eq, deviceVecF_continuousOn.

Lemma 499 (deviceOpC_ofReal).  source ↗

deviceOpC at a real point is deviceOpReal (d_{(t:ℂ)} = d_t): the half-strip device operator restricts to the real-axis device operator Δ^{it}·√R on the boundary Im z = 0.

Proof. Immediate from the definitions. $\square$

Used by deviceVecF_real_eq.

Lemma 500 (deviceOpC_norm_le).  source ↗

Operator-norm bound for the complex-z device operator: ‖d_z(R)‖ ≤ 2√2 uniformly on the half-strip −1/2 ≤ Im z ≤ 0 (the bounded-FC norm bound ‖borelFC f‖ ≤ 2·sup‖f‖ applied to the device symbol bound ‖d_z‖ ≤ √2). This is the operator-level boundedness the g-function g(z) = ⟨h(z), J d_z(R) ζ⟩ consumes: ‖g(z)‖ ≤ ‖h(z)‖·‖d_z(R)ζ‖ ≤ ‖h(z)‖·2√2·‖ζ‖, uniform over the half-strip.

Proof. By boundedFC, boundedFC_norm_le, PVM_of_selfAdjoint, borelFC, rvdRC, rvdRC_isSelfAdjoint, devChar. $\square$

Used by deviceVecF_norm_le.

Lemma 501 (deviceOpReal_zero).  source ↗

The device operator at z = 0 is √R (deviceOpReal 0 = rvdSqrtR, the device interpolation start). devChar 0 = √·, so deviceOpReal 0 = borelFC(√·) = cfcCont(√·), and cfcCont(√·) is the positive square root of R: (cfcCont √·)² = R (cfcCont_mul + cfcCont_coord, since √ω·√ω = ω on σ(R)⊆[0,∞)), and cfcCont(√·) = (cfcCont ∜·)² ≥ 0 (cfcCont ∜· self-adjoint as a real symbol). CFC.sqrt_unique then identifies it with CFC.sqrt R = rvdSqrtR. Hence deviceOpReal 0 ζ = R^{1/2}ζ = ξ, so the g-function’s value at the origin is g(0) = ⟪η, Jξ⟫ — the right-hand side of GConstancy.

Proof. By devSpecReal, devSpecReal_measurable, devSpecReal_norm_le, borelFC, rvdRC, borelFC_congr, rvdRC_isSelfAdjoint, specCoord, rvdRC_spectrum_mem_Icc, cfcCont, cfcCont_mul, cfcCont_star, cfcCont_coord, devChar, devChar_zero. $\square$

Used by deviceOpReal_eq.

Lemma 502 (cfcCont_sqrtTwoSub_eq).  source ↗

The continuous symbol √(2−·) gives √(2−R): cfcCont(√(2−·)) = rvdSqrtTwoSubR (the bottom-edge analogue of deviceOpReal_zero, which does cfcCont(√·) = √R). Route: the square is 2−R (cfcCont_mul + cfcCont(2−coord) = 2−R via cfcCont_add/_smul/_one/_coord, since √(2−ω)·√(2−ω) = 2−ω on σ(R) ⊆ [0,2]), and cfcCont(√(2−·)) = (cfcCont ∜(2−·))² ≥ 0; CFC.sqrt_unique then identifies it with CFC.sqrt(2−R) = rvdSqrtTwoSubR. This is the CONTINUOUS half of deviceOpC(−i/2) = √(2−R); the device character d_{−i/2} then matches √(2−·) only μ-a.e. (they swap at the spectral endpoints {0,2}), closed by borelFC_congr_ae + rvdSpecMeasure_endpoints.

Proof. By rvdTwoSubRC, specCoord, rvdRC_spectrum_mem_Icc, cfcCont_one, cfcCont_mul, cfcCont_add, cfcCont_smul, cfcCont_star, cfcCont_coord. $\square$

Used by deviceOpC_neg_half_eq.

Lemma 503 (deviceOpReal_eq).  source ↗

The real-axis device operator factors as Δ^{it}·√R: deviceOpReal t = modUnitary S t · rvdSqrtR (the general top-edge operator identity, deviceOpReal_zero is the t = 0 case). devChar(↑t) = u_t·√· (devChar_ofReal), so borelFC(devChar ↑t) = borelFC(u_t)·borelFC(√·) = Δ^{it}·√R (borelFC_mul + modUnitary = borelFC(u_t) + borelFC(√·) = rvdSqrtR from deviceOpReal_zero). Hence the device vector at the real axis is deviceVec(t) = deviceOpReal t ζ = Δ^{it}(√R ζ) = Δ^{it}ξ, so the g-function’s top edge is g(t) = ⟪U_t η, J Δ^{it} ξ⟫ (gTopEdge_real, real).

Proof. By devSpecReal, devSpecReal_measurable, devSpecReal_norm_le, deviceOpReal_zero, borelFC, borelFC_mul, rvdRC, modChar, borelFC_congr, modSpecFun, modSpecFun_measurable, modSpecFun_norm_le, rvdRC_isSelfAdjoint, devChar_ofReal, devChar_zero. $\square$

Used by deviceVecF_real_eq.

Lemma 504 (borelFC_inner_self).  source ↗

L² identity for the bounded Borel FC: ⟪f(R)ζ, f(R)ζ⟫ = ∫ conj(f)·f dμ^R_ζ (= ∫|f|² dμ, so ‖f(R)ζ‖² = ∫|f|² dμ^R_ζ). Via ⟪Aζ,Aζ⟫ = ⟪ζ, A*Aζ⟫ (adjoint_inner_right), A* = borelFC(conj f) (borelFC_adjoint), A*·A = borelFC(conj f·f) (borelFC_mul), then the spectral bridge ⟪ζ, g(R)ζ⟫ = ∫ g dμ^R_ζ (inner_borelFC). This is the linchpin for the strong (Fréchet) holomorphy of z ↦ d_z(R)ζ: the difference-quotient remainder q − d satisfies ‖q − d‖² = ∫|Δ_z − ∂_z d|² dμ^R_ζ → 0 by dominated convergence (the derivative is dominated by the devChar_deriv_norm_le constant).

Proof. By scalarMeasure, diagInt, bilinDiag, PVM_of_selfAdjoint, inner_borelFC, borelFC_mul, borelFC_adjoint. $\square$

Used by borelFC_apply_norm_sq.

Lemma 505 (borelFC_apply_norm_sq).  source ↗

L² isometry (real form): ‖f(R)ζ‖² = ∫ ‖f(ω)‖² dμ^R_ζ. The real-valued restatement of borelFC_inner_self (⟪f(R)ζ,f(R)ζ⟫ = ↑‖f(R)ζ‖², and conj(f)·f = ↑‖f‖²). This is the form the strong-holomorphy difference-quotient argument uses directly: ‖q_z − d‖² = ∫‖Δ_z − ∂_z d‖² dμ^R_ζ → 0.

Proof. By borelFC_inner_self. $\square$

Used by deviceOpC_slope_normSq, deviceOpC_diff_normSq.

Lemma 506 (rvdSpec_borelFC_diag).  source ↗

Diagonal of the bounded Borel FC against the spectral measure: ⟪x, f(R)x⟫ = ∫ f dμ^R_x. The linear (un-conjugated) companion to borelFC_inner_self, via the spectral bridge (inner_borelFC + bilinDiag_self + diagInt). This is the bridge for borelFC_congr_ae (borelFC depends only on the μ^R_x-a.e. class of f): combined with clm_eq_of_inner_self_eq it gives borelFC(f) = borelFC(g) whenever f =ᵐ g for every spectral measure — the tool for deviceOpC(−i/2) = √(2−R) (the device character and √(2−r) differ only on the E-null endpoints).

Proof. By scalarMeasure, diagInt, bilinDiag, PVM_of_selfAdjoint, inner_borelFC. $\square$

Used by borelFC_congr_ae.

Lemma 507 (rvdSpecMeasure_zero_levelSet).  source ↗

No spectral atom at 0: μ^R_x({λ = 0}) = 0, from E({0}) = 0 (rvdRC_E_zero_levelSet).

Proof. By E, scalarMeasure, scalarMeasure_apply, PVM_of_selfAdjoint, rvdRC_isSelfAdjoint, rvdRC_E_zero_levelSet. $\square$

Used by rvdSpecMeasure_endpoints.

Lemma 508 (rvdSpecMeasure_two_levelSet).  source ↗

No spectral atom at 2: μ^R_x({λ = 2}) = 0, from E({2}) = 0 (rvdRC_E_two_levelSet).

Proof. By E, scalarMeasure, scalarMeasure_apply, PVM_of_selfAdjoint, rvdRC_isSelfAdjoint, rvdRC_E_two_levelSet. $\square$

Used by rvdSpecMeasure_endpoints.

Lemma 509 (rvdSpecMeasure_endpoints).  source ↗

The device-character endpoints are μ^R_x-null: μ^R_x({λ ∈ {0,2}}) = 0. This is exactly the a.e.-equality input for borelFC_congr_ae needed for deviceOpC(−i/2) = √(2−R): the device character d_{−i/2} and the symbol √(2−r) of √(2−R) differ ONLY at the spectral endpoints {0,2}, which carry no spectral mass (no atom at 0 or 2, as R and 2−R are injective).

Proof. By rvdSpecMeasure_zero_levelSet, rvdSpecMeasure_two_levelSet. $\square$

Used by deviceOpC_neg_half_eq.

Lemma 510 (deviceOpC_bottomEdge_eq).  source ↗

Bottom-edge t-translation of the device operator: deviceOpC(t − i/2) = Δ^{it}·deviceOpC(−i/2) (the bottom-edge analogue of deviceOpReal_eq). devChar(↑t − i/2) = u_t·devChar(−i/2) EVERYWHERE (via modCharC_add: u_{↑t + (−i/2)} = u_{↑t}·u_{−i/2}, no endpoint issue), so borelFC factors through borelFC_mul into modUnitary t · deviceOpC(−i/2). Hence the device vector along the bottom edge is deviceVec(t − i/2) = Δ^{it}·deviceVec(−i/2) — the modular flow translating the fixed bottom-edge vector.

Proof. By borelFC, borelFC_mul, rvdRC, modChar, borelFC_congr, modSpecFun, modSpecFun_measurable, modSpecFun_norm_le, rvdRC_isSelfAdjoint, rvdRC_spectrum_mem_Icc, modCharC, modCharC_ofReal, modCharC_add, devChar, measurable_devChar, devChar_norm_le_Icc. $\square$

Used by deviceVecF_bottom_eq.

Lemma 511 (devCharDeriv_norm_le_slab).  source ↗

Derivative-norm bound of the device character on a slab (the ‖∂_z d_z(ω)‖ ≤ C companion to devChar_slope_norm_le): on {−β₁ < Im w < −β₀}, ‖i·log((2−ω)/ω)·d_w(ω)‖ ≤ C uniformly in ω (devChar_deriv_norm_le for ω ∈ (0,2); the coefficient vanishes for ω ∈ {0,2}). This bounds the candidate Fréchet derivative ∂_z d at every slab point — used as the second half of the dominating constant 4C² in the strong-holomorphy dominated-convergence step.

Proof. By rvdRC_spectrum_mem_Icc, modCharC, devChar_deriv_norm_le. $\square$

Used by tendsto_integral_devChar_remainder_sq, deviceDerivOpC, deviceOpC_slope_normSq.

Lemma 512 (devChar_slope_norm_le).  source ↗

Uniform slope (Lipschitz) bound of the device character on a slab (piece 2 of the strong-holomorphy dominated-convergence argument): on the open slab s = {−β₁ < Im z < −β₀} ⊂ (−1/2,0), ‖d_z(ω) − d_{z₀}(ω)‖ ≤ C·‖z − z₀‖ with C = √2(2/β₀+log2) + √2(2/(1/2−β₁)+log2) the devChar_deriv_norm_le constant — UNIFORM in the spectral point ω. Via the complex mean-value inequality Convex.norm_image_sub_le_of_norm_hasDerivWithin_le (hasDerivAt_devChar_Icc on the convex slab + the devChar_deriv_norm_le derivative bound, with ω ∈ {0,2} giving d_z z-constant ⇒ derivative 0 ≤ C). Hence ‖Δ_z(ω)‖ ≤ C uniformly: the dominating constant for the dominated-convergence step.

Proof. By rvdRC_spectrum_mem_Icc, modCharC, devChar_deriv_norm_le, hasDerivAt_devChar_Icc. $\square$

Used by tendsto_integral_devChar_remainder_sq.

Lemma 513 (tendsto_devChar_slope).  source ↗

Pointwise difference-quotient convergence of the device character (piece 1 of the strong-holomorphy dominated-convergence argument): for each spectral point ω, the slope (d_z(ω) − d_{z₀}(ω))/(z − z₀) → i·log((2−ω)/ω)·d_{z₀}(ω) as z → z₀ (z ≠ z₀). Immediate from hasDerivAt_devChar_Icc via hasDerivAt_iff_tendsto_slope (slope_def_field). Fed into tendsto_integral_filter_of_dominated_convergence to drive ∫‖Δ_z − ∂_z d‖² dμ^R_ζ → 0, hence the Fréchet derivative of z ↦ deviceOpC(z)ζ (via borelFC_sub + borelFC_apply_norm_sq).

Proof. By rvdRC_spectrum_mem_Icc, hasDerivAt_devChar_Icc. $\square$

Used by tendsto_integral_devChar_remainder_sq.

Lemma 514 (tendsto_integral_devChar_remainder_sq).  source ↗

Strong-holomorphy dominated convergence (piece 3 — the heart): the L² remainder of the device-vector difference quotient vanishes, ∫‖(d_z(ω)−d_{z₀}(ω))/(z−z₀) − ∂_z d_{z₀}(ω)‖² dμ^R_ζ → 0 as z → z₀ (z ≠ z₀), for z₀ in the slab. Lebesgue dominated convergence (tendsto_integral_filter_of_dominated_convergence): the integrand → 0 pointwise (tendsto_devChar_slope, piece 1) and is dominated by the constant 4C² (devChar_slope_norm_le + devCharDeriv_norm_le_slab, piece 2: ‖Δ_z(ω)‖ ≤ C, ‖∂d(ω)‖ ≤ C), integrable on the finite measure μ^R_ζ. Combined with borelFC_sub + borelFC_apply_norm_sq (‖slope − d‖² = ∫‖Δ_z − ∂d‖² dμ), this gives the Fréchet derivative of z ↦ deviceOpC(z)ζ.

Proof. By devCharDeriv_norm_le_slab, devChar_slope_norm_le, tendsto_devChar_slope, scalarMeasure, instIsFiniteMeasure_scalarMeasure, PVM_of_selfAdjoint, rvdRC_isSelfAdjoint, measurable_devChar. $\square$

Used by hasDerivAt_deviceVecF.

Lemma 515 (deviceOpC_sub).  source ↗

Device-operator difference as a single borelFC (first step of the slope operator-algebra): deviceOpC(z) − deviceOpC(z₀) = borelFC(d_z − d_{z₀}). Just borelFC_sub read backwards, using that deviceOpC is definitionally a borelFC with the √2 bound.

Proof. By borelFC_sub. $\square$

Used by deviceOpC_slope_normSq, deviceOpC_diff_normSq.

Definition 516 (deviceDerivOpC).  source ↗

Candidate Fréchet derivative operator of the device at an interior point: ∂_z d_{z₀}(R) = borelFC(ω ↦ i·log((2−ω)/ω)·d_{z₀}(ω)), the spectral operator whose symbol is the z-derivative of the device character at z₀. Bounded by the devCharDeriv_norm_le_slab constant C(β₀,β₁) (the operator is independent of the slab (β₀,β₁) ∋ Im z₀, by borelFC_congr). Applied to ζ it is the Fréchet derivative of deviceVecF S ζ at z₀ (hasDerivAt_deviceVecF).

Used by deviceOpC_slope_normSq, hasDerivAt_deviceVecF, differentiableOn_deviceVecF.

Lemma 517 (deviceOpC_slope_normSq).  source ↗

L² identity for the device-vector slope remainder (the operator-algebra heart of piece 4): ‖(z−z₀)⁻¹·(deviceOpC(z)ζ − deviceOpC(z₀)ζ) − deviceDerivOpC(z₀)ζ‖² = ∫‖Δ_z(ω) − ∂d(ω)‖² dμ^R_ζ, the integrand of tendsto_integral_devChar_remainder_sq. The slope-minus-derivative vector is a single borelFC applied to ζ (deviceOpC_sub + borelFC_smul + borelFC_sub, pushed through the CLM sub_apply/smul_apply), so borelFC_apply_norm_sq turns its norm² into the spectral L² integral.

Proof. By borelFC_apply_norm_sq, devCharDeriv_norm_le_slab, deviceOpC_sub, borelFC, rvdRC_isSelfAdjoint, rvdRC_spectrum_mem_Icc, borelFC_smul, borelFC_sub, measurable_devChar, devChar_norm_le_Icc. $\square$

Used by hasDerivAt_deviceVecF.

Lemma 518 (hasDerivAt_deviceVecF).  source ↗

Strong (Fréchet) holomorphy of the device vector (piece 4 COMPLETE): z ↦ deviceOpC(z)ζ is complex-differentiable at every interior point z₀ of the open half-strip, with derivative deviceDerivOpC(z₀)ζ. The slope-minus-derivative norm → 0: its square is the remainder integral (deviceOpC_slope_normSq) which → 0 (tendsto_integral_devChar_remainder_sq), so ‖slope − deriv‖ = √(remainder) → √0 = 0 (Real.sqrt continuity), hence slope → deriv (tendsto_iff_norm_sub_tendsto_zero). This defeats the holomorphy wall WITHOUT Mathlib’s missing weak⟹strong (Dunford): the H-valued derivative is obtained from a scalar dominated-convergence integral.

Proof. By rvdSpecMeasure, deviceOpC, deviceVecF_eq_of_mem, tendsto_integral_devChar_remainder_sq, deviceOpC_slope_normSq, rvdRC, devChar. $\square$

Used by differentiableOn_deviceVecF.

Lemma 519 (differentiableOn_deviceVecF).  source ↗

The device vector is holomorphic on the open half-strip (piece 4 ⇒ DifferentiableOn): immediate from hasDerivAt_deviceVecF at every interior point (choosing the slab β₀ = −Im z₀/2, β₁ = (1/2 − Im z₀)/2 around z₀). This is the strong-holomorphic half-strip input the g-function Phragmén–Lindelöf constancy consumes — now available for the device vector of EVERY standard subspace.

Proof. By deviceDerivOpC, hasDerivAt_deviceVecF. $\square$

Used by differentiableOn_gFunction.

Lemma 520 (deviceVecF_real_eq).  source ↗

Real-axis value of the device vector: deviceVecF(t) = Δ^{it}·√R ζ (the top-edge value of the g-function). Via deviceVecF_eq_of_mem (the strip contains the real axis), deviceOpC_ofReal (d_{(t:ℂ)} = d_t), and deviceOpReal_eq (d_t = Δ^{it}·√R). With ξ = √R ζ, J·deviceVecF(t) = JΔ^{it}ξ = Δ^{it}(Jξ) is the second slot of the g-function on its real edge g(t) = ⟪V_t η, Δ^{it}Jξ⟫.

Proof. By deviceOpReal, deviceOpC, deviceVecF_eq_of_mem, deviceOpC_ofReal, deviceOpReal_eq. $\square$

Used by deviceVecF_zero, gFunction_real_eq.

Lemma 521 (differentiableOn_gFunction).  source ↗

The device-vector RvD g-function is HOLOMORPHIC on the open half-strip (piece 2 of the endgame): g(z) = ⟪J·d_z(R)ζ, V_z η⟫ = modConjBilin S (deviceVecF S ζ z) (gaussSmearC V n η z) is complex-differentiable on {−1/2 < Im z < 0}. It is the continuous ℂ-bilinear form modConjBilin (= ⟪J·,·⟫, holomorphic by the J-cancellation) applied to the two HOLOMORPHIC curves: the device vector deviceVecF (differentiableOn_deviceVecF, the strong-holomorphy result) and the entire V-orbit gaussSmearC (differentiable_gaussSmearC). Bilinear chain rule (DifferentiableOn.clm_apply). This is the holomorphic strip function the Phragmén–Lindelöf constancy g(t) = g(0) ⟹ GConstancy consumes.

Proof. By differentiableOn_deviceVecF, differentiable_gaussSmearC. $\square$

Used by diffContOnCl_gFunction.

Lemma 522 (deviceVecF_zero).  source ↗

Device vector at the origin: deviceVecF(0) = √R ζ (= ξ, the comparison point). From deviceVecF_real_eq at t = 0 (Δ^{i·0} = 1, modUnitary_zero).

Proof. By deviceVecF_real_eq, modUnitary, modUnitary_zero. $\square$

Used by gFunction_zero.

Lemma 523 (gFunction_zero).  source ↗

g-function value at the origin g(0) = ⟪J ξ, η_n⟫ (ξ = √R ζ, η_n = gaussSmear): the comparison point of the Phragmén–Lindelöf constancy. With g constant this equals g(t), the top-edge matrix element — the heart of RvD Theorem 3.8. Via deviceVecF_zero + gaussSmearC_zero.

Proof. By deviceVecF_zero, modConjBilin_apply, gaussSmearC_zero. $\square$

Used by gConstancy_entire.

Lemma 524 (gFunction_real_eq).  source ↗

g-function value on the real axis (top edge) g(t) = ⟪Δ^{it}(J ξ), V_t η_n⟫ (ξ = √R ζ): via deviceVecF_real_eq (d_t ζ = Δ^{it}√R ζ), gaussSmearC_ofReal (h(t) = V_t η_n), and modConj_commute_modUnitary (JΔ^{it} = Δ^{it}J). Its conjugate is the GConstancy LHS ⟪V_t η_n, Δ^{it}Jξ⟫; reality (RvD top edge) makes g(t) equal to it.

Proof. By deviceVecF_real_eq, modConjBilin_apply, modConj_commute_modUnitary, gaussSmearC_ofReal. $\square$

Used by gConstancy_entire, gFunction_top_edge_real.

Lemma 525 (gFunction_top_edge_real).  source ↗

Top-edge reality of the g-function (RvD Theorem 3.8, the real-axis edge): for ξ = √R ζ ∈ 𝒦 and the V-orbit staying in 𝒦, g(t) = ⟪Δ^{it}(Jξ), V_t η_n⟫ is REAL. Δ^{it}(Jξ) = J(Δ^{it}ξ) (modConj_commute_modUnitary) with Δ^{it}ξ ∈ 𝒦 (modUnitary_mapsTo_K), so J(Δ^{it}ξ) ⊥ i𝒦 (projIK_modConj_eq_zero_of_mem_K, J𝒦 = (i𝒦)^⊥); pairing it against the 𝒦-vector V_t η_n is real (inner_real_of_mem_K_perp_IK, RvD Prop 2.3) — and g(t) is the conjugate of that. Geometric, no analysis; the real-axis edge of the holomorphic strip g-function feeding the Phragmén–Lindelöf constancy.

Proof. By gFunction_real_eq, modUnitary, mem_K_iff_projK, modConj, projIK_modConj_eq_zero_of_mem_K, inner_real_of_mem_K_perp_IK, modUnitary_mapsTo_K, modConj_commute_modUnitary. $\square$

Used by gFunction_top_edge_real_all.

Lemma 526 (deviceVecF_bottom_eq).  source ↗

Bottom-edge value of the device vector: deviceVecF(t − i/2) = Δ^{it}·deviceOpC(−i/2) ζ, the modular flow translating the FIXED bottom vector deviceOpC(−i/2) ζ (= √(2−R) ζ off the spectral endpoints {0,2}). Via deviceVecF_eq_of_mem (the closed half-strip contains the mid-line Im z = −1/2) and deviceOpC_bottomEdge_eq. This is the second-slot device vector on the bottom edge of the g-function, whose reality is the KMS input (HalfStripReal) feeding the Phragmén–Lindelöf constancy.

Proof. By deviceVecF_eq_of_mem, deviceOpC_bottomEdge_eq. $\square$

Used by modConj_deviceVecF_bottom.

Lemma 527 (modConj_deviceVecF_bottom).  source ↗

Device/J commute on the bottom edge: J·deviceVecF(t − i/2) = Δ^{it}·(J·deviceOpC(−i/2) ζ). The modular conjugation pulls through Δ^{it} (modConj_commute_modUnitary) after deviceVecF_bottom_eq. With deviceOpC(−i/2) = √(2−R) and J √(2−R) ζ = √R ζ (modConj_rvdSqrtTwoSubR_of_fixed, J ζ = ζ) this becomes Δ^{it}·√R ζ = Δ^{it}ξ — the second slot of the g-function bottom edge g(t − i/2), whose reality is the KMS input (RvD’s (2−R)^{1/2}ζ = Jξ device argument).

Proof. By deviceVecF_bottom_eq, modConj_commute_modUnitary. $\square$

Used by modConj_deviceVecF_bottom_eq.

Lemma 528 (deviceVecF_norm_le).  source ↗

Uniform bound of the device vector ‖deviceVecF z‖ ≤ 2√2·‖ζ‖ for EVERY z (the device operator’s 2√2 operator-norm bound, deviceOpC_norm_le, applied to ζ; 0 off the strip). The bounded factor of the g-function ‖g(z)‖ ≤ 2√2·‖ζ‖·‖h(z)‖, the bound input the Phragmén–Lindelöf constancy needs.

Proof. By deviceOpC, deviceOpC_norm_le. $\square$

Used by gFunction_norm_le.

Lemma 529 (gFunction_norm_le).  source ↗

Pointwise bound of the g-function ‖g(z)‖ ≤ 2√2·‖ζ‖·‖h(z)‖ (h(z) = gaussSmearC): J is an isometry (modConj_norm) and ‖d_z(R)ζ‖ ≤ 2√2·‖ζ‖ (deviceVecF_norm_le), so the inner product is bounded by the product (norm_inner_le_norm). Combined with the Gaussian bound on ‖h(z)‖ this gives the uniform strip bound the Phragmén–Lindelöf constancy consumes.

Proof. By deviceVecF_norm_le, modConj, modConj_norm, modConjBilin_apply. $\square$

Used by gFunction_eq_zero_const.

Lemma 530 (deviceOpC_diff_normSq).  source ↗

L² identity for the device-vector difference: ‖deviceOpC(z)ζ − deviceOpC(z₀)ζ‖² = ∫‖d_z(ω) − d_{z₀}(ω)‖² dμ^R_ζ. The difference is a single borelFC applied to ζ (deviceOpC_sub), so borelFC_apply_norm_sq turns its norm² into the spectral L² integral. Feeds the device-vector continuity (∫‖d_z − d_{z₀}‖² → 0 by dominated convergence, d_z continuous + dominated by 2√2) — the continuity-to-closure half of DiffContOnCl for the g-function.

Proof. By borelFC_apply_norm_sq, deviceOpC_sub, borelFC, rvdRC_isSelfAdjoint, rvdRC_spectrum_mem_Icc, measurable_devChar, devChar_norm_le_Icc. $\square$

Used by deviceVecF_continuousOn.

Lemma 531 (tendsto_integral_devChar_diff_sq).  source ↗

Device-character L² continuity (dominated convergence): ∫‖d_z(ω) − d_{z₀}(ω)‖² dμ^R_ζ → 0 as z → z₀ within the closed half-strip {−1/2 ≤ Im z ≤ 0}. The integrand → 0 pointwise (d_z continuous in z, hasDerivAt_devChar_Icc.continuousAt) and is dominated by (√2+√2)² = 8 (devChar_norm_le_Icc), integrable on the finite spectral measure. With deviceOpC_diff_normSq this gives the device-vector continuity ‖deviceVecF z − deviceVecF z₀‖ = √(∫…) → 0 — the continuity-to-closure half of DiffContOnCl.

Proof. By scalarMeasure, instIsFiniteMeasure_scalarMeasure, PVM_of_selfAdjoint, rvdRC_isSelfAdjoint, rvdRC_spectrum_mem_Icc, measurable_devChar, devChar_norm_le_Icc, hasDerivAt_devChar_Icc. $\square$

Used by deviceVecF_continuousOn.

Lemma 532 (deviceVecF_continuousOn).  source ↗

The device vector is continuous on the closed half-strip (the DiffContOnCl continuity-to-closure): ContinuousOn (deviceVecF S ζ) {−1/2 ≤ Im z ≤ 0}. At each z₀, ‖deviceVecF z − deviceVecF z₀‖ = √(∫‖d_z − d_{z₀}‖² dμ^R_ζ) (deviceVecF_eq_of_mem + deviceOpC_diff_normSq + Real.sqrt_sq), which → √0 = 0 (tendsto_integral_devChar_diff_sq + Real.sqrt continuity). Together with differentiableOn_deviceVecF this is the device-vector half of DiffContOnCl for the g-function.

Proof. By rvdSpecMeasure, deviceOpC, deviceVecF_eq_of_mem, deviceOpC_diff_normSq, tendsto_integral_devChar_diff_sq, rvdRC, devChar. $\square$

Used by diffContOnCl_gFunction.

Lemma 533 (diffContOnCl_gFunction).  source ↗

The g-function is bounded-holomorphic (DiffContOnCl) on the half-strip (the full analytic regularity for Phragmén–Lindelöf): holomorphic on the open half-strip (differentiableOn_gFunction) and continuous up to the closure {−1/2 ≤ Im z ≤ 0} (the bilinear modConjBilin of the continuous device vector deviceVecF_continuousOn and the continuous V-orbit gaussSmearC). With the uniform bound (gFunction_norm_le) and the two edge realities this is the exact input the half-strip constancy consumes.

Proof. By differentiableOn_gFunction, deviceVecF_continuousOn, differentiable_gaussSmearC. $\square$

Used by gFunction_eq_zero_const.

← all sections · ← LocalizedMode · PPWaveMetric →